Homotopy Type Theory group > history (Rev #2)

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, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)