Homotopy Type Theory monoid > history (Rev #5, changes)

Homomorphisms of monoids

A homomorphism of monoids between two monoids $A$ and $B$ consists of

• A function $\phi:A \to B$ such that
  • The basepoint is preserved
    $$\phi(e_A) = e_B$$
  • The binary operation is preserved
    $$\prod_{(a:A)} \prod_{(b:A)} \phi(\mu_A(a, b)) = \mu_B(\phi(a),\phi(b))$$

For any monoid $A$, the 0-truncator means that the identity types between any two terms of $A$ 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 $A$ and $B$, 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 $A_3$-spaces. Finally, the 0-truncator is always preserved in a function between two sets.