Promonoidal category of optics

See also

• Doubles for Monoidal Categories (Pastro and Street, 2008)
• Open Diagrams via Coend Calculus (Román, 2020)
• optics
• Monoidal contexts

Definition

Let $\mathbb{V}$ be a monoidal category. The multicategory - promonoidal category of optics $\mathrm{Optic}(\mathbb{V})$ is a category with the same objects as $\mathbb{V}\times {\mathbb{V}}^{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{array}{rl}& {\int }^{\left(\begin{array}{c}X\\ X^{\prime }\end{array}\right)\in \mathbb{OV}}\mathbb{OV}\left(\begin{array}{c}X\\ X^{\prime }\end{array}\right)\times \mathbb{OV}\left(\begin{array}{c}X\\ X^{\prime }\end{array},\begin{array}{c}Y\\ Y^{\prime }\end{array};\begin{array}{c}Z\\ Z^{\prime }\end{array}\right)\\ \cong & \text{mbox}Introducingunitsbydefinitionofoptic.\\ & {\int }^{\left(\begin{array}{c}X\\ X^{\prime }\end{array}\right)\in \mathbb{OV}}\mathbb{OV}\left(\begin{array}{c}X\\ X^{\prime }\end{array};\begin{array}{c}I\\ I\end{array}\right)\times \mathbb{OV}\left(\begin{array}{c}X\\ X^{\prime }\end{array},\begin{array}{c}Y\\ Y^{\prime }\end{array};\begin{array}{c}Z\\ Z^{\prime }\end{array}\right)\\ \cong & \text{mbox}Yonedareduction.\\ & \mathbb{OV}\left(\begin{array}{c}I\\ I\end{array},\begin{array}{c}Y\\ Y^{\prime }\end{array};\begin{array}{c}Z\\ Z^{\prime }\end{array}\right)\\ \cong & \text{mbox}Reducingunitsbydefinitionofoptic.\\ & \mathbb{OV}\left(\begin{array}{c}Y\\ Y^{\prime }\end{array};\begin{array}{c}Z\\ Z^{\prime }\end{array}\right)\end{array}$$

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{array}{rl}& {\int }^{\left(\begin{array}{c}U\\ U^{\prime }\end{array}\right)\in \mathbb{OV}}\mathbb{OV}\left(\begin{array}{c}X\\ X^{\prime }\end{array},\begin{array}{c}Y\\ Y^{\prime }\end{array};\begin{array}{c}U\\ U^{\prime }\end{array}\right)\times \mathbb{OV}\left(\begin{array}{c}U\\ U^{\prime }\end{array},\begin{array}{c}Z\\ Z^{\prime }\end{array};\begin{array}{c}T\\ T^{\prime }\end{array}\right)\\ \cong & \text{mbox}Splittingbydefinitionofoptic.\\ & {\int }^{\left(\begin{array}{c}U\\ U^{\prime }\end{array}\right)\in \mathbb{OV},C\in \mathbb{V}}\mathbb{OV}\left(\begin{array}{c}X\\ X^{\prime }\end{array},\begin{array}{c}Y\\ Y^{\prime }\end{array};\begin{array}{c}U\\ U^{\prime }\end{array}\right)\times \mathbb{OV}\left(\begin{array}{c}U\\ U^{\prime }\end{array};\begin{array}{c}T\\ C\otimes Z\end{array}\right)\times \mathbb{V}\left(C\otimes Z^{\prime },T^{\prime }\right)\\ \cong & \text{mbox}Yonedareduction.\\ & {\int }^{C\in \mathbb{V}}\mathbb{OV}\left(\begin{array}{c}X\\ X^{\prime }\end{array},\begin{array}{c}Y\\ Y^{\prime }\end{array};\begin{array}{c}T\\ C\otimes Z\end{array}\right)\times \mathbb{V}\left(C\otimes Z^{\prime },T^{\prime }\right)\\ \cong & \text{mbox}Bythedefinitionofprotensor.\\ & {\int }^{A,B,C\in \mathbb{V}}\mathbb{V}(T;A\otimes X)\times \mathbb{V}(A\otimes X^{\prime };B\otimes Y)\times \mathbb{V}(B\otimes Y^{\prime };C\otimes Z)\times \mathbb{V}(C\otimes Z^{\prime },T^{\prime })\\ \cong & \text{mbox}Bythedefinitionofprotensor.\\ & {\int }^{A\in \mathbb{V}}\mathbb{V}\left(T,A\otimes X\right)\times \mathbb{OV}\left(\begin{array}{c}Y\\ Z\end{array},\begin{array}{c}Z\\ Z^{\prime }\end{array};\begin{array}{c}A\otimes X^{\prime }\\ T^{\prime }\end{array}\right)\\ \cong & \text{mbox}Yonedareduction.\\ & {\int }^{\left(\begin{array}{c}U\\ U^{\prime }\end{array}\right)\in \mathbb{OV},A\in \mathbb{V}}\mathbb{V}\left(T,A\otimes X\right)\times \mathbb{OV}\left(\begin{array}{c}U\\ U^{\prime }\end{array};\begin{array}{c}A\otimes X^{\prime }\\ T^{\prime }\end{array}\right)\times \mathbb{OV}\left(\begin{array}{c}Y\\ Y^{\prime }\end{array},\begin{array}{c}Z\\ Z^{\prime }\end{array};\begin{array}{c}U\\ U^{\prime }\end{array}\right)\\ \cong & \text{mbox}Splittingbydefinitionofoptic.\\ & {\int }^{\left(\begin{array}{c}U\\ U^{\prime }\end{array}\right)\in \mathbb{OV}}\mathbb{OV}\left(\begin{array}{c}X\\ X^{\prime }\end{array},\begin{array}{c}U\\ U^{\prime }\end{array};\begin{array}{c}T\\ T^{\prime }\end{array}\right)\times \mathbb{OV}\left(\begin{array}{c}Y\\ Y^{\prime }\end{array},\begin{array}{c}Z\\ Z^{\prime }\end{array};\begin{array}{c}U\\ U^{\prime }\end{array}\right).\end{array}$$