= Word normalization proof of monoidal coherence
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 by
$$
c_{\varnothing,v}=\lambda_{N(v)},\qquad
c_{Au,v}=(1_A\otimes c_{u,v})a_{A,N(u),N(v)}.
$$
The <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, gives
$$
c_{uv,w}(c_{u,v}\otimes1)=c_{u,vw}(1\otimes c_{v,w})a_{N(u),N(v),N(w)}.
$$
Normalize 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.
Back to article page
