# 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
- TallCat Meeting on Monoidal Contexts
- Produoidal contour
- Monoidal spliced arrows
- Normalization of a produoidal

**Tags**:
Produoidal category,
Duoidal Tambara.