MacLane’s coherence theorem and free monoidal categories Original question
The nLab gives one formulation of the coherence theorem for monoidal categories:

Every diagram in a free monoidal category made up of associators and unitors commutes.

It seems to me in practice this coherence theorem is often used as follows:
One has a diagram on a set of objects $S$ of a specific monoidal category $(C,\otimes,I)$ made up from the associators and unitors of $C$. One then considers this diagram "in the free monoidal category on $S$." Subsequently, one argues that since the diagram in the free monoidal category commutes, so does the original diagram.
How do you make this sketch of an argument precise? I tried using the universal property of „the free monoidal category“ – to no avail.
Edit:
In his answer Jonas suggested that any monoidal category is the quotient of a free monoidal category. Is this true? In the context of group theory this is easily proved using the universal property of the free group and the first isomorphism theorem for groups. Does an analogue of the isomorphism theorem hold for (monoidal) categories?
 A: The free monoidal category $\mathbb M A$ on a set $A$ has the following universal property. For every monoidal category $\mathbf C$ and function $f \colon A \to |\mathbf C|$, there is a unique monoidal functor $\tilde f \colon \mathbb M A \to \mathbf C$ such that $\tilde f \circ \eta_A = f$, where $\eta_A \colon A \to \mathbb M A$ is the inclusion (concretely, $\mathbb M A$ has as its objects lists of objects in $A$, and $\eta_A$ sends $a \mapsto [a]$).
A diagram in the free monoidal category on $A$ is simply a pair of morphisms $\ell, r \colon x \to y$ in $\mathbb M A$. Conceptually, these are built inductively from the structural isomorphisms $\alpha$, $\lambda$, and $\rho$.
A formal diagram in a monoidal category $\mathbf A$ is simply a diagram in $\mathbb M(|\mathbf A|)$. We have a canonical functor $\mathbb M(|\mathbf A|) \to \mathbf A$ given by the universal property of the free monoidal category. Therefore, a formal diagram in $\mathbf A$ is sent to a pair of morphisms in $\mathbf A$. Since the morphisms in the free monoidal category were constructed inductively from structural isomorphisms, so will be the morphisms in $\mathbf A$ in the image of the functor.
However, the coherence theorem says that necessarily that for any diagram $\ell, r$ in the free monoidal category, we have $\ell = r$. Since functors preserve equality of morphisms, the functor $\mathbb M(|\mathbf A|) \to \mathbf A$ sends any diagram to an equal pair of morphisms in $\mathbf A$. Therefore any formal diagram in $\mathbf A$ commutes.
A: Without looking into my notes I am not 100% sure how the universal property of a free monoidal category actually looks like (is it the free monoidal category on a graph? Or the free monoidal category on a category with distinguished unit object? Do you consider strict or strong monoidal functors?). Anyway the result will be that any monoidal category is a (probably 2-categorical) colimit of a free one. So if you have a diagram in a monoidal category $\mathscr{C}$, it will be represented by a diagram in the free monoidal category, of which $\mathscr{C}$ is a quotient. If the representing diagram commutes, by functoriality of the quotient functor the original diagram commutes. In fact in practice one often only proves commutativity of diagrams in free monoidal categories, since in a non-free monoidal category $\mathscr{C}$ there might be unwanted coherences (e.g. some maps suddenly being an identity morphism), which could possibly falsify the argument.
I know that this answer is probably unsatisfying, but the problem is that (to my knowledge) proving the existence of free monoidal categories is actually not that easy. This is essentially the case since colimits of categories are hard to compute.
