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 is commutative 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))

## 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 (3 + n) H-Level-Deloop = basic-instance 3 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

##
And the standard argument shows that `path`

, being a group
homomorphism, preserves the group identity.

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 3) 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 1) 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 3) (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 `Set`

s: 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 3)

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 2) _ _ _ _)

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 1 Ξ» _ β 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 β‘ Οβββ 0 (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)))