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

## Definition

### As a twice-delooping of a pointed simply connected 2-groupoid

A pointed simply connected 2-groupoid consists of

• A type $G$
• A basepoint $e:G$
• A 1-connector
$\kappa_1:\prod_{f:G \to \mathbb{1}} \prod_{a:\mathbb{1}} \mathrm{isContr}(\left[\mathrm{fiber}(f, a)\right]_{1})$
• A 2-truncator:
$\tau_2:\mathrm{isTwoGroupoid}(G)$

An abelian group or $\mathbb{Z}$-module is the type $\mathrm{Aut}(\mathrm{Aut}(G))$ of automorphisms of automorphisms in $G$.

### As a group

An abelian group or $\mathbb{Z}$-module 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)$

### As a module

An abelian group or $\mathbb{Z}$-module is a set $S$ with a term $0:S$ and a binary function $(-)+(-):S \times S \to S$, and a left multiplicative $\mathbb{Z}$-action $(-)\cdot_l(-):\mathbb{Z} \times S \to S$, such that

$\prod_{a:S} \prod_{b:S} a + b = b + a$
$\prod_{a:S} \prod_{b:S} \prod_{c:S} a + (b + c) = (a + b) + c$
$\prod_{a:S} 1 \cdot_l a = a$
$\prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} \prod_{c:S} (a \cdot b) \cdot_l c = a \cdot_l (b \cdot_l c)$
$\prod_{a:S} 0 \cdot_l a = 0$
$\prod_{a:\mathbb{Z}} \prod_{b:S} \prod_{c:S} a \cdot_l (b + c) = a \cdot_l b + a \cdot_l c$
$\prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} \prod_{c:S} (a + b) \cdot_l c = a \cdot_l c + b \cdot_l c$

We define the functions $-:S \to S$ and $(-)\cdot_r(-):S \times \mathbb{Z} \to S$ to be

$-a \coloneqq (-1) \cdot_l a$
$a \cdot_r b \coloneqq b \cdot_l a$

and $S$ is an abelian group and a $\mathbb{Z}$-bimodule

$a = 1 \cdot_1 a = (1 + 0) \cdot_1 a = (1 \cdot_1 a) + (0 \cdot_1 a) = a + 0$
$a = 1 \cdot_1 a = (0 + 1) \cdot_1 a = (0 \cdot_1 a) + (1 \cdot_1 a) = 0 + a$
$0 = 0 \cdot_1 a = (1 + -1) \cdot_1 a = (1 \cdot_1 a) + (-1 \cdot_1 a) = a + -a$
$0 = 0 \cdot_1 a = (-1 + 1) \cdot_1 a = (-1 \cdot_1 a) + (1 \cdot_1 a) = -a + a$

## Examples

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

• The integers are an abelian group.