Normalization of a produoidal

Last updated Feb 3, 2024

Normal produoidal categories are the profunctorial analogue of normal duoidal categories. Produoidal normalization is analogue to duoidal normalization.

See also.

• Unit of the normalization monad
• Multiplication of the normalization monad
• Algebras of normalization are normal produoidals

We define the following multiplication and unit for the promonad, $𝓝𝕍$. They are constructed out of laxators of the produoidal category $𝕍$ and Yoneda isomorphisms; thus, they must be associative and unital by coherence. The unit is defined by $$\begin{aligned} & 𝕍(A; B) \ \cong & \quad\mbox{(by unitality of $𝕍$)} \ & 𝕍(A; I \otimes B \otimes I) \ \to & \quad\mbox{(by the laxators of $𝕍$)} \ & 𝕍(A; N \otimes B \otimes N) \ = & \quad\mbox{(by definition)} \ & 𝓝𝕍(A; B). \ \end{aligned}$$

The multiplication is defined by, $$\begin{aligned} & ∫^{B ∈ 𝕍} 𝓝𝕍(A; B) × 𝓝𝕍(B; C) \ = & \quad\mbox{(by definition)} \ & ∫^{B ∈ 𝕍} 𝕍(A; N ⊗ B ⊗ N) × 𝕍(B; N ⊗ C ⊗ N) \ ≅ & \quad\mbox{(by Yoneda lemma)} \ & 𝕍(A; N ⊗ N ⊗ C ⊗ N ⊗ N) \phantom{\int}\ → & \quad\mbox{(by laxators of $𝕍$)} \ & 𝕍(A; N ⊗ C ⊗ N) \phantom{\int}\ = & \quad\mbox{(by definition)} \ & 𝓝𝕍(A;C). \phantom{\int}\ \end{aligned}$$

Let us now construct the unitors and the associators. Again, they are constructed out of laxators of the produoidal category $𝕍$, the associators and unitors of $𝕍$, and Yoneda isomorphisms. We first consider the right unitor. $$\begin{aligned} & ∫^{X ∈ ℕ𝕍} ℕ𝕍(A; B ⊗ X) × ℕ𝕍(X; N) \ = & \quad\mbox{(by definition)} \ & ∫^{X ∈ ℕ𝕍} 𝕍(A; N ⊗ B ⊗ N ⊗ X ⊗ N) × ℕ𝕍(X; N) \ = & \quad\mbox{(by associativity of $𝕍$)} \ & ∫^{X ∈ ℕ𝕍, P ∈ 𝕍} 𝕍(A; N ⊗ B ⊗ P) × 𝕍(P; N ⊗ X ⊗ N) × ℕ𝕍(X; N) \ = & \quad\mbox{(by definition)} \ & ∫^{X ∈ ℕ𝕍, P ∈ 𝕍} 𝕍(A; N ⊗ B ⊗ P) × ℕ𝕍(P;X) × ℕ𝕍(X; N) \ = & \quad\mbox{(by Yoneda)} \ & ∫^{P ∈ 𝕍} 𝕍(A; N ⊗ B ⊗ P) × ℕ𝕍(P; N) \ = & \quad\mbox{(by definition)} \ & ∫^{P ∈ 𝕍} 𝕍(A; N ⊗ B ⊗ P) × 𝕍(P; N) \ = & \quad\mbox{(by unitality)} \ & ∫^{P ∈ 𝕍} 𝕍(A; N ⊗ B ⊗ N). \ \end{aligned}$$ We now consider the left unitor. $$\begin{aligned} & ∫^{X ∈ ℕ𝕍} ℕ𝕍(A; X ⊗ B) × ℕ𝕍(X; N) \ = & \quad\mbox{(by definition)} \ & ∫^{X ∈ ℕ𝕍} 𝕍(A; N ⊗ X ⊗ N ⊗ B ⊗ N) × ℕ𝕍(X; N) \ = & \quad\mbox{(by associativity of $𝕍$)} \ & ∫^{X ∈ ℕ𝕍, P ∈ 𝕍} 𝕍(A; P ⊗ B ⊗ N) × 𝕍(P; N ⊗ X ⊗ N) × ℕ𝕍(X; N) \ = & \quad\mbox{(by definition)} \ & ∫^{X ∈ ℕ𝕍, P ∈ 𝕍} 𝕍(A; P ⊗ B ⊗ N) × ℕ𝕍(P;X) × ℕ𝕍(X; N) \ = & \quad\mbox{(by Yoneda)} \ & ∫^{P ∈ 𝕍} 𝕍(A; P ⊗ B ⊗ N) × ℕ𝕍(P; N) \ = & \quad\mbox{(by definition)} \ & ∫^{P ∈ 𝕍} 𝕍(A; P ⊗ B ⊗ N) × 𝕍(P; N) \ = & \quad\mbox{(by unitality)} \ & ∫^{P ∈ 𝕍} 𝕍(A; N ⊗ B ⊗ N). \ \end{aligned}$$ Finally, we consider the associator. We can do so in two steps, showing that both sides of the equation $$∫^{X ∈ ℕ𝕍} ℕ𝕍(A; B ⊗ X) × ℕ𝕍(X; C ⊗ D) ≅ ∫^{Y ∈ ℕ𝕍} ℕ𝕍(A; Y ⊗ D) × ℕ𝕍(Y; B ⊗ C)$$ are isomorphic to $𝕍(A; N ⊗ B ⊗ N ⊗ C ⊗ N ⊗ D ⊗ N)$. The first side by $$\begin{aligned} & ∫^{X ∈ ℕ𝕍} ℕ𝕍(A; B ⊗ X) × ℕ𝕍(X; C ⊗ D) \\ = & \quad\mbox{(by definition)} \\ & ∫^{X ∈ ℕ𝕍} 𝕍(A; N ⊗ B ⊗ N ⊗ X ⊗ N) × ℕ𝕍(X; C ⊗ D) \\ = & \quad\mbox{(by associativity)} \\ & ∫^{X ∈ ℕ𝕍, P ∈ 𝕍} 𝕍(A; N ⊗ B ⊗ P) × 𝕍(P; N ⊗ X ⊗ N) × ℕ𝕍(X; C ⊗ D) \\ = & \quad\mbox{(by definition)} \\ & ∫^{X ∈ ℕ𝕍, P ∈ 𝕍} 𝕍(A; N ⊗ B ⊗ P) × ℕ𝕍(P; X) × ℕ𝕍(X; C ⊗ D) \\ = & \quad\mbox{(by Yoneda)} \\ & ∫^{P ∈ 𝕍} 𝕍(A; N ⊗ B ⊗ P) × ℕ𝕍(P; C ⊗ D) \\ = & \quad\mbox{(by definition)} \\ & ∫^{P ∈ 𝕍} 𝕍(A; N ⊗ B ⊗ P) × 𝕍(P; N ⊗ C ⊗ N ⊗ D ⊗ N) \\ = & \quad\mbox{(by associativity)} \\ & 𝕍(A; N ⊗ B ⊗ N ⊗ C ⊗ N ⊗ D ⊗ N), \\ \end{aligned}$$ and the second side by $$\begin{aligned} & ∫^{Y ∈ ℕ𝕍} ℕ𝕍(A; Y ⊗ D) × ℕ𝕍(Y; B ⊗ C) \\ = & \quad\mbox{(by definition)} \\ & ∫^{Y ∈ ℕ𝕍} 𝕍(A; N ⊗ Y ⊗ N ⊗ D ⊗ N) × ℕ𝕍(Y; B ⊗ C) \\ = & \quad\mbox{(by associativity)} \\ & ∫^{Y ∈ ℕ𝕍, P ∈ 𝕍} 𝕍(A; P ⊗ D ⊗ N) × 𝕍(P; N ⊗ Y ⊗ N) × ℕ𝕍(Y; B ⊗ C) \\ = & \quad\mbox{(by definition)} \\ & ∫^{Y ∈ ℕ𝕍, P ∈ 𝕍} 𝕍(A; P ⊗ D ⊗ N) × ℕ𝕍(P; X) × ℕ𝕍(X; B ⊗ C) \\ = & \quad\mbox{(by Yoneda)} \\ & ∫^{P ∈ 𝕍} 𝕍(A; P ⊗ D ⊗ N) × ℕ𝕍(P; B ⊗ C) \\ = & \quad\mbox{(by definition)} \\ & ∫^{P ∈ 𝕍} 𝕍(A; P ⊗ D ⊗ N) × 𝕍(P; N ⊗ B ⊗ N ⊗ C ⊗ N) \\ = & \quad\mbox{(by associativity)} \\ & 𝕍(A; N ⊗ B ⊗ N ⊗ C ⊗ N ⊗ D ⊗ N). \\ \end{aligned}$$

Tags: produoidal category, duoidal normalization, Monoidal contexts, Symmetric normalization of a produoidal.