module Homotopy.Truncation where

General truncations🔗

Inspired by the equivalence between loop spaces and maps out of spheres, 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 : S^n \to A$ is equivalently some loop in $A$ ¹, we can characterise the trivial loops as the constant functions $S^n \to A$ . Correspondingly, if every function $S^n \to A$ is trivial, this means that all $n$ -loops in $A$ are trivial, so that $A$ is $(n+1)$ -truncated!

We refer to a trivialisation of a map $f : S^n \to A$ as being a “hubs-and-spokes” construction. Geometrically, a trivial loop $f : S^n \to A$ can be understood as a map from the $n$ -disc rather than the $n$ -sphere, where the $n$ -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)

Using this idea, we can define a general $n$ -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 $n$ -truncated, what we can do is freely generate hubs and spokes for any $n$ -sphere drawn on the $n$ -truncation of $A$ . The result is the universal $n$ -type admitting a map from $A$ .

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 $n$ -truncation has the right h-level, and proving that one can eliminate from it to $n$ -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 $n$ -truncation of $A$ is characterising its path spaces, at least for the inclusions of points from $A$ . Identifications between (the images of) points in $A$ in the $(n+1)$ -truncation are equivalently $n$ -truncated identifications in $A$ :

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

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

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

n-Tr-univ
  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} n
  → is-hlevel B (suc n)
  → (n-Tr A (suc n) → B) ≃ (A → B)
n-Tr-univ n b-hl = Iso→Equiv λ where
  .fst              f → f ∘ inc
  .snd .is-iso.inv  f → n-Tr-rec b-hl f
  .snd .is-iso.rinv f → refl
  .snd .is-iso.linv f → funext $ n-Tr-elim _ (λ x → Path-is-hlevel (suc n) b-hl) λ _ → refl

n-Tr-product
  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {n}
  → n-Tr (A × B) (suc n) ≃ (n-Tr A (suc n) × n-Tr B (suc n))
n-Tr-product {A = A} {B} {n} = distrib , distrib-is-equiv module n-Tr-product where
  distrib : n-Tr (A × B) (suc n) → n-Tr A (suc n) × n-Tr B (suc n)
  distrib (inc (x , y)) = inc x , inc y
  distrib (hub r) .fst = hub λ s → distrib (r s) .fst
  distrib (hub r) .snd = hub λ s → distrib (r s) .snd
  distrib (spokes r x i) .fst = spokes (λ s → distrib (r s) .fst) x i
  distrib (spokes r x i) .snd = spokes (λ s → distrib (r s) .snd) x i

  pair : n-Tr A (suc n) → n-Tr B (suc n) → n-Tr (A × B) (suc n)
  pair (inc x) (inc y)        = inc (x , y)
  pair (inc x) (hub r)        = hub λ s → pair (inc x) (r s)
  pair (inc x) (spokes r y i) = spokes (λ s → pair (inc x) (r s)) y i

  pair (hub r) y        = hub λ s → pair (r s) y
  pair (spokes r x i) y = spokes (λ s → pair (r s) y) x i

  open is-iso

  distrib-is-iso : is-iso distrib
  distrib-is-iso .inv (x , y)  = pair x y
  distrib-is-iso .rinv (x , y) = n-Tr-elim
    (λ x → ∀ y → distrib (pair x y) ≡ (x , y))
    (λ _ → Π-is-hlevel (suc n) λ x → Path-is-hlevel (suc n) (×-is-hlevel (suc n) hlevel! hlevel!))
    (λ x → n-Tr-elim _ (λ y → Path-is-hlevel (suc n) (×-is-hlevel (suc n) hlevel! hlevel!)) λ y → refl)
    x y
  distrib-is-iso .linv = n-Tr-elim! _ λ x → refl

  distrib-is-equiv = is-iso→is-equiv distrib-is-iso

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