Strictification and Mac Lanes Coherence Theorem

If $f:v\to v^{\mathrm{\prime }}$ and $g:w\to w^{\mathrm{\prime }}$ exist in $W$, then $\mathrm{\mid }v\mathrm{\mid }=\mathrm{\mid }{v}^{\mathrm{\prime }}\mathrm{\mid }$ and $\mathrm{\mid }w\mathrm{\mid }=\mathrm{\mid }{w}^{\mathrm{\prime }}\mathrm{\mid }$, so $\mathrm{\mid }v\mathrm{\square }w\mathrm{\mid }=\mathrm{\mid }{v}^{\mathrm{\prime }}\mathrm{\square }{w}^{\mathrm{\prime }}\mathrm{\mid }$. Define $f\otimes g$ to be the unique morphism $v\mathrm{\square }w\to v^{\mathrm{\prime }}\mathrm{\square }{w}^{\mathrm{\prime }}$. Because all such morphisms are unique when they exist, this tensor preserves identities and composition automatically.

For words $u,v,w$, the source and target of $((u\mathrm{\square }v)\mathrm{\square }w)⟶u\mathrm{\square }(v\mathrm{\square }w),e_0\mathrm{\square }u⟶u,u\mathrm{\square }{e}_0⟶u$ have the same lengths, so [L1] gives unique arrows ${\alpha }_{u,v,w}$, ${\lambda }_u$, and ${\rho }_u$. Their reverse arrows also exist uniquely, so these are isomorphisms.

The two sides of the pentagon are morphisms in $W$ from one fourfold word to another of length $\mathrm{\mid }u\mathrm{\mid }+\mathrm{\mid }v\mathrm{\mid }+\mathrm{\mid }w\mathrm{\mid }+\mathrm{\mid }z\mathrm{\mid }$. By [L1] there is only one such morphism, so the pentagon commutes. The same uniqueness argument gives the triangle identity.

Steps 1.1-2.1 supply exactly the data required in [L2], so $W$ is monoidal.

For objects $(F,c)$ and $(G,d)$ of ${\mathcal{C}}^{\mathrm{\prime }}$, define $(F,c)\otimes (G,d):=(FG,e)$ with $e_{X,Y}:=F(d_{X,Y})\circ c_{G(X),Y}$. The axioms from [L1] for $c$ and $d$ imply the same associativity and unit equations for $e$, so $(FG,e)$ is again an object of ${\mathcal{C}}^{\mathrm{\prime }}$. For morphisms $\theta :(F,c)\Rightarrow (F^{\mathrm{\prime }},c^{\mathrm{\prime }})$ and $\eta :(G,d)\Rightarrow (G^{\mathrm{\prime }},d^{\mathrm{\prime }})$, define $(\theta \otimes \eta {)}_X:={\theta }_{G^{\mathrm{\prime }}(X)}\circ F({\eta }_X)=F^{\mathrm{\prime }}({\eta }_X)\circ {\theta }_{G(X)}$. The equality is naturality, and the module-compatibility equation follows from the corresponding equations for $\theta$ and $\eta$.

Let $\mathbf{I}$ be the identity functor on $\mathcal{C}$ with structure map $i_{X,Y}=1_{X\otimes Y}$. Then $(\mathbf{I},i)$ is an object of ${\mathcal{C}}^{\mathrm{\prime }}$ and acts as a two-sided unit for the tensor just defined.

Composition of endofunctors is literally associative and unital, so $((F\otimes G)\otimes H)=FGH=F\otimes (G\otimes H)$ and $\mathbf{I}\otimes F=F=F\otimes \mathbf{I}$ as equalities of objects. The induced structure maps agree term by term from the definition in step 1.1, so the associator and unitors are identities.

Step 2.1 verifies the strictness clause of [L2], so ${\mathcal{C}}^{\mathrm{\prime }}$ is strict monoidal under composition.

For each object $X$ of $\mathcal{C}$, put $L(X)=(X\otimes -,{\alpha }_{X,-,-})$. The pentagon and triangle axioms of $\mathcal{C}$ are exactly the coherence and unit equations required in [L1], so $L(X)$ is an object of ${\mathcal{C}}^{\mathrm{\prime }}$. For a morphism $f:X\to Y$, define $L(f{)}_Z=f\otimes 1_Z$. Naturality of the associator shows that $L(f)$ is a morphism in ${\mathcal{C}}^{\mathrm{\prime }}$.

The functor $L$ is split essentially surjective. For an object $(F,c)$ of ${\mathcal{C}}^{\mathrm{\prime }}$, let $X:=F(\mathbf{1})$ and define ${\varphi }_Y:=F({\lambda }_Y)\circ c_{\mathbf{1},Y}:X\otimes Y\to F(Y)$. Each ${\varphi }_Y$ is an isomorphism because both factors are, and naturality of $c$ together with its coherence equations makes $\varphi :L(X)\Rightarrow (F,c)$ a morphism in ${\mathcal{C}}^{\mathrm{\prime }}$.

The unit comparison for $L$ is the natural isomorphism $(L_0{)}_Z={\lambda }_Z^{-1}:Z\to \mathbf{1}\otimes Z$, and the binary comparison $L_2(X,Y):L(X)\otimes L(Y)\Rightarrow L(X\otimes Y)$ has component ${\alpha }_{X,Y,Z}^{-1}:X\otimes (Y\otimes Z)\to (X\otimes Y)\otimes Z$. The same pentagon and triangle identities show these are morphisms in ${\mathcal{C}}^{\mathrm{\prime }}$, so $L$ is strong monoidal into the strict monoidal target of [L2].

The functor $L$ is faithful. If $L(f)=L(g)$, then their components at the unit object agree, and composing with the right unitors gives $f={\rho }_Y\circ L(f{)}_{\mathbf{1}}\circ {\rho }_X^{-1}={\rho }_Y\circ L(g{)}_{\mathbf{1}}\circ {\rho }_X^{-1}=g$.

The functor $L$ is full. Given a morphism $\theta :L(X)\Rightarrow L(Y)$ in ${\mathcal{C}}^{\mathrm{\prime }}$, define $f={\rho }_Y\circ {\theta }_{\mathbf{1}}\circ {\rho }_X^{-1}:X\to Y$. The compatibility equation from [L1], evaluated at $(\mathbf{1},Z)$, identifies ${\theta }_Z$ with $f\otimes 1_Z$ after the unitors are inserted, so $\theta =L(f)$.

By steps 2.2-3.1 and [L4], the underlying functor of $L$ is an equivalence of categories. By [L5], choose an adjoint-equivalence quasi-inverse $G:{\mathcal{C}}^{\mathrm{\prime }}\to \mathcal{C}$ with natural isomorphisms $\eta :1_{\mathcal{C}}\Rightarrow GL$ and $\epsilon :LG\Rightarrow 1_{{\mathcal{C}}^{\mathrm{\prime }}}$.

Use full faithfulness of $L$ to define the binary comparison $G_2(A,B):G(A)\otimes G(B)\to G(A\otimes B)$ as the unique morphism whose image under $L$ is ${\epsilon }_{A\otimes B}^{-1}\circ ({\epsilon }_A\otimes {\epsilon }_B)\circ L_2(GA,GB{)}^{-1}\mathrm{.}$ Define $G_0:{\mathbf{1}}_{\mathcal{C}}\to G({\mathbf{1}}_{{\mathcal{C}}^{\mathrm{\prime }}})$ uniquely by $L(G_0)={\epsilon }_{{\mathbf{1}}_{{\mathcal{C}}^{\mathrm{\prime }}}}^{-1}\circ L_0^{-1}\mathrm{.}$ Naturality of $\epsilon$ and $L_2$ makes the displayed images natural in $A,B$, so faithfulness of $L$ makes $G_2$ natural. Both comparisons are isomorphisms by [L6].

Apply the faithful functor $L$ to the associativity and unit diagrams for $G_2,G_0$. By their defining formulas, the images reduce to the coherence diagrams for the strong monoidal functor $L$ together with naturality of $\epsilon$, so they commute. Thus $G$ is strong monoidal, and the defining equations in step 5.1 say exactly that $\epsilon$ is monoidal. The triangle identity $\epsilon L\circ L\eta =1_L$ gives $L\eta =(\epsilon L{)}^{-1}$; since the inverse of a monoidal natural isomorphism is monoidal, faithfulness of $L$ then verifies the binary and unit equations for $\eta$. Hence $\eta$ is monoidal. The data $(L,G,\eta ,\epsilon )$ therefore satisfy [L3], so $L$ is a monoidal equivalence to the strict monoidal category ${\mathcal{C}}^{\mathrm{\prime }}$.

Because $F$ is strong monoidal, applying $F$ to any generator listed in [L1] and then using the structure isomorphisms of $F$ again yields a canonical morphism in $\mathcal{D}$ between the corresponding parenthesised tensor words in the images of the objects. Therefore $F$ sends canonical composites in $\mathcal{C}$ to canonical composites in $\mathcal{D}$.

In the strict target $\mathcal{D}$, [L4] makes every canonical morphism between the same source and target the identity of the common tensor object. Hence the images under $F$ of any two canonical morphisms in $\mathcal{C}$ with the same source and target are equal.

By [L2] and [L3], the underlying functor of $F$ is faithful. So equality after applying $F$ implies equality before applying $F$. Therefore any two canonical morphisms in $\mathcal{C}$ with the same source and target are equal.

For a consecutive block $x_i,\dots ,x_{i+m-1}$, let $r_{i,0}:=\mathbf{1}$, $r_{i,1}:=x_i$, and, for $m\ge 1$, let $r_{i,m+1}:=(r_{i,m}\otimes x_{i+m})$. We claim that every parenthesised tensor word $w$ whose ordered letters are exactly this block admits a canonical natural isomorphism ${\kappa }_w:E_w\Rightarrow E_{r_{i,m}}$.

The claim is proved recursively. For a word containing no letters, repeated unitors give a canonical map to $r_{i,0}=\mathbf{1}$; for a one-letter word, repeated unitors give a canonical map to that actual letter $r_{i,1}=x_i$. For $w=(a\otimes b)$, suppose $a$ contains the first $p$ letters $x_i,\dots ,x_{i+p-1}$ and $b$ contains the next $q$ letters $x_{i+p},\dots ,x_{i+p+q-1}$. Recursion gives ${\kappa }_a:E_a\Rightarrow E_{r_{i,p}}$ and ${\kappa }_b:E_b\Rightarrow E_{r_{i+p,q}}$. Their tensor is canonical, and repeated associators and unitors give a canonical isomorphism $E_{r_{i,p}\otimes r_{i+p,q}}\Rightarrow E_{r_{i,p+q}}$. The composite is ${\kappa }_w$, and every step uses only the generators allowed in [L1].

For the given words $u$ and $v$, define ${\theta }_{u,v}:={\kappa }_v^{-1}\circ {\kappa }_u:E_u\Rightarrow E_v$. This is a canonical natural isomorphism.

By [L2], the ambient monoidal category is equivalent to a strict one, so [L3] applies. Hence any two canonical morphisms from $u$ to $v$ are equal. Since step 3.1 produced one such morphism, it is the unique canonical natural isomorphism $E_u\Rightarrow E_v$.

For $n=0$, interpret the empty tensor string as the unit object; for $n=1$, as $A_1$; and for $n\ge 2$, choose any parenthesised tensor word $w$ on the letters $x_1,\dots ,x_n$ and evaluate it at $(A_1,\dots ,A_n)$.

If $w^{\mathrm{\prime }}$ is another such parenthesisation, [L2] gives a unique canonical natural isomorphism $w\Rightarrow w^{\mathrm{\prime }}$, and evaluating at $(A_1,\dots ,A_n)$ yields a unique canonical isomorphism between the two resulting objects of $\mathcal{C}$.

Therefore suppressing brackets does not change the resulting tensor object except by a unique canonical identification. This discharges the warning of [L1]: after coherence, the notation $A_1\otimes \cdots \otimes A_n$ is well defined.

Choose a strictification of $\mathcal{C}$ as in [L2]. Applying the strong monoidal functor of that equivalence to the diagrams from [L1] transports the monoid-object structure of $M$ to a monoid-object structure on its image in a strict monoidal category.

In the strict target, the associator and unitors are identities, so the transported axioms become exactly the displayed unbracketed equalities.

By [L3], those unbracketed composites denote definite maps back in the original category and do not depend on which brackets were suppressed. Hence the monoid-object axioms may be written in the simplified form without changing their content.

Define $T_b$ recursively on objects by $T_b(e_0)={\mathbf{1}}_{\mathcal{B}}$, $T_b((-))=b$, and $T_b(v\mathrm{\square }w)=T_b(v)\otimes T_b(w)$. If $u:v\to w$ is the unique morphism of $W$, then $v$ and $w$ have the same length, so [L4] gives a unique canonical isomorphism $T_b(v)\to T_b(w)$; define $T_b(u)$ to be that morphism. Because identities and composites in $W$ are themselves the unique arrows between equal-length words, uniqueness in [L4] makes $T_b$ a functor.

The recursive object formula already matches the tensor and unit of $W$, and the same canonical comparison maps from [L4] provide the invertible structural maps required by [L3]. Thus $T_b$ is a strong monoidal functor.

Let $S:W\to \mathcal{B}$ be another strong monoidal functor with $S((-))=b$. Build isomorphisms ${\sigma }_v:S(v)\to T_b(v)$ recursively: for $e_0$, use the inverse of the unit map of $S$; for $(-)$, use $1_b$; and for $v\mathrm{\square }w$, use the inverse of the binary structure isomorphism of $S$ followed by ${\sigma }_v\otimes {\sigma }_w$.

Since every morphism in $W$ is unique when it exists, the family ${\sigma }_v$ is automatically natural, and the same recursion forces compatibility with the monoidal structure maps. Uniqueness of the recursion makes $\sigma :S\Rightarrow T_b$ the unique monoidal natural isomorphism fixing the generator.

Because $v$ and $w$ have the same length, [L1] gives a unique arrow $u_{v,w}:v\to w$ in $W$.

By [L2], the image $T_b(u_{v,w})$ is exactly the canonical comparison isomorphism between the two parenthesised tensor powers represented by $v$ and $w$.

Therefore the unique formal arrow of $W$ between $v$ and $w$ is carried by evaluation to the canonical comparison map between the corresponding tensor powers of $b$. This is precisely the canonical-map formulation in the one-generator setting.

Thus the free-word presentation recovers the canonical-map presentation of coherence for tensor powers of one chosen object.

Let $A=\{0,1\}$ in the cartesian monoidal category of sets supplied by [L2], and let $c:A\to A$ be the constant-zero map. Consider the square with all four vertices $A$, top edge $c$, and the other three edges $1_A$.

The composite along the top and right edges is $c$, while the composite along the left and bottom edges is $1_A$. These maps differ because $c(1)=0\mathrm{\ne }1=1_A(1)$, so the square does not commute.

This noncanonical square lies outside the scope described in [L1] and is a diagram in a monoidal category that does not commute. Therefore the claim is false.

Suppose a strict monoidal isomorphism $F:\mathbf{S}\mathbf{e}\mathbf{t}\to \mathcal{D}$ existed with $\mathcal{D}$ strict. Strict preservation and strict associativity in $\mathcal{D}$ would give $F((A\times B)\times C)=(F(A)\otimes F(B))\otimes F(C)=F(A)\otimes (F(B)\otimes F(C))=F(A\times (B\times C))\mathrm{.}$ Since $F$ is injective on objects, this would force $(A\times B)\times C=A\times (B\times C)$ as literal sets for all $A,B,C$.

For nonempty sets under the usual ordered-pair construction, these two nested cartesian products are not literally equal: their elements have different bracketed pair shapes. This contradicts step 1.1.

Thus cartesian $\mathbf{S}\mathbf{e}\mathbf{t}$ is not strictly monoidally isomorphic to a strict monoidal category, even though [L1] supplies a monoidal equivalence to one. Therefore the claim is false.

By [L1], adding the word "skeletal" strengthens the strictification target by requiring equality of all isomorphic objects there.

But [L2] states that this stronger simultaneous requirement can fail even though ordinary strictification succeeds.

Hence the claim is false.

If the claim were true, the theorem would identify every parallel pair in the category, with no restriction on how those morphisms were built.

That contradicts [L1], which records the theorem's actual quantifiers and restricts it to canonical structural morphisms.

Therefore the claim is false.

If strictification itself required choice, then the theorem's own construction would already depend on selecting representatives.

But [L1] states that the selection occurs only in the stronger skeletal refinement, not in strictification itself.

Therefore the claim is false.