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

Showing changes from revision #2 to #3: Added | Removed | Changed

Definition

A commutative monoid or commutative $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 commutator
  $$\kappa:\prod_{(a:A)} \prod_{(b:A)} \mu(a, b)=\mu(b, a)$$
• 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$$

Examples

• The integers are an commutative monoid.

See also

• Synthetic homotopy theory
• abelian group
• commutative A3-space
• monoid