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

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)$$

A homomorphism of commutative $A_3$-spaces between two commutative $A_3$-spaces $A$ and $B$ is a function $\phi:A \to B$ such that

• The basepoint is preserved
  $$\phi(e_A) =_B e_B$$
• The binary operation is preserved
  $$\prod_{(a:A)} \prod_{(b:A)} \phi(\mu_A(a, b)) =_B \mu_B(\phi(a),\phi(b))$$
• The left unitor is preserved
• The right unitor is preserved
• The associator is preserved
• The commutator is preserved

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