Homotopy Type Theory group > history (Rev #5)

Definition

A group consists of

  • A type GG,
  • A basepoint e:Ge:G
  • A binary operation μ:GGG\mu : G \to G \to G
  • A unary operation ι:GG\iota: G \to G
  • A contractible left unit identity
    c λ: (a:G)isContr(μ(e,a)=a)c_\lambda:\prod_{(a:G)} isContr(\mu(e,a)=a)
  • A contractible right unit identity
    c ρ: (a:G)isContr(μ(a,e)=a)c_\rho:\prod_{(a:G)} isContr(\mu(a,e)=a)
  • A contractible associative identity
    c α: (a:G) (b:G) (c:G)isContr(μ(μ(a,b),c)=μ(a,μ(b,c)))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: (a:G)isContr(μ(ι(a),a)=e)c_l:\prod_{(a:G)} isContr(\mu(\iota(a), a)=e)
  • A contractible right inverse identity
    c r: (a:G)isContr(μ(a,ι(a))=e)c_r:\prod_{(a:G)} isContr(\mu(a,\iota(a))=e)
  • A 0-truncator
    τ 0: (a:G) (b:G)isProp(a=b)\tau_0: \prod_{(a:G)} \prod_{(b:G)} isProp(a=b)

Examples

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

  • The integers are a group.

  • Given a set AA, the type of automorphisms Aut(A)Aut(A) has the structure of a group, with basepoint id Aid_A, binary operation function composition, and unary operation inverse automorphism () 1{(-)}^{-1}.

See also

References

Revision on February 14, 2022 at 22:30:41 by Anonymous?. See the history of this page for a list of all contributions to it.