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

## 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 is the type $\mathrm{Aut}(\mathrm{Aut}(G))$ of automorphisms of automorphisms in $G$.

### As a group

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 left unit identity
$c_\lambda:\prod_{a:G} \mu(e,a)=a$
• A right unit identity
$c_\rho:\prod_{a:G} \mu(a,e)=a$
• A associative identity
$c_\alpha:\prod_{a:G} \prod_{b:G} \prod_{c:G} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))$
• A left inverse identity
$c_l:\prod_{a:G} \mu(\iota(a), a)=e$
• A right inverse identity
$c_r:\prod_{a:G} \mu(a,\iota(a))=e$
• A commutative identity
$c_\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)} c = d$