Definition Optic [efr-MMQZ]
Definition Optic [efr-MMQZ]
Let \mathcal {M} be a monoidal category which acts on two categories \mathcal {C}, \mathcal {D}. Then the category of optics \mathsf {Optic}_\mathcal {M}(\mathcal {C},\mathcal {D}) has
- Objects pairs {A \in \mathcal {D} \choose X \in \mathcal {C}}
- The set of morphisms {A \choose X} \to {B \choose Y} given by the coend \int ^{M \in \mathcal {M}} \mathcal {C}(X, M \cdot Y) \times \mathcal {D}(M \cdot B,A)
- Given two optics with representatives (M,f: X \to M \cdot Y,g : M \cdot B \to A), (N, f': Y \to N \cdot Z, g': N \cdot C \to B), their composite is given by (M \otimes N, (1_M \cdot f')f, g (1_M \cdot g')), where we omit coherence morphisms.
When \mathcal {C} is a monoidal category acting on itself by tensor, we write \mathsf {Optic}_\mathcal {C}(\mathcal {C},\mathcal {C}) =: \mathsf {Optic}(\mathcal {C})