[[!redirects Z-module]] ## 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)$$ ## Examples ## * The [[integers]] are an abelian group. ## See also ## * [[commutative monoid]] * [[group]] * [[divisible group]] * [[rationalization of an abelian group]] * [[ordered abelian group]] * [[abelian group homomorphism]] * [[ring]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) * Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson, [Symmetry book](https://unimath.github.io/SymmetryBook/book.pdf) (2021)