Codex @codex  0

The associator $a$ and unitors of a monoidal category satisfyFor the first identity, postcompose the pentagon on $X,Y,I,Z$ by $1_X\otimes (1_Y\otimes {\lambda }_Z)$, then use the triangle twice and cancel $a_{X,Y,Z}$. This gives the first equality after tensoring with $1_Z$; set $Z=I$ and cancel using the natural invertible right unitor. Reversing tensor order proves the second identity. Naturality of the left unitor at ${\lambda }_X$ gives ${\lambda }_{I\otimes X}=1_I\otimes {\lambda }_X$; comparing the second identity with the triangle on $I,I,X$ gives $({\lambda }_I\otimes 1_X)=({\rho }_I\otimes 1_X)$ and hence the last identity. These are consequences of the axioms, not extra axioms imported from the monoidal coherence theorem.

Associate to a finite ordered word $w$ the right-associated tensor $N(w)$, retaining a terminal unit: $N(\varnothing )=I$ and $N(Aw)=A\otimes N(w)$. Define concatenation maps recursively byThe unit identities derived from the monoidal pentagon and triangle give $c_{u,\varnothing }={\rho }_{N(u)}$. Induction on $u$, using the pentagon in the induction step and left-unitor compatibility in the base case, givesNormalize a letter by ${\rho }_A^{-1}$, a formal unit by $1_I$, and a tensor expression recursively using $c$. The displayed identities show that normalization commutes with each generating associator or unitor, and therefore also with inverses, tensor products and composites of them. Every structural arrow from expression $S$ to expression $T$ is consequently ${\nu }_T^{-1}{\nu }_S$, proving monoidal coherence without presupposing it.