Optics

Optics are getters and setters for data in functional form. Let T_0 be the primitive types. Define data T = T_0 + \Pi T^* + \Sigma T^*. Data are either a primitive type, products of data, or sums of data.

A lens takes data T, a view of the data A, and an update taking T and a replacement B for the view to produce data U with the view of A replaced by B, (T\to A)\times(S\times B)\to U.

A prism takes data T, a choice of A in T, and an way to build U from B to produce data U, (T\to A + U)\times(B\to U).

The Yoneda lemma provides a way of representing homsets of any category in terms of homsets of \mathbf{Set}: \mathbf{C}(A,B)\cong \int_X \mathbf{Set}(\mathbf{C}(B,X), \mathbf{C}(A,X)). If \mathbf{C} is \mathbf{Set} this is analogous to Cayley’s theorem that every group can be respresented by a permutation group. This may have stunted the development of group theory by hiding the abstract axioms in a much richer and concrete representation.

If \mathbf{C} is a category we write \mathbf{C}(A,B) for all arrows in \mathbf{C} from object A\in\mathbf{C} to object B\in\mathbf{C}. If \mathbf{C} and \mathbf{D} are categories we write [\mathbf{C},\mathbf{D}] for the functor category with objects being the functors from \mathbf{C} to \cal{D} and arrows being the natural transformations.