## Definition ## ### As a monoid ### A __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 0-truncator $$\tau_0: \prod_{(a:G)} \prod_{(b:G)} isProp(a=b)$$ ## Examples ## * The [[integers]] are a group. * Given a [[set]] $A$, the type of automorphisms $Aut(A)$ has the structure of a group, with basepoint $id_A$, binary operation function composition, and unary operation inverse automorphism ${(-)}^{-1}$. ## See also ## * [[monoid]] * [[abelian group]] ## 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)