Search

# 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.

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}