Ian Ray, 23 July 2024

Minor modifications by Tom de Jong on 4 September 2024

Modifications made by Ian Ray on 26th September 2024.

Using records we define the general truncation of a type; this will include
a constructor, an induction principle and a computation rule
(up to identification). We then proceed to develop some machinery derived from
the induction principle and explore relationships, closure properties and
finally characterize the identity type of truncations. We explicitly assume
univalence locally for the characterization of identity types but not
globally as many important properties hold in the absence of univalence.

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import UF.FunExt

module UF.Truncations
        (fe : Fun-Ext)
       where

open import MLTT.Spartan hiding (_+_)

open import UF.Base
open import UF.Equiv
open import UF.PropTrunc
open import UF.Retracts
open import UF.Sets
open import UF.Subsingletons
open import UF.TruncationLevels
open import UF.TruncatedTypes fe
open import UF.Univalence
open import UF.Yoneda
open import Notation.Decimal

\end{code}

We define the general notion of truncation using record types.

\begin{code}

record general-truncations-exist : 𝓀ω where
 field
  βˆ₯_βˆ₯[_] : 𝓀 Μ‡ β†’ β„•β‚‹β‚‚ β†’ 𝓀 Μ‡
  βˆ₯βˆ₯β‚™-is-truncated : {X : 𝓀 Μ‡ } {n : β„•β‚‹β‚‚} β†’ βˆ₯ X βˆ₯[ n ] is n truncated
  ∣_∣[_] :  {X : 𝓀 Μ‡ } β†’ X β†’ (n : β„•β‚‹β‚‚) β†’ βˆ₯ X βˆ₯[ n ]
  βˆ₯βˆ₯β‚™-ind : {X : 𝓀 Μ‡ } {n : β„•β‚‹β‚‚} {P : βˆ₯ X βˆ₯[ n ] β†’ π“₯ Μ‡}
          β†’ ((s : βˆ₯ X βˆ₯[ n ]) β†’ (P s) is n truncated)
          β†’ ((x : X) β†’ P (∣ x ∣[ n ]))
          β†’ (s : βˆ₯ X βˆ₯[ n ]) β†’ P s
  βˆ₯βˆ₯β‚™-ind-comp : {X : 𝓀 Μ‡ } {n : β„•β‚‹β‚‚} {P : βˆ₯ X βˆ₯[ n ] β†’ π“₯ Μ‡ }
               β†’ (m : (s : βˆ₯ X βˆ₯[ n ]) β†’ (P s) is n truncated)
               β†’ (g : (x : X) β†’ P (∣ x ∣[ n ]))
               β†’ (x : X) β†’ βˆ₯βˆ₯β‚™-ind m g (∣ x ∣[ n ]) ＝ g x
 infix 0 βˆ₯_βˆ₯[_]
 infix 0 ∣_∣[_]

\end{code}

We now add some some machinery that will prove useful: truncation recursion
and uniqueness, induction/recursion for two arguments and all associated
computation rules.

\begin{code}

 βˆ₯βˆ₯β‚™-rec : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {n : β„•β‚‹β‚‚}
         β†’ Y is n truncated
         β†’ (X β†’ Y)
         β†’ βˆ₯ X βˆ₯[ n ] β†’ Y
 βˆ₯βˆ₯β‚™-rec m f s = βˆ₯βˆ₯β‚™-ind (Ξ» - β†’ m) f s

 βˆ₯βˆ₯β‚™-uniqueness : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {n : β„•β‚‹β‚‚}
                β†’ Y is n truncated
                β†’ (f g : βˆ₯ X βˆ₯[ n ] β†’ Y)
                β†’ ((x : X) β†’ f (∣ x ∣[ n ]) ＝ g (∣ x ∣[ n ]))
                β†’ f ∼ g
 βˆ₯βˆ₯β‚™-uniqueness m f g =
  βˆ₯βˆ₯β‚™-ind (Ξ» s β†’ truncation-levels-closed-under-Id m (f s) (g s))

 to-∼-of-maps-between-truncated-types : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {n : β„•β‚‹β‚‚}
                                      β†’ (f g : βˆ₯ X βˆ₯[ n ] β†’ βˆ₯ Y βˆ₯[ n ])
                                      β†’ ((x : X)
                                            β†’ f (∣ x ∣[ n ]) ＝ g (∣ x ∣[ n ]))
                                      β†’ f ∼ g
 to-∼-of-maps-between-truncated-types {𝓀} {π“₯} {X} {Y} {n} f g =
  βˆ₯βˆ₯β‚™-uniqueness βˆ₯βˆ₯β‚™-is-truncated f g

 βˆ₯βˆ₯β‚™-rec-comp : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {n : β„•β‚‹β‚‚}
              β†’ (m : Y is n truncated)
              β†’ (g : X β†’ Y)
              β†’ (x : X) β†’ βˆ₯βˆ₯β‚™-rec m g ∣ x ∣[ n ] ＝ g x
 βˆ₯βˆ₯β‚™-rec-comp m = βˆ₯βˆ₯β‚™-ind-comp (Ξ» - β†’ m)

 ∣_βˆ£β‚™ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {n : β„•β‚‹β‚‚}
      β†’ (f : X β†’ Y)
      β†’ X β†’ βˆ₯ Y βˆ₯[ n ]
 ∣_βˆ£β‚™ {_} {_} {_} {_} {n} f = ∣_∣[ n ] ∘ f

 βˆ₯_βˆ₯β‚™ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {n : β„•β‚‹β‚‚}
      β†’ (f : X β†’ Y)
      β†’ βˆ₯ X βˆ₯[ n ] β†’ βˆ₯ Y βˆ₯[ n ]
 βˆ₯ f βˆ₯β‚™ = βˆ₯βˆ₯β‚™-rec βˆ₯βˆ₯β‚™-is-truncated (∣ f βˆ£β‚™)

 βˆ₯βˆ₯β‚™-id-functorial : {X : 𝓀 Μ‡ } {n : β„•β‚‹β‚‚}
                   β†’ βˆ₯ id βˆ₯β‚™ ∼ id
 βˆ₯βˆ₯β‚™-id-functorial {_} {X} {n} =
  βˆ₯βˆ₯β‚™-uniqueness βˆ₯βˆ₯β‚™-is-truncated βˆ₯ id βˆ₯β‚™ id H
  where
   H : (x : X) β†’ βˆ₯ id βˆ₯β‚™ ∣ x ∣[ n ] ＝ ∣ x ∣[ n ]
   H = βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated ∣_∣[ n ]

 βˆ₯βˆ₯β‚™-composition-functorial : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } {n : β„•β‚‹β‚‚}
                            β†’ (f : X β†’ Y)
                            β†’ (g : Y β†’ Z)
                            β†’ βˆ₯ g ∘ f βˆ₯β‚™ ∼ βˆ₯ g βˆ₯β‚™ ∘ βˆ₯ f βˆ₯β‚™
 βˆ₯βˆ₯β‚™-composition-functorial {_} {_} {_} {X} {_} {_} {n} f g =
  βˆ₯βˆ₯β‚™-uniqueness βˆ₯βˆ₯β‚™-is-truncated βˆ₯ g ∘ f βˆ₯β‚™ (βˆ₯ g βˆ₯β‚™ ∘ βˆ₯ f βˆ₯β‚™) H
  where
   H : (x : X) β†’ βˆ₯ g ∘ f βˆ₯β‚™ ∣ x ∣[ n ] ＝ βˆ₯ g βˆ₯β‚™ (βˆ₯ f βˆ₯β‚™ ∣ x ∣[ n ])
   H x = βˆ₯ g ∘ f βˆ₯β‚™ ∣ x ∣[ n ]         ＝⟨ I ⟩
         ∣ g (f x) ∣[ n ]              ＝⟨ II ⟩
         βˆ₯ g βˆ₯β‚™ ∣ f x ∣[ n ]           ＝⟨ III ⟩
         βˆ₯ g βˆ₯β‚™ (βˆ₯ f βˆ₯β‚™ ∣ x ∣[ n ])    ∎
    where
     I = βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated ∣ g ∘ f βˆ£β‚™ x
     II = βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated ∣ g βˆ£β‚™ (f x) ⁻¹
     III = ap βˆ₯ g βˆ₯β‚™ (βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated ∣ f βˆ£β‚™ x) ⁻¹

 βˆ₯βˆ₯β‚™-preserves-homotopy' : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {n : β„•β‚‹β‚‚}
                        β†’ (f g : X β†’ Y)
                        β†’ f ∼ g
                        β†’ βˆ₯ f βˆ₯β‚™ ∘ ∣_∣[ n ] ∼ βˆ₯ g βˆ₯β‚™ ∘ ∣_∣[ n ]
 βˆ₯βˆ₯β‚™-preserves-homotopy' {_} {_} {X} {_} {n} f g H x =
  βˆ₯ f βˆ₯β‚™ ∣ x ∣[ n ]         ＝⟨ I ⟩
  ∣ f x ∣[ n ]              ＝⟨ II ⟩
  ∣ g x ∣[ n ]              ＝⟨ III ⟩
  βˆ₯ g βˆ₯β‚™ ∣ x ∣[ n ]         ∎
  where
   I = βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated ∣ f βˆ£β‚™ x
   II = ap ∣_∣[ n ] (H x)
   III = βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated ∣ g βˆ£β‚™ x ⁻¹

 βˆ₯βˆ₯β‚™-preserves-homotopy : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {n : β„•β‚‹β‚‚}
                        β†’ (f g : X β†’ Y)
                        β†’ f ∼ g
                        β†’ βˆ₯ f βˆ₯β‚™ ∼ βˆ₯ g βˆ₯β‚™
 βˆ₯βˆ₯β‚™-preserves-homotopy {_} {_} {X} {_} {n} f g H = G
  where
   G : (x : βˆ₯ X βˆ₯[ n ]) β†’ βˆ₯ f βˆ₯β‚™ x ＝ βˆ₯ g βˆ₯β‚™ x
   G = βˆ₯βˆ₯β‚™-uniqueness βˆ₯βˆ₯β‚™-is-truncated βˆ₯ f βˆ₯β‚™ βˆ₯ g βˆ₯β‚™
                      (βˆ₯βˆ₯β‚™-preserves-homotopy' f g H)

 βˆ₯βˆ₯β‚™-recβ‚‚ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } {n : β„•β‚‹β‚‚}
          β†’ Z is n truncated
          β†’ (X β†’ Y β†’ Z)
          β†’ βˆ₯ X βˆ₯[ n ] β†’ βˆ₯ Y βˆ₯[ n ] β†’ Z
 βˆ₯βˆ₯β‚™-recβ‚‚ m g = βˆ₯βˆ₯β‚™-rec (truncated-types-closed-under-β†’ m)
                        (Ξ» x β†’ βˆ₯βˆ₯β‚™-rec m (g x))

 βˆ₯βˆ₯β‚™-rec-compβ‚‚ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } {n : β„•β‚‹β‚‚}
               β†’ (m : Z is n truncated)
               β†’ (g : X β†’ Y β†’ Z)
               β†’ (x : X) β†’ (y : Y)
               β†’ βˆ₯βˆ₯β‚™-recβ‚‚ m g ∣ x ∣[ n ] ∣ y ∣[ n ] ＝ g x y
 βˆ₯βˆ₯β‚™-rec-compβ‚‚ {𝓀} {π“₯} {𝓦} {X} {Y} {Z} {n} m g x y =
  βˆ₯βˆ₯β‚™-recβ‚‚ m g ∣ x ∣[ n ] ∣ y ∣[ n ] ＝⟨ I ⟩
  βˆ₯βˆ₯β‚™-rec m (g x) ∣ y ∣[ n ]         ＝⟨ βˆ₯βˆ₯β‚™-rec-comp m (g x) y ⟩
  g x y                              ∎
   where
    I = happly (βˆ₯βˆ₯β‚™-rec-comp (truncated-types-closed-under-β†’ m)
                (Ξ» x β†’ βˆ₯βˆ₯β‚™-rec m (g x)) x)
               ∣ y ∣[ n ]

 abstract
  βˆ₯βˆ₯β‚™-indβ‚‚ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {n : β„•β‚‹β‚‚}
           β†’ (P : βˆ₯ X βˆ₯[ n ] β†’ βˆ₯ Y βˆ₯[ n ] β†’ 𝓦 Μ‡)
           β†’ ((u : βˆ₯ X βˆ₯[ n ]) β†’ (v : βˆ₯ Y βˆ₯[ n ]) β†’ (P u v) is n truncated)
           β†’ ((x : X) β†’ (y : Y) β†’ P (∣ x ∣[ n ]) (∣ y ∣[ n ]))
           β†’ (u : βˆ₯ X βˆ₯[ n ]) β†’ (v : βˆ₯ Y βˆ₯[ n ]) β†’ P u v
  βˆ₯βˆ₯β‚™-indβ‚‚ {𝓀} {π“₯} {𝓦} {X} {Y} {n} P m f =
   βˆ₯βˆ₯β‚™-ind (Ξ» u β†’ truncated-types-closed-under-Ξ  (P u) (m u))
           (Ξ» x β†’ βˆ₯βˆ₯β‚™-ind (Ξ» v β†’ m ∣ x ∣[ n ] v) (f x))

  βˆ₯βˆ₯β‚™-ind-compβ‚‚ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {n : β„•β‚‹β‚‚}
                β†’ (P : βˆ₯ X βˆ₯[ n ] β†’ βˆ₯ Y βˆ₯[ n ] β†’ 𝓦 Μ‡)
                β†’ (m : (u : βˆ₯ X βˆ₯[ n ]) β†’ (v : βˆ₯ Y βˆ₯[ n ])
                 β†’ (P u v) is n truncated)
                β†’ (g : (x : X) β†’ (y : Y) β†’ P (∣ x ∣[ n ]) (∣ y ∣[ n ]))
                β†’ (x : X) β†’ (y : Y)
                β†’ βˆ₯βˆ₯β‚™-indβ‚‚ P m g ∣ x ∣[ n ] ∣ y ∣[ n ] ＝ g x y
  βˆ₯βˆ₯β‚™-ind-compβ‚‚ {𝓀} {π“₯} {𝓦} {X} {Y} {n} P m g x y =
   βˆ₯βˆ₯β‚™-indβ‚‚ P m g ∣ x ∣[ n ] ∣ y ∣[ n ]     ＝⟨ I ⟩
   βˆ₯βˆ₯β‚™-ind (m ∣ x ∣[ n ]) (g x) ∣ y ∣[ n ]  ＝⟨ II ⟩
   g x y                                    ∎
    where
     I : βˆ₯βˆ₯β‚™-indβ‚‚ P m g ∣ x ∣[ n ] ∣ y ∣[ n ]
       ＝ βˆ₯βˆ₯β‚™-ind (m ∣ x ∣[ n ]) (g x) ∣ y ∣[ n ]
     I = happly
          (βˆ₯βˆ₯β‚™-ind-comp (Ξ» u β†’ truncated-types-closed-under-Ξ  (P u) (m u))
           (Ξ» x' β†’ βˆ₯βˆ₯β‚™-ind (m ∣ x' ∣[ n ]) (g x')) x)
          ∣ y ∣[ n ]
     II : βˆ₯βˆ₯β‚™-ind (m ∣ x ∣[ n ]) (g x) ∣ y ∣[ n ] ＝ g x y
     II = βˆ₯βˆ₯β‚™-ind-comp (m ∣ x ∣[ n ]) (g x) y

\end{code}

We characterize the first couple truncation levels.

(TODO: 1-type is a groupoid).

\begin{code}

 βˆ’2-trunc-is-contr : {X : 𝓀 Μ‡ } β†’ is-contr (βˆ₯ X βˆ₯[ βˆ’2 ])
 βˆ’2-trunc-is-contr = βˆ₯βˆ₯β‚™-is-truncated

 βˆ’1-trunc-is-prop : {X : 𝓀 Μ‡ } β†’ is-prop (βˆ₯ X βˆ₯[ βˆ’1 ])
 βˆ’1-trunc-is-prop = is-prop'-implies-is-prop βˆ₯βˆ₯β‚™-is-truncated

 0-trunc-is-set : {X : 𝓀 Μ‡ } β†’ is-set (βˆ₯ X βˆ₯[ 0 ])
 0-trunc-is-set {𝓀} {X} {x} {y} =
  is-prop'-implies-is-prop (βˆ₯βˆ₯β‚™-is-truncated x y)

\end{code}

We demonstrate the equivalence of -1-truncation and propositional truncation:
 βˆ₯ X βˆ₯[ βˆ’1 ] ≃ βˆ₯ X βˆ₯

\begin{code}

 module _ (pt : propositional-truncations-exist)
           where

  open propositional-truncations-exist pt

  βˆ’1-trunc-to-prop-trunc : {X : 𝓀 Μ‡} β†’ βˆ₯ X βˆ₯[ βˆ’1 ] β†’ βˆ₯ X βˆ₯
  βˆ’1-trunc-to-prop-trunc = βˆ₯βˆ₯β‚™-rec (is-prop-implies-is-prop' βˆ₯βˆ₯-is-prop) ∣_∣

  prop-trunc-to-βˆ’1-trunc : {X : 𝓀 Μ‡} β†’ βˆ₯ X βˆ₯ β†’ βˆ₯ X βˆ₯[ βˆ’1 ]
  prop-trunc-to-βˆ’1-trunc = βˆ₯βˆ₯-rec βˆ’1-trunc-is-prop (∣_∣[ βˆ’1 ])

  βˆ’1-trunc-≃-prop-trunc : {X : 𝓀 Μ‡}
                         β†’ (βˆ₯ X βˆ₯[ βˆ’1 ]) ≃ βˆ₯ X βˆ₯
  βˆ’1-trunc-≃-prop-trunc =
   logically-equivalent-props-are-equivalent βˆ’1-trunc-is-prop βˆ₯βˆ₯-is-prop
                                             βˆ’1-trunc-to-prop-trunc
                                             prop-trunc-to-βˆ’1-trunc

\end{code}

We define the canonical predecessor map and give a computation rule.

\begin{code}
 canonical-pred-map : {X : 𝓀 Μ‡} {n : β„•β‚‹β‚‚}
                    β†’ βˆ₯ X βˆ₯[ n + 1 ] β†’ βˆ₯ X βˆ₯[ n ]
 canonical-pred-map {𝓀} {X} {n} =
  βˆ₯βˆ₯β‚™-rec (truncation-levels-are-upper-closed βˆ₯βˆ₯β‚™-is-truncated) ∣_∣[ n ]

 canonical-pred-map-comp : {X : 𝓀 Μ‡} {n : β„•β‚‹β‚‚} (x : X)
                         β†’ canonical-pred-map (∣ x ∣[ n + 1 ]) ＝ (∣ x ∣[ n ])
 canonical-pred-map-comp {𝓀} {X} {n} =
  βˆ₯βˆ₯β‚™-rec-comp (truncation-levels-are-upper-closed βˆ₯βˆ₯β‚™-is-truncated) ∣_∣[ n ]

\end{code}

We show truncations are closed under equivalence and successive applications
of truncation.

TODO: closure under retracts, embeddings, etc. Note closure under equivalence
can be refactored to use closure under retracts.

\begin{code}

 truncation-closed-under-retract : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {n : β„•β‚‹β‚‚}
                                 β†’ retract Y of X
                                 β†’ retract βˆ₯ Y βˆ₯[ n ] of βˆ₯ X βˆ₯[ n ]
 truncation-closed-under-retract {_} {_} {X} {Y} {n} (r , s , H) =
  (βˆ₯ r βˆ₯β‚™ , βˆ₯ s βˆ₯β‚™ , G)
  where
   G : βˆ₯ r βˆ₯β‚™ ∘ βˆ₯ s βˆ₯β‚™ ∼ id
   G y = (βˆ₯ r βˆ₯β‚™ ∘ βˆ₯ s βˆ₯β‚™) y ＝⟨ I ⟩
         βˆ₯ r ∘ s βˆ₯β‚™ y        ＝⟨ II ⟩
         βˆ₯ id βˆ₯β‚™ y           ＝⟨ III ⟩
         y                   ∎
    where
     I = βˆ₯βˆ₯β‚™-composition-functorial s r y ⁻¹
     II = βˆ₯βˆ₯β‚™-preserves-homotopy (r ∘ s) id H y
     III = βˆ₯βˆ₯β‚™-id-functorial y

 truncation-closed-under-equiv : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {n : β„•β‚‹β‚‚}
                               β†’ X ≃ Y
                               β†’ βˆ₯ X βˆ₯[ n ] ≃ βˆ₯ Y βˆ₯[ n ]
 truncation-closed-under-equiv {𝓀} {π“₯} {X} {Y} {n} e = (f , (b , G) , (b , H))
  where
   f : βˆ₯ X βˆ₯[ n ] β†’ βˆ₯ Y βˆ₯[ n ]
   f = βˆ₯βˆ₯β‚™-rec βˆ₯βˆ₯β‚™-is-truncated (Ξ» x β†’ ∣ ⌜ e ⌝ x ∣[ n ])
   b : βˆ₯ Y βˆ₯[ n ] β†’ βˆ₯ X βˆ₯[ n ]
   b = βˆ₯βˆ₯β‚™-rec βˆ₯βˆ₯β‚™-is-truncated (Ξ» y β†’ ∣ ⌜ e ⌝⁻¹ y ∣[ n ])
   H : b ∘ f ∼ id
   H = to-∼-of-maps-between-truncated-types (b ∘ f) id H'
    where
     H' : (x : X) β†’ b (f (∣ x ∣[ n ])) ＝ (∣ x ∣[ n ])
     H' x = b (f (∣ x ∣[ n ]))           ＝⟨ I ⟩
            b (∣ ⌜ e ⌝ x ∣[ n ])         ＝⟨ II ⟩
            (∣ ⌜ e ⌝⁻¹ (⌜ e ⌝ x) ∣[ n ]) ＝⟨ III ⟩
            (∣ x ∣[ n ])                 ∎
      where
       I = ap b (βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated (Ξ» x β†’ ∣ (⌜ e ⌝ x) ∣[ n ]) x)
       II = βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated (Ξ» y β†’ ∣ (⌜ e ⌝⁻¹ y) ∣[ n ]) (⌜ e ⌝ x)
       III = ap (Ξ» x β†’ ∣ x ∣[ n ]) (inverses-are-retractions' e x)
   G : f ∘ b ∼ id
   G = to-∼-of-maps-between-truncated-types (f ∘ b) id G'
    where
     G' : (y : Y) β†’ f (b (∣ y ∣[ n ])) ＝ (∣ y ∣[ n ])
     G' y = f (b (∣ y ∣[ n ]))           ＝⟨ I ⟩
            f (∣ (⌜ e ⌝⁻¹ y) ∣[ n ])     ＝⟨ II ⟩
            (∣ ⌜ e ⌝ (⌜ e ⌝⁻¹ y) ∣[ n ]) ＝⟨ III ⟩
            (∣ y ∣[ n ])                 ∎
      where
       I = ap f (βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated (Ξ» y β†’ ∣ (⌜ e ⌝⁻¹ y) ∣[ n ]) y)
       II = βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated (Ξ» x β†’ ∣ ⌜ e ⌝ x ∣[ n ]) (⌜ e ⌝⁻¹ y)
       III = ap ∣_∣[ n ] (inverses-are-sections' e y)

 successive-truncations-equiv : {X : 𝓀 Μ‡} {n : β„•β‚‹β‚‚}
                              β†’ (βˆ₯ X βˆ₯[ n ]) ≃ (βˆ₯ (βˆ₯ X βˆ₯[ n + 1 ]) βˆ₯[ n ])
 successive-truncations-equiv {𝓀} {X} {n} = (f , (b , G) , (b , H))
  where
   f : βˆ₯ X βˆ₯[ n ] β†’ βˆ₯ βˆ₯ X βˆ₯[ n + 1 ] βˆ₯[ n ]
   f = βˆ₯βˆ₯β‚™-rec βˆ₯βˆ₯β‚™-is-truncated (Ξ» _ β†’ ∣ ∣ _ ∣[ n + 1 ] ∣[ n ])
   b : βˆ₯ βˆ₯ X βˆ₯[ succ n ] βˆ₯[ n ] β†’ βˆ₯ X βˆ₯[ n ]
   b = βˆ₯βˆ₯β‚™-rec βˆ₯βˆ₯β‚™-is-truncated canonical-pred-map
   G : f ∘ b ∼ id
   G = βˆ₯βˆ₯β‚™-uniqueness βˆ₯βˆ₯β‚™-is-truncated (f ∘ b) id
        (βˆ₯βˆ₯β‚™-uniqueness
          (truncation-levels-are-upper-closed βˆ₯βˆ₯β‚™-is-truncated)
          (f ∘ b ∘ ∣_∣[ n ])
          ∣_∣[ n ]
          G')
    where
     G' : (x : X)
        β†’ f (b (∣ ∣ x ∣[ n + 1 ] ∣[ n ])) ＝ (∣ ∣ x ∣[ n + 1 ] ∣[ n ])
     G' x = f (b (∣ ∣ x ∣[ n + 1 ] ∣[ n ]))         ＝⟨ I ⟩
            f (canonical-pred-map (∣ x ∣[ n + 1 ])) ＝⟨ II ⟩
            f (∣ x ∣[ n ])                          ＝⟨ III ⟩
            (∣ ∣ x ∣[ n + 1 ] ∣[ n ])               ∎
      where
       I = ap f (βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated canonical-pred-map
                              (∣ x ∣[ n + 1 ]))
       II = ap f (canonical-pred-map-comp x)
       III = βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated (Ξ» _ β†’ ∣ ∣ _ ∣[ n + 1 ] ∣[ n ]) x
   H : b ∘ f ∼ id
   H = βˆ₯βˆ₯β‚™-uniqueness βˆ₯βˆ₯β‚™-is-truncated (b ∘ f) id H'
    where
     H' : (x : X) β†’ b (f (∣ x ∣[ n ])) ＝ (∣ x ∣[ n ])
     H' x = b (f (∣ x ∣[ n ]))                   ＝⟨ I ⟩
            b (∣ ∣ x ∣[ n + 1 ] ∣[ n ])          ＝⟨ II ⟩
            canonical-pred-map (∣ x ∣[ n + 1 ])  ＝⟨ canonical-pred-map-comp x ⟩
            (∣ x ∣[ n ])                          ∎
      where
       I = ap b (βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated (Ξ» _ β†’ ∣ ∣ _ ∣[ n + 1 ] ∣[ n ]) x)
       II = βˆ₯βˆ₯β‚™-rec-comp βˆ₯βˆ₯β‚™-is-truncated canonical-pred-map (∣ x ∣[ n + 1 ])

\end{code}

We now define an equivalence that characterizes the truncated identity type
under the assumption of univalence. The following proof was inspired by
the agda unimath library -- although the development there is more thorough --
for details see: https://unimath.github.io/agda-unimath/foundation.truncations.

\begin{code}

 canonical-identity-trunc-map : {X : 𝓀 Μ‡} {x x' : X} {n : β„•β‚‹β‚‚}
                              β†’ βˆ₯ x ＝ x' βˆ₯[ n ]
                              β†’ ∣ x ∣[ n + 1 ] ＝ ∣ x' ∣[ n + 1 ]
 canonical-identity-trunc-map {𝓀} {X} {x} {x'} {n} =
  βˆ₯βˆ₯β‚™-rec (βˆ₯βˆ₯β‚™-is-truncated ∣ x ∣[ n + 1 ] ∣ x' ∣[ n + 1 ])
          (ap ∣_∣[ n + 1 ])

 module _ {X : 𝓀 Μ‡} {n : β„•β‚‹β‚‚}
          (ua : is-univalent 𝓀) (x : X)
           where

  trunc-id-family : βˆ₯ X βˆ₯[ n + 1 ] β†’ 𝕋 n 𝓀
  trunc-id-family = βˆ₯βˆ₯β‚™-rec (𝕋-is-of-next-truncation-level ua)
                            (Ξ» x' β†’ (βˆ₯ x ＝ x' βˆ₯[ n ] , βˆ₯βˆ₯β‚™-is-truncated))

  trunc-id-family-type : βˆ₯ X βˆ₯[ n + 1 ] β†’ 𝓀 Μ‡
  trunc-id-family-type = pr₁ ∘ trunc-id-family

  trunc-id-family-level : (v : βˆ₯ X βˆ₯[ n + 1 ])
                        β†’ (trunc-id-family-type v) is n truncated
  trunc-id-family-level = prβ‚‚ ∘ trunc-id-family

  trunc-id-family-computes : (x' : X)
                           β†’ trunc-id-family-type ∣ x' ∣[ n + 1 ]
                           ＝ βˆ₯ x ＝ x' βˆ₯[ n ]
  trunc-id-family-computes x' =
    ap pr₁ (βˆ₯βˆ₯β‚™-rec-comp (𝕋-is-of-next-truncation-level ua)
                         (Ξ» x' β†’ (βˆ₯ x ＝ x' βˆ₯[ n ] , βˆ₯βˆ₯β‚™-is-truncated))
                         x')

  trunc-id-forward-map : (x' : X)
                       β†’ trunc-id-family-type ∣ x' ∣[ n + 1 ]
                       β†’ βˆ₯ x ＝ x' βˆ₯[ n ]
  trunc-id-forward-map x' = transport id (trunc-id-family-computes x')

  trunc-id-backward-map : (x' : X)
                        β†’ βˆ₯ x ＝ x' βˆ₯[ n ]
                        β†’ trunc-id-family-type ∣ x' ∣[ n + 1 ]
  trunc-id-backward-map x' = transport⁻¹ id (trunc-id-family-computes x')

  trunc-id-back-is-retraction
   : (x' : X)
   β†’ trunc-id-backward-map x' ∘ trunc-id-forward-map x' ∼ id
  trunc-id-back-is-retraction x' q =
   forth-and-back-transport (trunc-id-family-computes x')

  refl-trunc-id-family : trunc-id-family-type ∣ x ∣[ n + 1 ]
  refl-trunc-id-family = trunc-id-backward-map x ∣ refl ∣[ n ]

  identity-on-trunc-to-family : (v : βˆ₯ X βˆ₯[ n + 1 ])
                              β†’ ∣ x ∣[ n + 1 ] ＝ v
                              β†’ trunc-id-family-type v
  identity-on-trunc-to-family .(∣ x ∣[ n + 1 ]) refl = refl-trunc-id-family

  trunc-id-family-is-identity-system : is-contr (Ξ£ trunc-id-family-type)
  trunc-id-family-is-identity-system =
   ((∣ x ∣[ n + 1 ] , refl-trunc-id-family) , trunc-id-fam-is-central)
   where
    I : (x' : X) (p : x ＝ x')
      β†’ (∣ x ∣[ n + 1 ] , refl-trunc-id-family)
       ＝[ Σ trunc-id-family-type ]
        (∣ x' ∣[ n + 1 ] , trunc-id-backward-map x' ∣ p ∣[ n ])
    I x' refl = refl

    II : (x' : X) (q' : βˆ₯ x ＝ x' βˆ₯[ n ])
       β†’ (∣ x ∣[ n + 1 ] , refl-trunc-id-family)
        ＝[ Σ trunc-id-family-type ]
         (∣ x' ∣[ n + 1 ] , trunc-id-backward-map x' q')
    II x' = βˆ₯βˆ₯β‚™-ind (Ξ» s β†’ truncated-types-closed-under-Ξ£
                            trunc-id-family-type
                            βˆ₯βˆ₯β‚™-is-truncated
                            (Ξ» v β†’ truncation-levels-are-upper-closed
                                    (trunc-id-family-level v))
                            (∣ x ∣[ n + 1 ] , refl-trunc-id-family)
                            (∣ x' ∣[ n + 1 ] , trunc-id-backward-map x' s))
                      (I x')

    III : (x' : X) (q : trunc-id-family-type ∣ x' ∣[ n + 1 ])
        β†’ (∣ x ∣[ n + 1 ] , refl-trunc-id-family)
          ＝[ Σ trunc-id-family-type ]
          (∣ x' ∣[ n + 1 ] , q)
    III x' q = transport (Ξ» - β†’ (∣ x ∣[ n + 1 ] , refl-trunc-id-family)
                                ＝[ Σ trunc-id-family-type ]
                                (∣ x' ∣[ n + 1 ] , -))
                         (trunc-id-back-is-retraction x' q)
                         (II x' (trunc-id-forward-map x' q))

    IV : (v : βˆ₯ X βˆ₯[ n + 1 ]) (q : trunc-id-family-type v)
       β†’ (∣ x ∣[ n + 1 ] , refl-trunc-id-family) ＝ (v , q)
    IV =
     βˆ₯βˆ₯β‚™-ind
      (Ξ» s β†’ truncated-types-closed-under-Ξ 
              (Ξ» q β†’ (∣ x ∣[ n + 1 ] , refl-trunc-id-family) ＝ (s , q))
              (Ξ» q β†’ truncated-types-closed-under-Ξ£
                      trunc-id-family-type
                       (truncation-levels-are-upper-closed βˆ₯βˆ₯β‚™-is-truncated)
                       (Ξ» v β†’ truncation-levels-are-upper-closed
                               (truncation-levels-are-upper-closed
                                 (trunc-id-family-level v)))
                       (∣ x ∣[ n + 1 ] , refl-trunc-id-family)
                       (s , q)))
              III

    trunc-id-fam-is-central : is-central (Ξ£ trunc-id-family-type)
                                         (∣ x ∣[ n + 1 ] , refl-trunc-id-family)
    trunc-id-fam-is-central (v , q) = IV v q

 trunc-identity-characterization : {X : 𝓀 Μ‡} {n : β„•β‚‹β‚‚}
                                 β†’ (ua : is-univalent 𝓀)
                                 β†’ (x : X) (v : βˆ₯ X βˆ₯[ n + 1 ])
                                 β†’ (∣ x ∣[ n + 1 ] ＝ v)
                                 ≃ trunc-id-family-type ua x v
 trunc-identity-characterization {𝓀} {X} {n} ua x v =
  (identity-on-trunc-to-family ua x v ,
   Yoneda-Theorem-forth ∣ x ∣[ n + 1 ]
    (identity-on-trunc-to-family ua x)
    (trunc-id-family-is-identity-system ua x) v)

 eliminated-trunc-identity-char : {X : 𝓀 Μ‡} {x x' : X} {n : β„•β‚‹β‚‚}
                                β†’ (ua : is-univalent 𝓀)
                                β†’ βˆ₯ x ＝ x' βˆ₯[ n ]
                                ≃ (∣ x ∣[ n + 1 ] ＝ ∣ x' ∣[ n + 1 ])
 eliminated-trunc-identity-char {𝓀} {X} {x} {x'} {n} ua =
  ≃-comp (idtoeq βˆ₯ x ＝ x' βˆ₯[ n ]
                 (trunc-id-family-type ua x ∣ x' ∣[ n + 1 ])
                 (trunc-id-family-computes ua x x' ⁻¹))
         (≃-sym (trunc-identity-characterization ua x ∣ x' ∣[ n + 1 ]))

 forth-trunc-id-char : {X : 𝓀 Μ‡} {x x' : X} {n : β„•β‚‹β‚‚}
                     β†’ (ua : is-univalent 𝓀)
                     β†’ βˆ₯ x ＝ x' βˆ₯[ n ]
                     β†’ (∣ x ∣[ n + 1 ] ＝ ∣ x' ∣[ n + 1 ])
 forth-trunc-id-char ua = ⌜ eliminated-trunc-identity-char ua ⌝

\end{code}

We show that the existence of propositional truncation follows from the existence
of general truncations. Notice this implication manifests as a function between
record types.

\begin{code}

general-truncations-give-propositional-truncations : general-truncations-exist
                                                   β†’ propositional-truncations-exist
general-truncations-give-propositional-truncations te = record
 { βˆ₯_βˆ₯        = βˆ₯_βˆ₯[ βˆ’1 ]
 ; βˆ₯βˆ₯-is-prop = is-prop'-implies-is-prop βˆ₯βˆ₯β‚™-is-truncated
 ; ∣_∣        = ∣_∣[ βˆ’1 ]
 ; βˆ₯βˆ₯-rec     = Ξ» - β†’ βˆ₯βˆ₯β‚™-rec (is-prop-implies-is-prop' -)
 }
 where
  open general-truncations-exist te

\end{code}