module Algebra.Group.Homotopy where

Homotopy groups🔗

Given a pointed type $(A, a)$ we refer to the type $a = a$ as the loop space of $A$, and refer to it in short as $\Omega A$. Since we always have $\mathrm{refl} : a = a$, $\Omega A$ is itself a pointed type, the construction can be iterated, a process which we denote $\Omega^n A$.

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

For positive $n$, we can give $\Omega^n A$ a Group structure, obtained by truncating the higher groupoid structure that $A$ is equipped with. We call the sequence $\pi_n(A)$ the homotopy groups of $A$, but remark that the indexing used by πₙ is off by 1: πₙ 0 A is the fundamental group $\pi_1(A)$.

πₙ₊₁ : 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₃ (λ _ _ _ → is-prop→is-set (squash _ _))
      λ x y z i → inc (∙-assoc x y z i)
  omega .make-group.invl =
    ∥-∥₀-elim (λ _ → is-prop→is-set (squash _ _)) λ x i → inc (∙-invl x i)
  omega .make-group.idl =
    ∥-∥₀-elim (λ _ → is-prop→is-set (squash _ _)) λ x i → inc (∙-idl x i)

A direct cubical transcription of the Eckmann-Hilton argument tells us that path concatenation for $\Omega^{n + 2} A$ is commutative, independent of $A$.

Ωⁿ⁺²-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 $\Omega^{n + 1} A$. 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 $\pi_{n+2}$ 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 → is-prop→is-set (squash _ _))
             (λ x y i → inc (Ωⁿ⁺²-is-abelian-group n x y i))