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.

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) , N

Ω∙ :  {}  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

(ΣAB)(bs:BAb0bs), (\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.

module _ { ℓ′} {A : Type∙ } {B : Type∙ ℓ′} where
  Σ-map∙→loops : (Σ∙ A →∙ B)  (Σ _ λ bs  A .fst  B .snd  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 .fst  B .snd  bs)  (Σ∙ A →∙ B)
  loops→Σ-map∙ pair .fst N           = B .snd
  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 ΩB\Omega B is even simpler, perhaps because these are almost definitionally the same thing.

  loops→map∙-Ω : (Σ _ λ bs  A .fst  B .snd  bs)  (A →∙ Ω∙ B)
  loops→map∙-Ω (b , x) .fst a = x a  sym (x (A .snd))
  loops→map∙-Ω (b , x) .snd   = ∙-invr (x (A .snd))

  map∙-Ω→loops : (A →∙ Ω∙ B)  (Σ _ λ bs  A .fst  B .snd  bs)
  map∙-Ω→loops pair .fst = B .snd
  map∙-Ω→loops pair .snd = pair .fst
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 .fst  B .snd  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
      (to-pathp (funext  a  subst-path-right _ _  ∙-idr _  ∙-idl _  ap q (transport-refl _))))

    lemma :  (f : Σ∙ A →∙ B) x  Square
      (sym (f .snd)  ap (f .fst) (merid x))
      (sym (f .snd)) refl (ap (f .fst) (merid x))
    lemma f x = transport (sym Square≡double-composite-path) $
      sym (sym (f .snd)  ap (f .fst) (merid x)) ·· sym (f .snd) ·· ap (f .fst) (merid x)    ≡⟨ double-composite (sym _) _ _ 
       sym (sym (f .snd)  ap (f .fst) (merid x))   sym (f .snd)  ap (f .fst) (merid x)  ≡⟨ ap! (sym-∙ (sym _) _) 
      (ap (f .fst) (sym (merid x))  (f .snd))  sym (f .snd)  ap (f .fst) (merid x)        ≡˘⟨ ∙-assoc _ _ _ ≡˘
      ap (f .fst) (sym (merid x))   (f .snd)  sym (f .snd)  ap (f .fst) (merid x)       ≡⟨ ap! (∙-cancell (sym (f .snd)) _) 
      ap (f .fst) (sym (merid x))  ap (f .fst) (merid x)                                    ≡⟨ ∙-invl _ 
      refl                                                                                   

    invl : is-left-inverse loops→Σ-map∙ Σ-map∙→loops
    invl f = Σ-pathp (funext  { N  sym (f .snd)
                                ; S  refl
                                ; (merid x i)  λ j  lemma f x i j }))
                      (to-pathp (subst-path-left _ _  ∙-idr _  refl))

  loops≃map∙-Ω : (Σ _ λ bs  A .fst  B .snd  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 .snd)))   ∙-invr (b (A .snd))               ≡⟨ ap! (sym-∙ (sym _) _) 
          (sym (∙-idr (b (A .snd)))  ap (b (A .snd) ∙_) (ap sym (sym x)))  ∙-invr (b (A .snd))     ≡⟨ sym (∙-assoc _ _ _) 
          sym (∙-idr (b (A .snd)))   ap  p  b (A .snd)  sym p) (sym x)  ∙-invr (b (A .snd))  ≡⟨ ap! (lemma′ (b (A .snd)) (sym x)) 
          sym (∙-idr (b (A .snd)))  ∙-idr (b (A .snd))  x                                          ≡⟨ ∙-cancell _ _ 
          x                                                                                          

    invl : is-left-inverse map∙-Ω→loops loops→map∙-Ω
    invl (f , p) = Σ-pathp (p (A .snd)) $ to-pathp $ funext $ λ x 
        subst-path-right _ _  sym (∙-assoc _ _ _)
       ap₂ _∙_ refl (∙-invl (p (A .snd)))  ∙-idr _
       ap p (transport-refl x)

Composing these equivalences, we get the adjunction:

(ΣAB)(AΩB). (\Sigma A \to_* B) \simeq (A \to* \Omega B).

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

(SnA)(ΣSn1ΩA)...ΩnA, (S^n \to_* A) \simeq (\Sigma S^{n - 1} \to_* \Omega A) \simeq ... \simeq \Omega^n A,

thus characterising nn-fold loop spaces as basepoint-preserving maps out of SnS^n, the nn-dimensional sphere.

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

Ωⁿ≃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               ≃∎

Hubs and spokes🔗

Inspired by the equivalence built above, although not using it directly, we can characterise h-levels in terms of maps of spheres, too. The idea is that, since a map f:SnAf : S^n \to A is equivalently some loop in AA1, we can characterise the trivial loops as the constant functions SnAS^n \to A. Correspondingly, if every function SnAS^n \to A is trivial, this means that all nn-loops in AA are trivial, so that AA is (n+1)(n+1)-truncated!

We refer to a trivialisation of a map f:SnAf : S^n \to A as being a “hubs-and-spokes” construction. Geometrically, a trivial loop f:SnAf : S^n \to A can be understood as a map from the nn-disc rather than the nn-sphere, where the nn-disc is the type generated by attaching a new point to the sphere (the “hub”), and paths connecting the hub to each point along the sphere (the “spokes”). The resulting type is contractible, whence every function out of it is constant.

hlevel→hubs-and-spokes
  :  {} {A : Type } (n : Nat)  is-hlevel A (suc n)
   (sph : Sⁿ n .fst  A)
   Σ[ hub  A ] (∀ x  sph x  hub)

hubs-and-spokes→hlevel
  :  {} {A : Type } (n : Nat)
   ((sph : Sⁿ n .fst  A)  Σ[ hub  A ] (∀ x  sph x  hub))
   is-hlevel A (suc n)
hlevel→hubs-and-spokes 0 prop sph = sph N , λ x  prop (sph x) (sph N)
hlevel→hubs-and-spokes {A = A} (suc n) h =
  helper λ x y  hlevel→hubs-and-spokes n (h x y)
  where
  helper
    : ((a b : A)  (sph : Sⁿ⁻¹ (1 + n)  a  b)  Σ _ λ hub   x  sph x  hub)
     (sph : Sⁿ⁻¹ (2 + n)  A)
     Σ _ λ hub   x  sph x  hub
  helper h f = f N , sym  r where
    r : (x : Sⁿ⁻¹ (2 + n))  f N  f x
    r N = refl
    r S = h (f N) (f S)  x i  f (merid x i)) .fst
    r (merid x i) j = hcomp ( i   j) λ where
       k (i = i0)  f N
       k (i = i1)  h (f N) (f S)  x i  f (merid x i)) .snd x k j
       k (j = i0)  f N
       k (j = i1)  f (merid x i)
       k (k = i0)  f (merid x (i  j))

hubs-and-spokes→hlevel {A = A} zero spheres x y
  = spheres map .snd N  sym (spheres map .snd S) where
    map : Sⁿ⁻¹ 1  A
    map N = x
    map S = y
hubs-and-spokes→hlevel {A = A} (suc n) spheres x y =
  hubs-and-spokes→hlevel n $ helper spheres x y where
  helper
    : ((sph : Sⁿ⁻¹ (2 + n)  A)  Σ _ λ hub   x  sph x  hub)
      a b
     (sph : Sⁿ⁻¹ (1 + n)  a  b)
     Σ _ λ hub   x  sph x  hub
  helper h x y f = _ , r  where
    f' : Sⁿ⁻¹ (2 + n)  A
    f' N = x
    f' S = y
    f' (merid u i) = f u i

    r : (s : Sⁿ⁻¹ (1 + n))  f s  h f' .snd N  sym (h f' .snd S)
    r s i j = hcomp ( i   j) λ where
      k (k = i0)  h f' .snd N (~ i  j)
      k (i = i0)  h f' .snd (merid s j) (~ k)
      k (i = i1)  hfill ( j) k λ where
        l (j = i0)  x
        l (j = i1)  h f' .snd S (~ l)
        l (l = i0)  h f' .snd N j
      k (j = i0)  h f' .snd N (~ i  ~ k)
      k (j = i1)  h f' .snd S (~ k)

Using this idea, we can define a general nn-truncation type, as a joint generalisation of the propositional and set truncations. While we can not directly build a type with a constructor saying the type is nn-truncated, what we can do is freely generate hubs and spokes for any nn-sphere drawn on the nn-truncation of AA. The result is the universal nn-type admitting a map from AA.

data n-Tr {} (A : Type ) n : Type  where
  inc    : A  n-Tr A n
  hub    : (r : Sⁿ⁻¹ n  n-Tr A n)  n-Tr A n
  spokes : (r : Sⁿ⁻¹ n  n-Tr A n)   x  r x  hub r

For both proving that the nn-truncation has the right h-level, and proving that one can eliminate from it to nn-types, we use the characterisations of truncation in terms of hubs-and-spokes.

n-Tr-is-hlevel
  :  {} {A : Type } n  is-hlevel (n-Tr A (suc n)) (suc n)
n-Tr-is-hlevel n = hubs-and-spokes→hlevel n λ sph  hub sph , spokes sph

instance
  n-tr-decomp :  {} {A : Type } {n}  hlevel-decomposition (n-Tr A (suc n))
  n-tr-decomp = decomp (quote n-Tr-is-hlevel) (`level-minus 1  [])

n-Tr-elim
  :  { ℓ′} {A : Type } {n}
   (P : n-Tr A (suc n)  Type ℓ′)
   (∀ x  is-hlevel (P x) (suc n))
   (∀ x  P (inc x))
    x  P x
n-Tr-elim {A = A} {n} P ptrunc pbase = go where
  module _ (r : Sⁿ n .fst  n-Tr A (1 + n))
           (w : (x : Sⁿ n .fst)  P (r x))
    where
      circle : Sⁿ⁻¹ (1 + n)  P (hub r)
      circle x = subst P (spokes r x) (w x)

      hub′ = hlevel→hubs-and-spokes n (ptrunc (hub r)) circle .fst

      spokes′ :  x  PathP  i  P (spokes r x i)) (w x) hub′
      spokes′ x = to-pathp $
        hlevel→hubs-and-spokes n (ptrunc (hub r)) circle .snd x

  go :  x  P x
  go (inc x)        = pbase x
  go (hub r)        = hub′ r  x  go (r x))
  go (spokes r x i) = spokes′ r  x  go (r x)) x i

As a simpler case of n-Tr-elim, we have the recursion principle, where the type we are eliminating into is constant.

n-Tr-rec
  :  { ℓ′} {A : Type } {B : Type ℓ′} {n}
   is-hlevel B (suc n)  (A  B)  n-Tr A (suc n)  B
n-Tr-rec hl = n-Tr-elim  _  _)  _  hl)

An initial application of the induction principle for nn-truncation of AA is characterising its path spaces, at least for the inclusions of points from AA. Identifications between (the images of) points in AA in the (n+1)(n+1)-truncation are equivalently nn-truncated identifications in AA:

n-Tr-path-equiv
  :  {} {A : Type } {n} {x y : A}
   Path (n-Tr A (2 + n)) (inc x) (inc y)  n-Tr (x  y) (suc n)
n-Tr-path-equiv {A = A} {n} {x = x} {y} = Iso→Equiv isom where

The proof is an application of the encode-decode method. We would like to characterise the space

inc(x)A2+ny, \mathrm{inc}(x) \equiv_{\|A\|_{2+n}} y,

so we will, for every x:Ax : A, define a type family code(x):A2+nType\mathrm{code}(x) : \|A\|_{2+n} \to \mathrm{Type}, where the fibre of code(x)\mathrm{code}(x) over inc(y)\mathrm{inc}(y) should be xy1+n\|x \equiv y\|_{1+n}. However, induction principle for A2+n\|A\|_{2+n} only allows us to map into (2+n)(2+n)-types, while Type\mathrm{Type} itself is not an nn-type for any nn. We salvage our definition by instead mapping into (1+n)-Type(1+n)\text{-}\mathrm{Type}, which is a (2+n)(2+n)-type.

  code : (x : A) (y′ : n-Tr A (2 + n))  n-Type _ (suc n)
  code x =
    n-Tr-elim!
       y′  n-Type _ (suc n))
       y′  el! (n-Tr (Path A x y′) (suc n)))

The rest of the proof boils down to applications of path induction and the induction principle for An+2\|A\|_{n+2}.

  encode′ :  x y  inc x  y   code x y 
  encode′ x _ = J  y _   code x y ) (inc refl)

  decode′ :  x y   code x y   inc x  y
  decode′ x =
    n-Tr-elim! _ λ x  n-Tr-rec hlevel! (ap inc)

  rinv :  x y  is-right-inverse (decode′ x y) (encode′ x y)
  rinv x = n-Tr-elim _
     y  Π-is-hlevel (2 + n)
       c  Path-is-hlevel (2 + n) (is-hlevel-suc (suc n) (code x y .is-tr))))
    λ x  n-Tr-elim! _ λ p  ap n-Tr.inc (subst-path-right _ _  ∙-idl _)

  linv :  x y  is-left-inverse (decode′ x y) (encode′ x y)
  linv x _ = J  y p  decode′ x y (encode′ x y p)  p)
    (ap (decode′ x (inc x)) (transport-refl (inc refl))  refl)

  isom : Iso (inc x  inc y) (n-Tr (x  y) (suc n))
  isom = encode′ _ (inc _)
       , iso (decode′ _ (inc _)) (rinv _ (inc _)) (linv _ (inc _))

  1. Any map f:SnAf : S^n \to A can be made basepoint-preserving by letting AA be based at f(N)f(N).↩︎