## Definition ## 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 left unitor $$\lambda:\prod_{(a:G)} \mu(e,a)=a$$ * A right unitor $$\rho:\prod_{(a:G)} \mu(a,e)=a$$ * An asssociator $$\alpha:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))$$ * A left invertor $$l:\prod_{(a:G)} \mu(\iota(a), a)=e$$ * A right invertor $$r:\prod_{(a:G)} \mu(a,\iota(a))=e$$ * A 0-truncator $$\tau_0: \prod_{(a:G)} \prod_{(b:G)} \prod_{(c:a=b)} \prod_{(d:a=b)} \sum_{(x:c=d)} \prod_{(y:c=d)} x=y$$ ## 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 ## * [[Synthetic homotopy theory]] * [[grouplike A3-space]] * [[monoid]] * [[abelian group]] * [[free group]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)