open import 1Lab.Prelude

open import Data.Nat.Base
open import Data.List using (_∷_ ; [])

open import Homotopy.Space.Suspension
open import Homotopy.Space.Sphere
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 is equivalently some loop in 1, we can characterise the trivial loops as the constant functions Correspondingly, if every function is trivial, this means that all in are trivial, so that is

We refer to a trivialisation of a map as being a β€œhubs-and-spokes” construction. Geometrically, a trivial loop can be understood as a map from the disc rather than the where the 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 go .snd N βˆ™ sym (spheres go .snd S) where
    go : Sⁿ⁻¹ 1 β†’ A
    go N = x
    go 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 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 what we can do is freely generate hubs and spokes for any drawn on the of The result is the universal admitting a map from 

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 has the right h-level, and proving that one can eliminate from it to 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
  H-Level-n-Tr : βˆ€ {β„“} {A : Type β„“} {n k} ⦃ _ : suc n ≀ k ⦄ β†’ H-Level (n-Tr A (suc n)) k
  H-Level-n-Tr {k = _} ⦃ p ⦄ = hlevel-instance $ is-hlevel-le _ _ p (n-Tr-is-hlevel _)

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
instance
  Inductive-n-Tr
    : βˆ€ {β„“ β„“' β„“m} {A : Type β„“} {n} {P : n-Tr A (suc n) β†’ Type β„“'} ⦃ i : Inductive (βˆ€ x β†’ P (inc x)) β„“m ⦄
    β†’ ⦃ _ : βˆ€ {x} β†’ H-Level (P x) (suc n) ⦄
    β†’ Inductive (βˆ€ x β†’ P x) β„“m
  Inductive-n-Tr ⦃ i ⦄ = record
    { from = Ξ» f β†’ n-Tr-elim _ (Ξ» x β†’ hlevel _) (i .Inductive.from f)
    }

n-Tr-elim!
  : βˆ€ {β„“ β„“'} {A : Type β„“} {n}
  β†’ (P : n-Tr A (suc n) β†’ Type β„“')
  β†’ ⦃ _ : βˆ€ {x} β†’ H-Level (P x) (suc n) ⦄
  β†’ (βˆ€ x β†’ P (inc x))
  β†’ βˆ€ x β†’ P x
n-Tr-elim! P f = n-Tr-elim P (Ξ» x β†’ hlevel _) f

n-Tr-rec!
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} {n}
  β†’ ⦃ hl : H-Level B (suc n) ⦄
  β†’ (A β†’ B) β†’ n-Tr A (suc n) β†’ B
n-Tr-rec! = n-Tr-elim (Ξ» _ β†’ _) (Ξ» _ β†’ hlevel _)

n-Tr-map
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} {n}
  β†’ (A β†’ B) β†’ n-Tr A (suc n) β†’ n-Tr B (suc n)
n-Tr-map f = n-Tr-rec! (inc ∘ f)

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 of is characterising its path spaces, at least for the inclusions of points from Identifications between (the images of) points in in the are equivalently identifications in 

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

so we will, for every define a type family where the fibre of over should be However, the induction principle for only allows us to map into while itself is not an for any We salvage our definition by instead mapping into which is a 

  code : (x : A) (y' : n-Tr A (2 + n)) β†’ n-Type _ (suc n)
  code x = n-Tr-rec! Ξ» 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 

  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' = elim! Ξ» x y β†’ ap inc

  rinv : βˆ€ x y β†’ is-right-inverse (decode' x y) (encode' x y)
  rinv = elim! Ξ» x y x=y β†’ 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 .fst f = f ∘ inc
n-Tr-univ n b-hl .snd = is-iso→is-equiv λ where
  .is-iso.from f β†’ n-Tr-rec b-hl f
  .is-iso.rinv f β†’ refl
  .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 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 .from (x , y)  = pair x y
  distrib-is-iso .rinv = elim! Ξ» x y β†’ refl
  distrib-is-iso .linv = n-Tr-elim! _ Ξ» x β†’ refl

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

n-Tr-Ξ£
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : A β†’ Type β„“'} {n}
  β†’ n-Tr (Ξ£ A B) (suc n) ≃ n-Tr (Ξ£ A Ξ» a β†’ n-Tr (B a) (suc n)) (suc n)
n-Tr-Σ {A = A} {B} {n} = Iso→Equiv is where
  is : Iso _ _
  is .fst = n-Tr-map (Ξ£-map id inc)
  is .snd .is-iso.from = n-Tr-rec! Ξ» (a , b) β†’ n-Tr-map (a ,_) b
  is .snd .is-iso.rinv = n-Tr-elim! _ Ξ» (a , b) β†’ n-Tr-elim! (Ξ» b β†’ n-Tr-map (Ξ£-map id inc) (n-Tr-map (a ,_) b) ≑ inc (a , b)) (Ξ» _ β†’ refl) b
  is .snd .is-iso.linv = n-Tr-elim! _ Ξ» _ β†’ refl

n-Tr-≃
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} {n}
  β†’ (e : A ≃ B) β†’ n-Tr A (suc n) ≃ n-Tr B (suc n)
n-Tr-≃ e = Isoβ†’Equiv is where
  is : Iso _ _
  is .fst = n-Tr-map (e .fst)
  is .snd .is-iso.from = n-Tr-map (Equiv.from e)
  is .snd .is-iso.rinv = elim! Ξ» _ β†’ ap inc (Equiv.Ξ΅ e _)
  is .snd .is-iso.linv = elim! Ξ» _ β†’ ap inc (Equiv.Ξ· e _)

  1. Any map can be made basepoint-preserving by letting be based at β†©οΈŽ