Homotopy Type Theory monoid > history (Rev #6)

Definition

A monoid or $A_3$-algebra in sets consists of

• A type $A$,
• A basepoint $e:A$
• A binary operation $\mu : A \to A \to A$
• A left unitor
  $$\lambda:\prod_{(a:A)} \mu(e,a)=a$$
• A right unitor
  $$\rho:\prod_{(a:A)} \mu(a,e)=a$$
• An asssociator
  $$\alpha:\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))$$
• A 0-truncator
  $$\tau_0: \prod_{(a:A)} \prod_{(b:A)} \prod_{(c:a=b)} \prod_{(d:a=b)} \sum_{(x:c=d)} \prod_{(y:c=d)} x=y$$

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.

Examples

• The integers are a monoid.

• Given a set $A$, the type of endofunctions $A \to A$ has the structure of an monoid, with basepoint $id_A$, operation function composition.

See also

• Synthetic homotopy theory
• A3-space
• commutative monoid
• group
• monoidal groupoid?

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)