⚠️ This module is not part of this project and is only included for reference.
It is either part of the 1lab, the cubical library, or a built-in Agda module.
<!--
```agda
{-# OPTIONS -vtactic.hlevel:10 #-}
open import 1Lab.Prelude
open import Algebra.Group.Homotopy
open import Data.List using (_∷_ ; [])
open import Homotopy.Space.Suspension
open import Homotopy.Space.Sphere
```
-->
```agda
module Homotopy.Base where
```
# Synthetic homotopy theory
This module contains the basic definitions for the study of synthetic
homotopy theory. Synthetic homotopy theory is the name given to studying
$\infty$-groupoids in their own terms, i.e., the application of homotopy type
theory to computing homotopy invariants of spaces. Central to the theory
is the concept of [[pointed type]] and [[pointed map]]. After all, [homotopy
groups] are no more than the set-truncations of n-fold iterated loop
spaces, and loop spaces are always relative to a basepoint.
[homotopy groups]: Algebra.Group.Homotopy.html
A helper that will come in handy is `Σ∙`{.Agda}, which attaches the
north pole as the basepoint of the suspended space.
```agda
Σ∙ : ∀ {ℓ} → Type∙ ℓ → Type∙ ℓ
Σ∙ A = Susp∙ (A .fst)
Ω∙ : ∀ {ℓ} → Type∙ ℓ → Type∙ ℓ
Ω∙ (A , a) = Path A a a , refl
```
## The suspension-loop space adjunction
An important stepping stone in calculating loop spaces of higher types
is the _suspension-loop space_ [[adjunction]]: basepoint-preserving maps
_from_ a suspension are the same thing as basepoint-preserving maps
_into_ a loop space. We construct the equivalence in two steps, but both
halves are constructed in elementary terms.
First, we'll prove that
$$
(\Sigma A \to_* B) \simeq \left(\sum_{b_s : B} A \to b_0 \equiv b_s\right),
$$
which is slightly involved, but not too much. The actual equivalence is
very straightforward to construct, but proving that the two maps
`Σ-map→loops` and `loops→Σ-map` are inverses involves nontrivial path
algebra.
```agda
module _ {ℓ ℓ'} {A∙@(A , a₀) : Type∙ ℓ} {B∙@(B , b₀) : Type∙ ℓ'} where
Σ-map∙→loops : (Σ∙ A∙ →∙ B∙) → (Σ _ λ bs → A → b₀ ≡ bs)
Σ-map∙→loops f .fst = f .fst S
Σ-map∙→loops f .snd a = sym (f .snd) ∙ ap (f .fst) (merid a)
loops→Σ-map∙ : (Σ _ λ bs → A → b₀ ≡ bs) → (Σ∙ A∙ →∙ B∙)
loops→Σ-map∙ pair .fst N = b₀
loops→Σ-map∙ pair .fst S = pair .fst
loops→Σ-map∙ pair .fst (merid x i) = pair .snd x i
loops→Σ-map∙ pair .snd = refl
```
The construction for turning a family of loops into a
basepoint-preserving map into $\Omega B$ is even simpler, perhaps
because these are almost definitionally the same thing.
```agda
loops→map∙-Ω : (Σ _ λ bs → A → b₀ ≡ bs) → (A∙ →∙ Ω∙ B∙)
loops→map∙-Ω (b , l) .fst a = l a ∙ sym (l a₀)
loops→map∙-Ω (b , l) .snd = ∙-invr (l a₀)
map∙-Ω→loops : (A∙ →∙ Ω∙ B∙) → (Σ _ λ bs → A → b₀ ≡ bs)
map∙-Ω→loops (f , _) .fst = b₀
map∙-Ω→loops (f , _) .snd = f
```
<details>
<summary>The path algebra for showing these are both pairs of inverse
equivalences is not very interesting, so I've kept it hidden.</summary>
```agda
Σ-map∙≃loops : (Σ∙ A∙ →∙ B∙) ≃ (Σ _ λ b → A → b₀ ≡ b)
Σ-map∙≃loops = Iso→Equiv (Σ-map∙→loops , iso loops→Σ-map∙ invr invl) where
invr : is-right-inverse loops→Σ-map∙ Σ-map∙→loops
invr (p , q) = Σ-pathp refl $ funext λ a → ∙-idl (q a)
invl : is-left-inverse loops→Σ-map∙ Σ-map∙→loops
invl (f , pres) i = funext f' i , λ j → pres (~ i ∨ j) where
f' : (a : Susp A) → loops→Σ-map∙ (Σ-map∙→loops (f , pres)) .fst a ≡ f a
f' N = sym pres
f' S = refl
f' (merid x i) j = ∙-filler₂ (sym pres) (ap f (merid x)) j i
loops≃map∙-Ω : (Σ _ λ bs → A → b₀ ≡ bs) ≃ (A∙ →∙ Ω∙ B∙)
loops≃map∙-Ω = Iso→Equiv (loops→map∙-Ω , iso map∙-Ω→loops invr invl) where
lemma' : ∀ {ℓ} {A : Type ℓ} {x : A} (q : x ≡ x) (r : refl ≡ q)
→ ap (λ p → q ∙ sym p) r ∙ ∙-invr q ≡ ∙-idr q ∙ sym r
lemma' q r =
J (λ q' r → ap (λ p → q' ∙ sym p) r ∙ ∙-invr q' ≡ ∙-idr q' ∙ sym r)
(∙-idl _ ∙ sym (∙-idr _))
r
invr : is-right-inverse map∙-Ω→loops loops→map∙-Ω
invr (b , x) = Σ-pathp (funext (λ a → ap₂ _∙_ refl (ap sym x) ∙ ∙-idr _)) (to-pathp (subst-path-left _ _ ∙ lemma)) where
lemma =
⌜ sym (ap₂ _∙_ refl (ap sym x) ∙ ∙-idr (b a₀)) ⌝ ∙ ∙-invr (b a₀) ≡⟨ ap! (sym-∙ (sym _) _) ⟩
(sym (∙-idr (b a₀)) ∙ ap (b a₀ ∙_) (ap sym (sym x))) ∙ ∙-invr (b a₀) ≡⟨ sym (∙-assoc _ _ _) ⟩
sym (∙-idr (b a₀)) ∙ ⌜ ap (λ p → b a₀ ∙ sym p) (sym x) ∙ ∙-invr (b a₀) ⌝ ≡⟨ ap! (lemma' (b a₀) (sym x)) ⟩
sym (∙-idr (b a₀)) ∙ ∙-idr (b a₀) ∙ x ≡⟨ ∙-cancell _ _ ⟩
x ∎
invl : is-left-inverse map∙-Ω→loops loops→map∙-Ω
invl (f , p) = Σ-pathp (p a₀) $ to-pathp $ funext $ λ x →
subst-path-right _ _ ∙ sym (∙-assoc _ _ _)
∙ ap₂ _∙_ refl (∙-invl (p a₀)) ∙ ∙-idr _
∙ ap p (transport-refl x)
```
</details>
Composing these equivalences, we get the adjunction:
$$
(\Sigma A \to_* B) \simeq (A \to* \Omega B).
$$
```agda
Σ-map∙≃map∙-Ω : (Σ∙ A∙ →∙ B∙) ≃ (A∙ →∙ Ωⁿ 1 B∙)
Σ-map∙≃map∙-Ω = Σ-map∙≃loops ∙e loops≃map∙-Ω
```
### Loop spaces are equivalently based maps out of spheres
Repeatedly applying the equivalence we just built, we can build an
equivalence
$$
(S^n \to_* A) \simeq (\Sigma S^{n - 1} \to_* \Omega A) \simeq ... \simeq \Omega^n A,
$$
thus characterising $n$-fold loop spaces as basepoint-preserving maps
out of $S^n$, the $n$-dimensional sphere.
<!--
```agda
reassoc-Ω : ∀ {ℓ} {A : Type∙ ℓ} n → Ωⁿ n (Ω∙ A) ≡ Ωⁿ (suc n) A
reassoc-Ω zero = refl
reassoc-Ω {A = A} (suc n) =
Ωⁿ 1 (Ωⁿ n (Ωⁿ 1 A)) ≡⟨ ap (Ωⁿ 1) (reassoc-Ω n) ⟩
Ωⁿ 1 (Ωⁿ (suc n) A) ∎
```
-->
As a special case, in the zeroth dimension, we conclude that $(2 \to_*
A) \equiv A$, i.e., basepoint-preserving maps from the booleans (based
at either point) are the same thing as points of $A$.
```agda
Ωⁿ≃Sⁿ-map : ∀ {ℓ} {A : Type∙ ℓ} n → (Sⁿ n →∙ A) ≃ Ωⁿ n A .fst
Ωⁿ≃Sⁿ-map {A = A} zero = Iso→Equiv (from , iso to (λ _ → refl) invr) where
to : A .fst → ((Susp ⊥ , N) →∙ A)
to x .fst N = A .snd
to x .fst S = x
to x .snd = refl
from : ((Susp ⊥ , N) →∙ A) → A .fst
from f = f .fst S
invr : is-right-inverse from to
invr (x , p) = Σ-pathp (funext (λ { N → sym p ; S → refl })) λ i j → p (~ i ∨ j)
Ωⁿ≃Sⁿ-map {A = A} (suc n) =
(Σ∙ (Susp _ , N) →∙ A) ≃⟨ Σ-map∙≃map∙-Ω ⟩
((Susp (Sⁿ⁻¹ n) , N) →∙ Ωⁿ 1 A) ≃⟨ Ωⁿ≃Sⁿ-map n ⟩
Ωⁿ n (Ωⁿ 1 A) .fst ≃⟨ path→equiv (ap fst (reassoc-Ω n)) ⟩
Ωⁿ (suc n) A .fst ≃∎
```