Optics and Lenses [efr-ZCTD]
Optics and Lenses [efr-ZCTD]
We have already given somewhat of an account of lenses, optics, and their applications in the introduction. We briefly review the theory here, especially to normalize the notation and definitions. The best general source for this material is still Reference [riley-optics].
The definition of optic relies on the notion of coend, which we briefly recall, see Reference [fosco-coend-calculus] for a textbook account. If F: \mathcal {I}^\mathrm {op} \times \mathcal {I} \to \mathcal {C} is a functor, the coend \int ^{i \in I} F(i,i) is defined as the initial object receiving a map f_i : F(i,i) \to \int ^{i \in I} F(i,i) for each i \in I, so that for each \phi : i \to j, the square
If \mathcal {C} has enough colimits, we may express the coend as the coequalizer of the diagram \coprod _{f : i \to j \in \mathcal {I}} F(i,j) \rightrightarrows \coprod _{i} F(i,i), where the two maps are given on each component by F(i,f): F(i,j) \to F(i,i) and F(f,j) : F(i,j) \to F(j,j), respectively. (This is Remark 1.2.4 in Reference [fosco-coend-calculus]). Note that in particular this implies that if \mathcal {C} has all colimits, then it also has all coends.
Note that if \mathcal {M},\mathcal {C},\mathcal {D} are symmetric monoidal and these actions are symmetric, \mathsf {Optic}_\mathcal {M}(\mathcal {C},\mathcal {D}) inherits a symmetric monoidal structure given by {A \choose X} \otimes {B \choose Y} = {A \otimes B \choose X \otimes Y}. (Also given a braiding one can induce a non-symmetric monoidal structure, but this almost never comes up).
As noted above, the coend \int ^M \mathcal {C}(X, M \cdot Y) \times \mathcal {D}(M \cdot B, A) consists of triples (M, f: X \to M \cdot Y, g: M \cdot B \to A) up to the equivalence relation which, for every \phi : M \to M', f: X \to M \cdot Y, g: M' \cdot B \to A, identifies the two tuples (M', (\phi \cdot 1_Y) f, g) and (M, f, g (\phi \cdot 1_B)). Note that this relation is not assumed to be inherently an equivalence relation---one takes the transitive-symmetric closure as usual.
We call this relation the sliding relation (because we slide the map \phi from the backwards part to the forwards part).
Of course, we can also let the arrows in \mathcal {D} go in the same direction as \mathcal {C}. This does not seem to have played any role in the literature, but we will give this a name, as it is a useful example to have in mind for Markov fibrations (where we will construct our dependent optics, conceptually, as a fiberwise opposite)
The fact that in \mathsf {Optic}(\mathcal {M}), states (maps from the monoidal unit) on {A \choose X} are given by states on X, while costates are given by maps X \to A plays an important role in the use of optics to describe open games. See § [efr-GFG0] for more on this.
Let us say a few things about lenses.
In this case we sometimes write \mathsf {Lens}(\mathcal {C}) for the category \mathsf {Optic}(\mathcal {C}). We have the following fact:
This is the first way to see the maps of (\mathcal {C}^\to )^\mathrm {fop} as dependent lenses---they receive the category of lenses as a full subcategory.
