A version of Mac Lane's Coherence Theorem states that every formal diagram (i.e., a diagram that involves only the associativity isomorphism, the unit isomorphisms, their inverses, identity morphisms, the monoidal product, and composites) commute.
From this version, how to deduce the other version that states that every monoidal category can be strictified via an adjoint equivalence consisting of strong monoidal functors?
I believe that the opposite question has already been answered by jgon. However, I cannot find in the literature the direction of interest to me. And I'm afraid I have no clue.