Homotopy Type Theory commutative A3-space > history (Rev #1)

Definition

A commutative $A_3$-space or commutative H-monoid 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)$$

Examples

• The integers are a commutative $A_3$-space.

• A commutative monoid is a 0-truncated commutative $A_3$-space.

See also

• Synthetic homotopy theory
• A3-space
• commutative monoid