# Homotopy Type Theory abelian group > history (Rev #15, changes)

Showing changes from revision #14 to #15: Added | Removed | Changed

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

## References

Revision on June 15, 2022 at 18:27:33 by Anonymous?. See the history of this page for a list of all contributions to it.