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 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β β
Ξ©βΏ (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
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)