open import 1Lab.Reflection.Induction
open import 1Lab.Prelude

open import Algebra.Group.Cat.Base
open import Algebra.Semigroup
open import Algebra.Group.Ab
open import Algebra.Monoid
open import Algebra.Group
open import Algebra.Magma

open import Data.Set.Truncation

open import Homotopy.Conjugation
open import Homotopy.Truncation
open import Homotopy.Loopspace

module Algebra.Group.Homotopy where

private variable
  ℓ     : Level
  A B C : Type∙ ℓ

Homotopy groups🔗

For positive $n\text{,}$ we can give the iterated loop space ${\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\text{,}$ but remark that the indexing used by πₙ₊₁ is off by 1: πₙ₊₁ 0 A is the fundamental group ${\pi }_1(A)\text{.}$

πₙ₊₁ : 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)

πₙ₊₁-ap
  : ∀ {ℓ} {A B : Type∙ ℓ} n (e : A ≃∙ B)
  → πₙ₊₁ n A Groups.≅ πₙ₊₁ n B
πₙ₊₁-ap n e = total-iso (∥-∥₀-ap (Ωⁿ-ap (suc n) e .fst)) record
  { pres-⋆ = elim! λ q r → ap ∥_∥₀.inc (Ωⁿ-map-∙ n (Equiv∙.to∙ e) _ _) }

πₙ₊₁-map
  : ∀ {ℓ ℓ'} {A : Type∙ ℓ} {B : Type∙ ℓ'} n (f : A →∙ B)
  → ⌞ πₙ₊₁ n A ⌟ → ⌞ πₙ₊₁ n B ⌟
πₙ₊₁-map n f = ∥-∥₀-map (Ωⁿ-map (suc n) f .fst)

opaque

  πₙ-def
    : ∀ {ℓ} (A : Type∙ ℓ) n
    → (⌞ πₙ₊₁ n A ⌟ , inc refl) ≃∙ Ωⁿ (suc n) (n-Tr∙ A (suc (n + )))
  πₙ-def A n = n-Tr-set ∙e n-Tr-Ωⁿ A  (suc n) .fst , n-Tr-Ωⁿ A  (suc n) .snd

  πₙ-def-inc
    : ∀ {ℓ} (A : Type∙ ℓ) n → (l : ⌞ Ωⁿ ( + n) A ⌟)
    → πₙ-def A n · inc l ≡ Ωⁿ-map ( + n) inc∙ · l
  πₙ-def-inc A n l = n-Tr-Ωⁿ-inc A  (suc n) ·ₚ l

  πₙ-def-∙
    : ∀ {ℓ} (A : Type∙ ℓ) n → (p q : ⌞ Ωⁿ ( + n) A ⌟)
    → πₙ-def A n · inc (p ∙ q) ≡ πₙ-def A n · inc p ∙ πₙ-def A n · inc q
  πₙ-def-∙ A = n-Tr-Ωⁿ-∙ A 

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

Ωⁿ⁺²-is-abelian
  : ∀ {ℓ} {A : Type∙ ℓ} (n : Nat) (p q : Ωⁿ ( + n) A .fst)
  → p ∙ q ≡ q ∙ p
Ωⁿ⁺²-is-abelian 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\text{.}$ 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 (πₙ₊₁ ( + n) A .snd)
πₙ₊₂-is-abelian-group {A = A} n =
  elim! λ x y i → inc (Ωⁿ⁺²-is-abelian n x y i)

We can give an alternative construction of the fundamental group ${\pi }_1$ 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

  π₁≡π₀₊₁ : π₁ Groups.≅ πₙ₊₁  (T , t)
  π₁≡π₀₊₁ = total-iso (inc , ∥-∥₀-idempotent (grpd _ _)) (record { pres-⋆ = λ x y → refl })