We’ve got free and forgetful functors Define Given a category the category has
- binary trees with labeled leaves as objects and
- binary trees with labeled leaves together with the natural isomorphisms from the definition of a weakly monoidal category as its morphisms.
The multiplication collapses two layers of trees down to one. The unit gives a one-leaf tree.
An algebra of the monad is a category together with a functor such that and Define
Then the associator should be a morphism
However, it isn’t immediately evident that the associator that comes from does the job, since just applying to gives
for the source instead of
which we get by replacing with its definition above. We need an isomorphism
so we can define Now we use the equations an algebra has to satisfy to derive this isomorphism. Since the following two objects are equal:
Therefore, the isomorphism we wanted is simply equality and It also means that satisfies the pentagon equation.
A similar derivation works for the unitors and the triangle equation.
A morphism of algebras is a functor such that Now
so we have the coherence laws for a strict monoidal functor.
so it preserves the associator as well. The unitors follow in the same way, so morphisms of these algebras are strict monoidal functors that preserve the associator and unitors.