## 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. ## See also ## * [[Synthetic homotopy theory]] * [[commutative monoid]] * [[group]] * [[ring]]