Search

# Promonoidal category of optics

Last updated Sep 8, 2023

## # Definition

Let $π$ be a monoidal category. The promonoidal category of optics $\operatorname{Optic}(π)$ is a category with the same objects as $π Γ π^{op}$ and with morphisms given by $$\operatorname{Optic}(π)\left( \binom{X}{X’};\binom{Y}{Y’} \right) = β«^{A \in π} π(Y; A β X) Γ π(A β X’; Y’).$$ The promonoidal structure is given by $$\operatorname{Optic}(π)\left( \binom{X}{X’},\binom{Y}{Y’};\binom{Z}{Z’} \right) = β«^{A \in π} π(Z; X β A) Γ π(A β X; B β Y) Γ π(Y β B’ ; Z’),$$ $$\operatorname{Optic}(π)\left( \binom{X}{X’} \right) = π(X,X’).$$

## # Protensor and prounit of optics

The promonoidal structure of optics is determined by two profunctors $ππ(\bullet)$ and $ππ(\bullet,\bullet;\bullet)$. The actions of optics on these two profunctors determine multiple possible insertions of optics and transformations on the context that an optic determines.

The prounit of optics becomes a profunctor, $(ππ(\bullet), <)$, with optic evaluation, $$(<)οΉ ππ\left( \begin{matrix} X \\ X’ \end{matrix} \right) Γ ππ\left( \begin{matrix} X \\ X’ \end{matrix}; \begin{matrix} Y \\ Y’ \end{matrix} \right) β ππ\left( \begin{matrix} Y \\ Y’ \end{matrix} \right),$$ defined by $f < \langle g_0 \mid g_1 \rangle = g_0 β¨Ύ (id β f) β¨Ύ g_1$.

The protensor of optics becomes a profunctor, $(ππ(\bullet,\bullet;\bullet),>_l,>_r,<)$, with the two possible optic insertions and evaluation, $$(>_l)οΉ ππ\left( \begin{matrix} X \\ X’ \end{matrix}; \begin{matrix} A \\ A’ \end{matrix} \right) Γ ππ\left( \begin{matrix} A \\ A’ \end{matrix}, \begin{matrix} Y \\ Y’ \end{matrix} ; \begin{matrix} Z \\ Z’ \end{matrix}\right) β ππ\left( \begin{matrix} X \\ X’ \end{matrix}, \begin{matrix} Y \\ Y’ \end{matrix} ; \begin{matrix} Z \\ Z’ \end{matrix}\right),$$ $$(>_r)οΉ ππ\left( \begin{matrix} Y \\ Y’ \end{matrix}; \begin{matrix} A \\ A’ \end{matrix} \right) Γ ππ\left( \begin{matrix} X \\ X’ \end{matrix}, \begin{matrix} A \\ A’ \end{matrix} ; \begin{matrix} Z \\ Z’ \end{matrix}\right) β ππ\left( \begin{matrix} X \\ X’ \end{matrix}, \begin{matrix} Y \\ Y’ \end{matrix} ; \begin{matrix} Z \\ Z’ \end{matrix}\right),$$ $$(<)οΉ ππ\left( \begin{matrix} X \\ X’ \end{matrix}, \begin{matrix} A \\ A’ \end{matrix} ; \begin{matrix} A \\ A’ \end{matrix}\right) Γ ππ\left( \begin{matrix} A \\ A’ \end{matrix}; \begin{matrix} Z \\ Z’ \end{matrix} \right) β ππ\left( \begin{matrix} X \\ X’ \end{matrix}, \begin{matrix} Y \\ Y’ \end{matrix} ; \begin{matrix} Z \\ Z’ \end{matrix}\right),$$ which are defined by $$\langle gβ \mid gβ \rangle \mathbin{>_l}\langle fβ \mid fβ \mid fβ \rangle = \langle fβ β¨Ύ (id β gβ) \mid (id β gβ) β¨Ύ fβ \mid fβ \rangle,$$ $$\langle hβ \mid hβ \rangle \mathbin{>_r}\langle fβ \mid fβ \mid fβ \rangle = \langle fβ \mid fβ β¨Ύ (id β hβ) \mid (id β hβ) β¨Ύ fβ \rangle,$$ $$\langle fβ \mid fβ \mid fβ \rangle \mathbin{<} \langle tβ \mid tβ \rangle = \langle tβ β¨Ύ (id β fβ) \mid (id β fβ) \mid (id β fβ) β¨Ύ tβ \rangle.$$

## # Procoherence for optics

The unitors may be constructed via coend calculus, using the units of the monoidal category. \begin{aligned} & β«^{\begin{pmatrix} X \\ X’ \end{pmatrix} \in ππ} ππ\left( \begin{matrix} X \\ X’ \end{matrix} \right) Γ ππ\left( \begin{matrix} X \\ X’ \end{matrix}, \begin{matrix} Y \\ Y’ \end{matrix}; \begin{matrix} Z \\ Z’ \end{matrix} \right) \\ \cong & \quad \mbox{Introducing units by definition of optic.} \\ & β«^{\begin{pmatrix} X \\ X’ \end{pmatrix} \in ππ} ππ\left( \begin{matrix} X \\ X’ \end{matrix} ; \begin{matrix} I \\ I \end{matrix} \right) Γ ππ\left( \begin{matrix} X \\ X’ \end{matrix}, \begin{matrix} Y \\ Y’ \end{matrix}; \begin{matrix} Z \\ Z’ \end{matrix} \right) \\ \cong & \quad \mbox{Yoneda reduction.}\\ & ππ\left( \begin{matrix} I \\ I \end{matrix}, \begin{matrix} Y \\ Y’ \end{matrix}; \begin{matrix} Z \\ Z’ \end{matrix} \right) \\ \cong & \quad \mbox{Reducing units by definition of optic.}\\ & ππ\left( \begin{matrix} Y \\ Y’ \end{matrix}; \begin{matrix} Z \\ Z’ \end{matrix} \right) \\ \end{aligned} The associators are finally constructed via coend calculus, by noticing that three-part data accessors have a common representation, independent of that how we get to them. \begin{aligned} & β«^{\begin{pmatrix} U \\ U’ \end{pmatrix} \in ππ} ππ \left( \begin{matrix} X \\ X’ \end{matrix}, \begin{matrix} Y \\ Y’ \end{matrix}; \begin{matrix} U \\ U’ \end{matrix} \right) Γ ππ \left( \begin{matrix} U \\ U’ \end{matrix}, \begin{matrix} Z \\ Z’ \end{matrix}; \begin{matrix} T \\ T’ \end{matrix} \right) \\ \cong & \quad \mbox{Splitting by definition of optic.} \\ & β«^{\begin{pmatrix} U \\ U’ \end{pmatrix} \in ππ, C \in π} ππ \left( \begin{matrix} X \\ X’ \end{matrix}, \begin{matrix} Y \\ Y’ \end{matrix}; \begin{matrix} U \\ U’ \end{matrix} \right) Γ ππ \left( \begin{matrix} U \\ U’ \end{matrix}; \begin{matrix} T \\ C β Z \end{matrix} \right) Γ π \left( C β Z’,T' \right) \\ \cong & \quad \mbox{Yoneda reduction.} \\ & β«^{C \in π} ππ \left( \begin{matrix} X \\ X’ \end{matrix}, \begin{matrix} Y \\ Y’ \end{matrix}; \begin{matrix} T \\ C β Z \end{matrix} \right) Γ π \left( C β Z’,T' \right) \\ \cong & \quad \mbox{By the definition of protensor.} \\ & β«^{A, B, C \in π} π (T; A β X) Γ π(A β X’; B β Y) Γ π(B β Y’; C β Z)Γπ(C β Z’,T’) \\ \cong & \quad \mbox{By the definition of protensor.} \\ & β«^{A \in π} π \left( T, A β X \right) Γ ππ \left( \begin{matrix} Y \\ Z \end{matrix}, \begin{matrix} Z \\ Z’ \end{matrix}; \begin{matrix} A β X’ \\ T’ \end{matrix} \right)\\ \cong & \quad \mbox{Yoneda reduction.} \\ & β«^{\begin{pmatrix} U \\ U’ \end{pmatrix} \in ππ, A \in π} π \left( T, A β X \right) Γ ππ \left( \begin{matrix} U \\ U’ \end{matrix}; \begin{matrix} A β X’ \\ T’ \end{matrix} \right) Γ ππ \left( \begin{matrix} Y \\ Y’ \end{matrix}, \begin{matrix} Z \\ Z’ \end{matrix}; \begin{matrix} U \\ U’ \end{matrix} \right)\\ \cong & \quad \mbox{Splitting by definition of optic.} \\ & β«^{\begin{pmatrix} U \\ U’ \end{pmatrix} \in ππ} ππ \left( \begin{matrix} X \\ X’ \end{matrix}, \begin{matrix} U \\ U’ \end{matrix}; \begin{matrix} T \\ T’ \end{matrix} \right) Γ ππ \left( \begin{matrix} Y \\ Y’ \end{matrix}, \begin{matrix} Z \\ Z’ \end{matrix}; \begin{matrix} U \\ U’ \end{matrix} \right). \end{aligned}