Mac Lane strictification

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 }}$.