# Homotopy Type Theory abelian group > history (Rev #4)

## Definition

An abelian group consists of

• A type $G$,
• A basepoint $e:G$
• A binary operation $\mu : G \to G \to G$
• A unary operation $\iota: G \to G$
• 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 contractible left inverse identity
$c_l:\prod_{(a:G)} isContr(\mu(\iota(a), a)=e)$
• A contractible right inverse identity
$c_r:\prod_{(a:G)} isContr(\mu(a,\iota(a))=e)$
• A contractible commutative identity
$c_\kappa:\prod_{(a:A)} \prod_{(b:A)} isContr(\mu(a, b)=\mu(b, a))$
• A 0-truncator
$\tau_0: \prod_{(a:G)} \prod_{(b:G)} isProp(a=b)$

## Examples

• Every contractible magma $(M, \mu)$ with a function $f:M \to M$ is an abelian group.

• The integers are an abelian group.