module Homotopy.Truncation where

General truncationsπŸ”—

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:Sn→Af : S^n \to A is equivalently some loop in AA1, we can characterise the trivial loops as the constant functions Sn→AS^n \to A. Correspondingly, if every function Sn→AS^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:Snβ†’Af : S^n \to A as being a β€œhubs-and-spokes” construction. Geometrically, a trivial loop f:Snβ†’Af : 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)

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)≑βˆ₯Aβˆ₯2+ny, \mathrm{inc}(x) \equiv_{\|A\|_{2+n}} y,

so we will, for every x:Ax : A, define a type family code(x):βˆ₯Aβˆ₯2+nβ†’Type\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 βˆ₯x≑yβˆ₯1+n\|x \equiv y\|_{1+n}. However, induction principle for βˆ₯Aβˆ₯2+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 βˆ₯Aβˆ₯n+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 _))
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

  1. Any map f:Snβ†’Af : S^n \to A can be made basepoint-preserving by letting AA be based at f(N)f(N).β†©οΈŽ