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 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.

A helper that will come in handy is Ξ£βˆ™, which attaches the north pole as the basepoint of the suspended space.

Ξ£βˆ™ : βˆ€ {β„“} β†’ 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

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.

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 is even simpler, perhaps because these are almost definitionally the same thing.

  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
The path algebra for showing these are both pairs of inverse equivalences is not very interesting, so I’ve kept it hidden.
  Ξ£-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 _))

    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)

Composing these equivalences, we get the adjunction:

  Ξ£-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

thus characterising loop spaces as basepoint-preserving maps out of the sphere.

As a special case, in the zeroth dimension, we conclude that i.e., basepoint-preserving maps from the booleans (based at either point) are the same thing as points of

Ωⁿ≃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               β‰ƒβˆŽ