<!--
```agda
open import 1Lab.Prelude

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

open import Homotopy.Space.Suspension
open import Homotopy.Space.Sphere
```
-->

```agda
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$[^someloop], 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!

[equivalence]: Homotopy.Base.html#loop-spaces-are-equivalently-based-maps-out-of-spheres
[h-levels]: 1Lab.HLevel.html
[^someloop]: Any map $f : S^n \to A$ can be made basepoint-preserving by
letting $A$ be based at $f(N)$.

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.

```agda
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)
```

<!--
```agda
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)
```
-->

:::{.definition #truncation}
Using this idea, we can define a general _$n$-truncation_ type, as a
joint generalisation of the [[propositional|propositional truncation]]
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 `hub`{.Agda}s and `spokes`{.Agda} for any $n$-sphere drawn on
the $n$-truncation of $A$. The result is the universal $n$-type
admitting a map from $A$.
:::

[set]: Data.Set.Truncation.html

```agda
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.

```agda
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
```

<!--
```agda
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`{.Agda}, we have the recursion
principle, where the type we are eliminating into is constant.

```agda
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$:

```agda
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

$$
\rm{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 \ty$, where the fibre of $\mathrm{code}(x)$ over
$\rm{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 $\ty$ itself is not an $n$-type for any $n$. We salvage our
definition by instead mapping into $(1+n)\text{-}\ty$, which _is_ a
$(2+n)$-type.

```agda
  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`{.Agda id=J} and the induction principle for $\|A\|_{n+2}$.

```agda
  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 _))
```

```agda
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
```

```agda
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 _)
```
