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

module Algebra.Group.Homotopy where

private variable
  ℓ : Level
  A : Type ℓ

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 is commutative for $\Omega^{n + 2} A$ is commutative, independent of $A$.

Ωⁿ⁺²-is-abelian-group
  : ∀ {ℓ} {A : Type∙ ℓ} (n : Nat) (p q : Ωⁿ ( + 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 (πₙ₊₁ ( + 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))

Deloopings🔗

A natural question to ask, given that all pointed types have a fundamental group, is whether every group arises as the fundamental group of some type. The answer to this question is “yes”, but in the annoying way that questions like these tend to be answered: Given any group $G$, we construct a type $\mathbf{B} G$ with $\pi_1(\mathbf{B} G) \equiv G$. We call $\mathbf{B} G$ the delooping of $G$.

module _ {ℓ} (G : Group ℓ) where
  module G = Group-on (G .snd)
  open G

  data Deloop : Type ℓ where
    base    : Deloop
    squash  : is-groupoid Deloop
    path    : ⌞ G ⌟ → base ≡ base
    path-sq : (x y : ⌞ G ⌟) → Square refl (path x) (path (x ⋆ y)) (path y)

  instance
    H-Level-Deloop : ∀ {n} → H-Level Deloop ( + n)
    H-Level-Deloop = basic-instance  squash

The delooping is constructed as a higher inductive type. We have a generic base point, and a constructor expressing that Deloop is a groupoid; Since it is a groupoid, it has a set of loops point ≡ point: this is necessary, since otherwise we would not be able to prove that $\pi_1(\mathbf{B} G) \equiv G$. We then have the “interesting” higher constructors: path lets us turn any element of $G$ to a path point ≡ point, and path-sq expresses that path is a group homomorphism. More specifically, path-sq fills the square below:

Using the uniqueness result for double composition, we derive that path is a homomorphism in the traditional sense:

  abstract
    path-∙ : ∀ x y → path (x ⋆ y) ≡ path x ∙ path y
    path-∙ x y i j =
      ··-unique refl (path x) (path y)
        (path (x ⋆ y)    , path-sq x y)
        (path x ∙ path y , ∙-filler _ _)
        i .fst j

    path-unit : path unit ≡ refl
    path-unit =
      path unit                               ≡⟨ sym (∙-idr _) ⟩≡
      path unit ∙ ⌜ refl ⌝                    ≡˘⟨ ap¡ (∙-invr _)  ⟩≡˘
      path unit ∙ path unit ∙ sym (path unit) ≡⟨ ∙-assoc _ _ _ ∙ ap₂ _∙_ (sym (path-∙ _ _)) refl ⟩≡
      path ⌜ unit ⋆ unit ⌝ ∙ sym (path unit)  ≡⟨ ap! G.idr ⟩≡
      path unit ∙ sym (path unit)             ≡⟨ ∙-invr _  ⟩≡
      refl                                    ∎

We define an elimination principle for Deloop, which has a monstruous type since it works in full generality. We’ll also need an eliminator into propositions later, so we define that now.

  Deloop-elim
    : ∀ {ℓ'} (P : Deloop → Type ℓ')
    → (∀ x → is-groupoid (P x))
    → (p : P base)
    → (ploop : ∀ x → PathP (λ i → P (path x i)) p p)
    → ( ∀ x y
        → SquareP (λ i j → P (path-sq x y i j))
                  (λ _ → p) (ploop x) (ploop (x ⋆ y)) (ploop y))
    → ∀ x → P x
  unquoteDef Deloop-elim = make-elim-with (default-elim-visible into )
    Deloop-elim (quote Deloop)

  Deloop-elim-prop
    : ∀ {ℓ'} (P : Deloop → Type ℓ')
    → (∀ x → is-prop (P x))
    → P base
    → ∀ x → P x
  unquoteDef Deloop-elim-prop = make-elim-with (default-elim-visible into )
    Deloop-elim-prop (quote Deloop)

We can then proceed to characterise the type point ≡ x by an encode-decode argument. We define a family Code, where the fibre over base is definitionally G; Then we exhibit inverse equivalences base ≡ x → Code x and Code x → base ≡ x, which fit together to establish G ≡ (base ≡ base). First, to define Code, we perform induction on Deloop:

  Code : Deloop → Set ℓ
  Code =
    Deloop-elim _ (λ _ → hlevel ) (G .fst)
      (λ x → n-ua (act x))
      λ x y → n-Type-square (transport (sym Square≡double-composite-path) (lemma x y))

Since we must map into a type which is known to be a groupoid, we map to the type of Sets: since the collection of $n$-types is a $(n+1)$-type, this is a groupoid. To arrange that the fibre over base is G, we give G as the argument for base in the elimination. This locks us into giving a family of automorphisms act : G → G ≡ G for the path constructor; The constructor path-sq then requires that act be a homomorphism from $G$ to $\mathrm{Aut}(G)$.

    where
      act : ∀ x → ⌞ G ⌟ ≃ ⌞ G ⌟
      act x = Iso→Equiv (_⋆ x , p) where
        open is-iso

        p : is-iso (_⋆ x)
        p .inv = _⋆ x ⁻¹
        p .rinv x = sym G.associative ·· ap₂ G._⋆_ refl G.inversel ·· G.idr
        p .linv x = sym G.associative ·· ap₂ G._⋆_ refl G.inverser ·· G.idr

We take $y \mapsto y \star x$ as the definition of the act, which is an automorphism of $G$ since it is invertible by $y \mapsto y \star x^{-1}$, and it preserves composition by associativity of $\star$, as is shown in the lemma below.

      lemma : ∀ x y → ua (act x) ∙ ua (act y) ≡ ua (act (x ⋆ y))
      lemma x y =
        ua (act x) ∙ ua (act y) ≡⟨ sym ua∙ ⟩≡
        ua (act x ∙e act y)     ≡⟨ ap ua (Σ-prop-path is-equiv-is-prop (funext λ z → sym (Group-on.associative (G .snd)))) ⟩≡
        ua (act (x ⋆ y))        ∎

We then define the encoding and decoding functions. The encoding function encode is given by lifting a path from Deloop to Code. For decoding, we do induction on Deloop with Code x .fst → base ≡ x as the motive.

  encode : ∀ x → base ≡ x → ∣ Code x ∣
  encode x p = subst (λ x → ∣ Code x ∣) p unit

  decode : ∀ x → ∣ Code x ∣ → base ≡ x
  decode = Deloop-elim _
    (λ _ → hlevel )

With this motive, the type of what we must give for base reduces to G → base ≡ base, for which path suffices; The path case is handled by path-sq, and the path-sq case is automatic.

    path
    (λ x → ua→ λ a → path-sq _ _)
    (λ x y → is-set→squarep (λ i j → hlevel ) _ _ _ _)

Proving that these are inverses finishes the proof. For one direction, we use path induction to reduce to the case decode base (encode base refl) ≡ refl; A quick argument tells us that encode base refl is the group identity, and since path is a group homomorphism, we have path unit = refl, as required.

  encode→decode : ∀ {x} (p : base ≡ x) → decode x (encode x p) ≡ p
  encode→decode p =
    J (λ y p → decode y (encode y p) ≡ p)
      (ap path (transport-refl _) ∙ path-unit)
      p

In the other direction, we do induction on deloopings; Since the motive is a family of propositions, we can use Deloop-elim-prop instead of the full Deloop-elim, which reduces the goal to proving $1 \star 1 = 1$.

  decode→encode : ∀ x (c : ∣ Code x ∣) → encode x (decode x c) ≡ c
  decode→encode =
    Deloop-elim-prop
      (λ x → (c : ∣ Code x ∣) → encode x (decode x c) ≡ c)
      (λ x → Π-is-hlevel  λ _ → Code x .is-tr _ _)
      λ c → transport-refl _ ∙ G.idl

This completes the proof, and lets us establish that the fundamental group of Deloop is G, which is what we wanted.

  G≃ΩB : ⌞ G ⌟ ≃ (base ≡ base)
  G≃ΩB = Iso→Equiv (path , iso (encode base) encode→decode (decode→encode base))

  G≡π₁B : G ≡ πₙ₊₁  (Deloop , base)
  G≡π₁B = ∫-Path Groups-equational
    (total-hom (λ x → inc (path x)) (record { pres-⋆ = λ x y → ap ∥_∥₀.inc (path-∙ _ _) }))
    (∙-is-equiv (G≃ΩB .snd) (∥-∥₀-idempotent (squash base base)))