A homomorphism of monoids between two monoids and consists of
A function such that
The basepoint is preserved
The binary operation is preserved
For any monoid , the 0-truncator means that the identity types between any two terms of are propositions, and thus the dependent product types
are propositions, and thus contractible because they are inhabited by definition of a monoid.
As a result, given monoids and , for any function
the left unitor is preserved:
because
is contractible. Likewise, for any function
the right unitor is preserved:
because
is contractible, and for any function
the associator is preserved:
because
is contractible. This means that a homomorphism of monoids is also a homomorphism of -spaces. Finally, the 0-truncator is always preserved in a function between two sets.