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

Properties

Relation to commutative $A_3$-spaces

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

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

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

Similarly, any 0-truncated commutative $A_3$-space or commutative $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$, $\mu(\mu(a, b),c)=\mu(a,\mu(b,c))$, and $\mu(a, b)=\mu(b, a)$ are propositions. Since the dependent product types

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

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