module Algebra.Group.Homotopy where

Homotopy groups🔗

Given a pointed type we refer to the type as the loop space of , and refer to it in short as Since we always have is itself a pointed type, the construction can be iterated, a process which we denote

Ωⁿ : Nat  Type∙   Type∙ 
Ωⁿ zero A    = A
Ωⁿ (suc n) (A , x) with Ωⁿ n (A , x)
... | (T , x) = Path T x x , refl

For positive we can give a Group structure, obtained by truncating the higher groupoid structure that is equipped with. We call the sequence the homotopy groups of but remark that the indexing used by πₙ₊₁ is off by 1: πₙ₊₁ 0 A is the fundamental group

πₙ₊₁ : Nat  Type∙   Group 
πₙ₊₁ n t = to-group omega where
  omega : make-group  Ωⁿ (suc n) t .fst ∥₀
  omega .make-group.group-is-set = squash
  omega .make-group.unit = inc refl
  omega .make-group.mul = ∥-∥₀-map₂ _∙_
  omega .make-group.inv = ∥-∥₀-map sym

As mentioned above, the group structure is given entirely by the groupoid structure of types: The neutral element is refl, the group operation is path concatenation, and the inverses are given by inverting paths.

  omega .make-group.assoc = elim! λ x y z i  inc (∙-assoc x y z i)
  omega .make-group.invl = elim! λ x i  inc (∙-invl x i)
  omega .make-group.idl = elim! λ x i  inc (∙-idl x i)

A direct cubical transcription of the Eckmann-Hilton argument tells us that path concatenation for is commutative, independent of

Ωⁿ⁺²-is-abelian-group
  :  {} {A : Type∙ } (n : Nat) (p q : Ωⁿ (2 + n) A .fst)
   p  q  q  p
Ωⁿ⁺²-is-abelian-group n p q =
  transport
     k  ap  x  ∙-idr x k) p  ap  x  ∙-idl x k) q
          ap  x  ∙-idl x k) q  ap  x  ∙-idr x k) p)
     i   j  p (j  ~ i)  q (j  i))
           j  p (~ i  j)  q (i  j)))

The proof can be visualized with the following diagram, where the vertices are in The outer rectangle shows p ∙ q ≡ q ∙ p, which is filled by transporting the two inner squares using ∙-idr on p j and ∙-idl on q j. Note that ∙-idr refl and ∙-idl refl are definitionally equal. In the two inner squares, p j and q j are on different sides of the path composition, so we can use the De Morgan structure on the interval to have p and q slip by each other.

Lifting this result through the set truncation establishes that is an Abelian group:

πₙ₊₂-is-abelian-group :  {} {A : Type∙ } (n : Nat)
                       Group-on-is-abelian (πₙ₊₁ (1 + n) A .snd)
πₙ₊₂-is-abelian-group {A = A} n =
  elim! λ x y i  inc (Ωⁿ⁺²-is-abelian-group n x y i)

We can give an alternative construction of the fundamental group for types that are known to be groupoids: in that case, we can avoid using a set truncation since the loop space is already a set.

module π₁Groupoid {} ((T , t) : Type∙ ) (grpd : is-groupoid T) where
  private
    mk : make-group (t  t)
    mk .make-group.group-is-set = grpd t t
    mk .make-group.unit         = refl
    mk .make-group.mul          = _∙_
    mk .make-group.inv          = sym
    mk .make-group.assoc        = ∙-assoc
    mk .make-group.invl         = ∙-invl
    mk .make-group.idl          = ∙-idl

  on-Ω : Group-on (t  t)
  on-Ω = to-group-on mk

  π₁ : Group 
  π₁ = to-group mk

  π₁≡π₀₊₁ : π₁  πₙ₊₁ 0 (T , t)
  π₁≡π₀₊₁ = ∫-Path
    (total-hom inc (record { pres-⋆ = λ _ _  refl }))
    (∥-∥₀-idempotent (grpd _ _))