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 $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)

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

inc (x) \equiv_{∥ A ∥_{2 + n}} y,

so we will, for every $x : A,$ define a type family $code (x) : ∥ A ∥_{2 + n} \to Type,$ where the fibre of $code (x)$ over $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 $Type$ itself is not an $n -type$ for any $n .$ We salvage our definition by instead mapping into $(1 + n) - Type,$ which is a $(2 + n) -type.$

  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 $∥ 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' = 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 = 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 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 = 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.inv = 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.inv = 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 _)

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