Homotopy Type Theory group > history (Rev #5)

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 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

• Every contractible magma $(M, \mu)$ with a function $f:M \to M$ is a group.

• 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

• Higher algebra
• grouplike A3-space
• monoid
• abelian group
• free group?

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)