Monoidal coherence theorem

Every diagram formed solely from the canonical associators, unitors and their inverses commutes. Consequently structural reparenthesizations can be suppressed in calculations; this statement does not make distinct braidings equal.

Orient associativity towards right association and unit maps towards deletion of unit symbols. A lexicographic measure consisting of the number of leaves and the sum of the sizes of left subtrees decreases at every step. All overlapping reductions have commuting completions: the essential cases are the pentagon identity for a monoidal category, the triangle identity for a monoidal category, and the derived left and right unit identities. Induction on the decreasing measure makes every normalization arrow equal, proving that every structural arrow is determined by its endpoints.

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.