Monoidal contexts

Monoidal contexts

Definition. Let $(C,\otimes ,I)$ be a monoidal category. The category of monoidal contexts has objects the pairs of objects of $C$ and morphisms $\mathbb{B}C\left(\genfrac{}{}{0ex}{}{X}{Y},\genfrac{}{}{0ex}{}{A}{B}\right)={\int }^{M,N}C(A;M\otimes X\otimes N)\times C(M\otimes Y\otimes N;B).$ Remark. One-sided contexts have been called “optics” or “monoidal lenses”. We avoid that name because it means different things to different authors and it is not self-explanatory.

We write the generic element of a context as $⟨f｜g⟩$, for some $f\in C(A;M\otimes X\otimes N)$ and some $g\in C(M\otimes Y\otimes N;B)$. These are pairs quotiented by the equivalence relation generated by dinaturality on $M$ and $N$, $⟨f⨾(m\otimes i{d}_X\otimes n⟩｜g⟩=⟨f｜(m\otimes i{d}_Y\otimes n)⨾g⟩.$ Composition is defined as follows; identities are pairs of identities. $⟨f｜g⟩⨾⟨f^{\prime }｜g^{\prime }⟩=⟨f⨾(i{d}_M\otimes f^{\prime }\otimes i{d}_N)｜(i{d}_M\otimes g^{\prime }\otimes i{d}_N)⨾g⟩,$ $i{d}_{\left(\genfrac{}{}{0ex}{}{A}{B}\right)}=⟨i{d}_A｜i{d}_B⟩.$

Promonoidal structures

Promonoidal vertical structure. The category of monoidal contexts is promonoidal with the following protensor and prounit.

\quad 𝔹ℂ_{◁}\left( {X \atop Y} \right) = ℂ(X,Y).$$ This is to say that elements of the prounit are just morphisms $f ∈ 𝔹ℂ_{◁}\left( {X \atop Y} \right)$; while elements of the protensor are triples $⟨ f ｜ g ｜ h ⟩$ for some $f ∈ ℂ(A; M ⊗ X ⊗ N)$, some $g ∈ ℂ(M ⊗ Y ⊗ N; M' ⊗ X' ⊗ N')$ and some $h ∈ ℂ(M'⊗Y'⊗N';B)$, quotiented by dinaturality $M,N,M'$ and $N'$. **Promonoidal horizontal structure.** The category of monoidal contexts is promonoidal with the following protensor and prounit. $$𝔹ℂ_{⊗}\left({X \atop Y}, {X' \atop Y'}; {A \atop B} \right) = ∫^{M,N,H} ℂ(A; M⊗X⊗N⊗X'⊗H) × ℂ(M⊗Y⊗N⊗Y'⊗H; B),$$ $$𝔹ℂ_{\otimes}\left( {X \atop Y} \right) = ℂ(X;Y).$$ This is to say that elements of the prounit are again just morphisms; while elements of the protensor are pairs $⟨f {｜ \atop ｜} g⟩$ for some $f ∈ ℂ(A; M⊗X⊗N⊗X'⊗H)$ and some $g ∈ ℂ(M⊗Y⊗N⊗Y'⊗H;B)$, quotiented by dinaturality of all $M,N$ and $H$. **Produoidal structure.** Both promonoidal structures, together, form a normal produoidal category, where the laxator map takes two separate contexts and puts them together, $$⟨ f {｜ h ｜ \atop ｜ k｜} g⟩ ↦ ⟨f {｜ \atop ｜} h ⊗ k {｜ \atop ｜} g⟩.$$  ### See also - [Monoidal contexts form a category](notes/pieces/Monoidal%20contexts%20form%20a%20category.md) - [Produoidal contour](notes/pieces/Produoidal%20contour.md) - [Monoidal spliced arrows](notes/pieces/Monoidal%20spliced%20arrows.md) - [produoidal normalization](notes/pieces/produoidal%20normalization.md) - [Context for context](private-notes/Context%20for%20context.md) - [TallCat Meeting on Monoidal Contexts](private-notes/TallCat%20Meeting%20on%20Monoidal%20Contexts.md) **Tags**: [produoidal category](notes/pieces/produoidal%20category.md), [Duoidal Tambara](notes/pieces/Duoidal%20Tambara.md).