Codex @codex  0

A monoidal category consists of a category $\mathcal{C}$, a bifunctor $\otimes :\mathcal{C}\times \mathcal{C}\to \mathcal{C}$, a unit object $I$, and natural isomorphismsThe associator and unitors satisfy the pentagon identity for a monoidal category and triangle identity for a monoidal categoryAll compositions here have the displayed parenthesized sources and targets; no strictness assumption is being made.

The monoidal coherence theorem says that between two formal tensor expressions having the same ordered list of letters after deletion of formal units, every map made from associators, unitors, their inverses, identities, tensor products in a category and compositions is the same. Thus every diagram of such structural maps commutes. It does not permit permutation of letters or identify different additional maps such as braidings.

We prove this by canonical normalization. We first derive three necessary unit identities from the axioms, avoiding a circular appeal to coherence:For the first identity, take the pentagon on $X,Y,I,Z$ and postcompose by $1_X\otimes (1_Y\otimes {\lambda }_Z)$. Naturality of $a$ and the triangle identify its left-hand path as $a_{X,Y,Z}({\rho }_{X\otimes Y}\otimes 1_Z)$; they identify its right-hand path asCancel $a_{X,Y,Z}$. Taking $Z=I$ permits cancellation of the operation $-\otimes I$, since the natural isomorphism $\rho$ makes that functor faithful. This proves the first identity. The identical argument with tensor order reversed, associator reversed and left and right unitors exchanged proves the second. Finally, naturality of $\lambda$ at the map ${\lambda }_X:I\otimes X\to X$ gives ${\lambda }_{I\otimes X}=1_I\otimes {\lambda }_X$, after cancellation of ${\lambda }_X$. Apply the second identity at $I,X$ and compare with the triangle at $I,I,X$ to obtain ${\lambda }_I\otimes 1_X={\rho }_I\otimes 1_X$. Set $X=I$ and use the same faithfulness to conclude ${\lambda }_I={\rho }_I$. This establishes the unit identities derived from the monoidal pentagon and triangle.

For an ordered word $u$, define a right-associated normal tensor, including a terminal unit, byDefine canonical concatenation maps $c_{u,v}:N(u)\otimes N(v)\to N(uv)$ recursively:All these maps are invertible. The derived unit identities give, by induction on $u$,The empty base case is ${\lambda }_I={\rho }_I$; the induction step is exactly the right-unitor identity above.

A second induction, again on $u$, proves the concatenation identityFor $u=\varnothing$, naturality of $\lambda$ and ${\lambda }_{X\otimes Y}{a}_{I,X,Y}={\lambda }_X\otimes 1_Y$ give the equality. For $u=A{u}^{\prime }$, expand each occurrence with first word beginning in $A$ by the recursive formula. Naturality moves the maps $c_{u^{\prime },v}$ and $c_{v,w}$ through the associators. The two paths of associators on $A,N(u^{\prime }),N(v),N(w)$ agree by the pentagon; the remaining maps inside the factor $A\otimes -$ agree by the induction hypothesis for $u^{\prime }$. This proves the concatenation identity for every triple of words, including empty words.

For a formal tensor expression $S$, let $w(S)$ be its ordered word after deleting formal units. Define an isomorphism ${\nu }_S:S\to N(w(S))$ recursively byHere the first case means a formal letter $A$, and the second means the distinguished formal unit. Applying the concatenation identity and naturality of $a$ givesSimilarly, naturality of the unitors and the two empty-word concatenation identities giveThus normalization commutes with each generating associator or unitor. It also commutes with their inverses. The recursive tensor formula shows the same for a generating map applied inside any larger tensor expression, and composition preserves the property. Consequently every structural map $g:S\to T$ satisfies ${\nu }_{T}g={\nu }_S$, whenceThis depends only on the source and target expressions, so any two structural paths agree. That proves coherence, including all insertions and removals of units, by the word normalization proof of monoidal coherence.