Homotopy Type Theory abelian group > history (Rev #16, changes)

Showing changes from revision #15 to #16: Added | Removed | Changed


As a twice-delooping of a pointed simply connected 2-groupoid

A pointed simply connected 2-groupoid consists of

  • A type GG
  • A basepoint e:Ge:G
  • A 1-connector
    κ 1:∏ f:G→𝟙∏ a:𝟙isContr([fiber(f,a)] 1)\kappa_1:\prod_{f:G \to \mathbb{1}} \prod_{a:\mathbb{1}} \mathrm{isContr}(\left[\mathrm{fiber}(f, a)\right]_{1})
  • A 2-truncator:
    τ 2:isTwoGroupoid(G)\tau_2:\mathrm{isTwoGroupoid}(G)

An abelian group is the type Aut(Aut(G))\mathrm{Aut}(\mathrm{Aut}(G)) of automorphisms of automorphisms in GG.

As a group

An abelian group or consists of

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


See also


Revision on June 16, 2022 at 08:05:41 by Anonymous?. See the history of this page for a list of all contributions to it.