Monoidal contexts
# Monoidal contexts
Definition. Let $(ℂ,⊗,I)$ be a monoidal category. The category of monoidal contexts has objects the pairs of objects of $ℂ$ and morphisms $$𝔹ℂ\left({X \atop Y}, {A \atop B}\right) = ∫^{M,N} ℂ(A; M⊗X⊗N) × ℂ(M⊗Y⊗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 ∈ ℂ(A; M⊗X⊗N)$ and some $g ∈ ℂ(M⊗Y⊗N;B)$. These are pairs quotiented by the equivalence relation generated by dinaturality on $M$ and $N$, $$⟨f⨾(m⊗ id_X ⊗n⟩ ｜ g⟩ = ⟨f ｜ (m ⊗ id_Y ⊗ n) ⨾ g⟩.$$ Composition is defined as follows; identities are pairs of identities. $$⟨f｜g⟩ ⨾ ⟨f’｜g’⟩ = ⟨f ⨾ (id_M⊗f’⊗id_N)｜(id_M⊗g’⊗id_N)⨾g⟩,$$ $$id_{\left({A \atop B}\right)} = ⟨id_A ｜ id_B⟩.$$
# Promonoidal structures
Promonoidal vertical 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) = ∫^{Z} 𝔹ℂ \left( {X \atop Y}; {A \atop Z}\right) × 𝔹ℂ\left( {X’ \atop Y’}; {Z \atop B} \right); \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
- Produoidal contour
- Monoidal spliced arrows
- produoidal normalization
- Context for context
- TallCat Meeting on Monoidal Contexts
Tags: produoidal category, Duoidal Tambara.