Showing changes from revision #11 to #12: Added | Removed | Changed

Contents

Definition

A monoid consists of

• A type $A$,
• A basepoint $e:A$
• A binary operation $\mu : A \to A \to A$
• A contractible left unit identity
  $$c_\lambda:\prod_{(a:G)} isContr(\mu(e,a)=a)$$
• A contractible right unit identity
  $$c_\rho:\prod_{(a:G)} isContr(\mu(a,e)=a)$$
• A contractible associative identity
  $$c_\alpha:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} isContr(\mu(\mu(a, b),c)=\mu(a,\mu(b,c)))$$
• A 0-truncator
  $$\tau_0: \prod_{(a:A)} \prod_{(b:A)} isProp(a=b)$$

Properties

Monoid homomorphisms

A monoid homomorphism 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 function

the contractible left unit identity is preserved:

because

is contractible. Likewise, for any function

the contractible right unit identity is preserved:

because

is contractible, and for any function

the contractible associative identity is preserved:

because

is contractible. Finally, the 0-truncator is always preserved in a function between two sets.

Monoid isomorphisms

A monoid isomorphism between two monoids $A$ and $B$ consists of

• a monoid homomorphism $f: A \to B$
• a monoid homomorphism $f^{-1}: B \to A$ that is an inverse function of $f$.

Structure identity principle for monoids

(…)

Relation to $A_3$-spaces

Since for all $a, b, c:A$, $\mu(e,a)=a$, $\mu(a,e)=a$, and $\mu(\mu(a, b),c)=\mu(a,\mu(b,c))$ are contractible, the types

$$\prod_{(a:A)} \mu(e,a)=a$$

$$\prod_{(a:A)} \mu(a,e)=a$$

$$\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))$$

are contractible and thus pointed, and thus one could choose any point

$$\lambda:\prod_{(a:A)} \mu(e,a)=a$$

$$\rho:\prod_{(a:A)} \mu(a,e)=a$$

$$\alpha:\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))$$

to be the left unitor, right unitor, and associator respectively, which means that a monoid is an $A_3$-space.

Similarly, any 0-truncated $A_3$-space or $A_3$-algebra in sets is a monoid, as any identity type between any two terms of a set are propositions, and thus for every $a, b, c:A$, the identity types $\mu(e,a)=a$, $\mu(a,e)=a$, and $\mu(\mu(a, b),c)=\mu(a,\mu(b,c))$ are propositions. Since the dependent product types

$$\prod_{(a:A)} \mu(e,a)=a$$

$$\prod_{(a:A)} \mu(a,e)=a$$

$$\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))$$

are inhabited by definition of an $A_3$-space, each identity type $\mu(e,a)=a$, $\mu(a,e)=a$, and $\mu(\mu(a, b),c)=\mu(a,\mu(b,c))$ is an inhabited proposition, which makes it contractible. Thus,

$$\prod_{(a:A)} isContr(\mu(e,a)=a)$$

$$\prod_{(a:A)} isContr(\mu(a,e)=a)$$

$$\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} isContr(\mu(\mu(a, b),c)=\mu(a,\mu(b,c)))$$

which along with the 0-truncator means that a 0-truncated $A_3$-space is a monoid.

As monoids are $A_3$-spaces, given monoids $A$ and $B$, for any function

$$\phi_\lambda:\left(\prod_{(a:A)} \mu(e_A,a)=a\right) \to \left(\prod_{(b:B)} \mu(e_B,b)=b\right)$$

the left unitor is preserved:

$$\phi_\lambda(\lambda_A) = \lambda_B$$

because

$$\prod_{(b:B)} \mu(e_B,b)=b$$

is contractible. Likewise, for any function

$$\phi_\rho:\left(\prod_{(a:A)} \mu(a, e_A)=a\right) \to \left(\prod_{(b:B)} \mu(b, e_B)=b\right)$$

the right unitor is preserved:

$$\phi_\rho(\rho_A) = \rho_B$$

because

$$\prod_{(b:B)} \mu(b,e_B)=b$$

is contractible, and for any function

$$\phi_\alpha:\left(\prod_{(a_1:A)} \prod_{(a_2:A)} \prod_{(a_3:A)} \mu(\mu(a_1, a_2),a_3)=\mu(a_1,\mu(a_2,a_3))\right) \to \left(\prod_{(b_1:B)} \prod_{(b_2:B)} \prod_{(b_3:B)} \mu(\mu(b_1, b_2),b_3)=\mu(b_1,\mu(b_2,b_3))\right)$$

the associator is preserved:

$$\phi_\alpha(\alpha_A) = \alpha_B$$

because

$$\prod_{(b_1:B)} \prod_{(b_2:B)} \prod_{(b_3:B)} \mu(\mu(b_1, b_2),b_3)=\mu(b_1,\mu(b_2,b_3))$$

is contractible. This means that a monoid homomorphism is also a homomorphism of $A_3$-spaces.

Examples

• Every contractible magma is a monoid.

• 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

• Higher algebra
• A3-space
• commutative monoid
• group
• action
• monoidal groupoid?
• free monoid?
• decimal numeral representations of the natural numbers

References

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