# Truncations

Content created by Egbert Rijke, Fredrik Bakke, Elisabeth Stenholm, Jonathan Prieto-Cubides and Tom de Jong.

Created on 2022-03-08.

module foundation.truncations where

Imports
open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.functoriality-dependent-function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.truncated-types
open import foundation.universal-property-dependent-pair-types
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.contractible-maps
open import foundation-core.equality-dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.propositions
open import foundation-core.torsorial-type-families
open import foundation-core.truncation-levels
open import foundation-core.universal-property-truncation


## Idea

We postulate the existence of truncations.

## Postulates

postulate
type-trunc : {l : Level} (k : 𝕋) → UU l → UU l

postulate
is-trunc-type-trunc :
{l : Level} {k : 𝕋} {A : UU l} → is-trunc k (type-trunc k A)

trunc : {l : Level} (k : 𝕋) → UU l → Truncated-Type l k
pr1 (trunc k A) = type-trunc k A
pr2 (trunc k A) = is-trunc-type-trunc

postulate
unit-trunc : {l : Level} {k : 𝕋} {A : UU l} → A → type-trunc k A

postulate
is-truncation-trunc :
{l : Level} {k : 𝕋} {A : UU l} →
is-truncation (trunc k A) unit-trunc

equiv-universal-property-trunc :
{l1 l2 : Level} {k : 𝕋} (A : UU l1) (B : Truncated-Type l2 k) →
(type-trunc k A → type-Truncated-Type B) ≃ (A → type-Truncated-Type B)
pr1 (equiv-universal-property-trunc A B) = precomp-Trunc unit-trunc B
pr2 (equiv-universal-property-trunc A B) = is-truncation-trunc B


## Properties

### The n-truncations satisfy the universal property of n-truncations

universal-property-trunc :
{l1 : Level} (k : 𝕋) (A : UU l1) →
universal-property-truncation (trunc k A) unit-trunc
universal-property-trunc k A =
universal-property-truncation-is-truncation
( trunc k A)
( unit-trunc)
( is-truncation-trunc)

module _
{l1 l2 : Level} {k : 𝕋} {A : UU l1}
where

apply-universal-property-trunc :
(B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) →
Σ ( type-trunc k A → type-Truncated-Type B)
( λ h → h ∘ unit-trunc ~ f)
apply-universal-property-trunc B f =
center
( universal-property-truncation-is-truncation
( trunc k A)
( unit-trunc)
( is-truncation-trunc)
( B)
( f))

map-universal-property-trunc :
(B : Truncated-Type l2 k) → (A → type-Truncated-Type B) →
type-trunc k A → type-Truncated-Type B
map-universal-property-trunc B f =
pr1 (apply-universal-property-trunc B f)

triangle-universal-property-trunc :
(B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) →
map-universal-property-trunc B f ∘ unit-trunc ~ f
triangle-universal-property-trunc B f =
pr2 (apply-universal-property-trunc B f)


### The n-truncations satisfy the dependent universal property of n-truncations

module _
{l1 : Level} {k : 𝕋} {A : UU l1}
where

dependent-universal-property-trunc :
dependent-universal-property-truncation (trunc k A) unit-trunc
dependent-universal-property-trunc =
dependent-universal-property-truncation-is-truncation
( trunc k A)
( unit-trunc)
( is-truncation-trunc)

equiv-dependent-universal-property-trunc :
{l2 : Level} (B : type-trunc k A → Truncated-Type l2 k) →
((x : type-trunc k A) → type-Truncated-Type (B x)) ≃
((a : A) → type-Truncated-Type (B (unit-trunc a)))
pr1 (equiv-dependent-universal-property-trunc B) =
precomp-Π-Truncated-Type unit-trunc B
pr2 (equiv-dependent-universal-property-trunc B) =
dependent-universal-property-trunc B

unique-dependent-function-trunc :
{l2 : Level} (B : type-trunc k A → Truncated-Type l2 k)
(f : (x : A) → type-Truncated-Type (B (unit-trunc x))) →
is-contr
( Σ ( (x : type-trunc k A) → type-Truncated-Type (B x))
( λ h → (h ∘ unit-trunc) ~ f))
unique-dependent-function-trunc B f =
is-contr-equiv'
( fiber (precomp-Π-Truncated-Type unit-trunc B) f)
( equiv-tot
( λ h → equiv-funext))
( is-contr-map-is-equiv
( dependent-universal-property-trunc B)
( f))

apply-dependent-universal-property-trunc :
{l2 : Level} (B : type-trunc k A → Truncated-Type l2 k) →
(f : (x : A) → type-Truncated-Type (B (unit-trunc x))) →
Σ ( (x : type-trunc k A) → type-Truncated-Type (B x))
( λ h → (h ∘ unit-trunc) ~ f)
apply-dependent-universal-property-trunc B f =
center (unique-dependent-function-trunc B f)

function-dependent-universal-property-trunc :
{l2 : Level} (B : type-trunc k A → Truncated-Type l2 k) →
(f : (x : A) → type-Truncated-Type (B (unit-trunc x))) →
(x : type-trunc k A) → type-Truncated-Type (B x)
function-dependent-universal-property-trunc B f =
pr1 (apply-dependent-universal-property-trunc B f)

htpy-dependent-universal-property-trunc :
{l2 : Level} (B : type-trunc k A → Truncated-Type l2 k) →
(f : (x : A) → type-Truncated-Type (B (unit-trunc x))) →
( function-dependent-universal-property-trunc B f ∘ unit-trunc) ~ f
htpy-dependent-universal-property-trunc B f =
pr2 (apply-dependent-universal-property-trunc B f)


### Families of k-truncated-types over k+1-truncations of types

unique-truncated-fam-trunc :
{l1 l2 : Level} {k : 𝕋} {A : UU l1} →
(B : A → Truncated-Type l2 k) →
is-contr
( Σ ( type-trunc (succ-𝕋 k) A → Truncated-Type l2 k)
( λ C → (x : A) → type-equiv-Truncated-Type (B x) (C (unit-trunc x))))
unique-truncated-fam-trunc {l1} {l2} {k} {A} B =
is-contr-equiv'
( Σ ( type-trunc (succ-𝕋 k) A → Truncated-Type l2 k)
( λ C → (C ∘ unit-trunc) ~ B))
( equiv-tot
( λ C →
equiv-Π-equiv-family
( λ x →
( extensionality-Truncated-Type (B x) (C (unit-trunc x))) ∘e
( equiv-inv (C (unit-trunc x)) (B x)))))
( universal-property-trunc
( succ-𝕋 k)
( A)
( Truncated-Type-Truncated-Type l2 k)
( B))

module _
{l1 l2 : Level} {k : 𝕋} {A : UU l1} (B : A → Truncated-Type l2 k)
where

truncated-fam-trunc : type-trunc (succ-𝕋 k) A → Truncated-Type l2 k
truncated-fam-trunc =
pr1 (center (unique-truncated-fam-trunc B))

fam-trunc : type-trunc (succ-𝕋 k) A → UU l2
fam-trunc = type-Truncated-Type ∘ truncated-fam-trunc

compute-truncated-fam-trunc :
(x : A) →
type-equiv-Truncated-Type (B x) (truncated-fam-trunc (unit-trunc x))
compute-truncated-fam-trunc =
pr2 (center (unique-truncated-fam-trunc B))

map-compute-truncated-fam-trunc :
(x : A) → type-Truncated-Type (B x) → (fam-trunc (unit-trunc x))
map-compute-truncated-fam-trunc x =
map-equiv (compute-truncated-fam-trunc x)

total-truncated-fam-trunc : UU (l1 ⊔ l2)
total-truncated-fam-trunc = Σ (type-trunc (succ-𝕋 k) A) fam-trunc

module _
{l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} (B : A → Truncated-Type l2 k)
( C : total-truncated-fam-trunc B → Truncated-Type l3 k)
( f :
( x : A)
( y : type-Truncated-Type (B x)) →
type-Truncated-Type
( C (unit-trunc x , map-equiv (compute-truncated-fam-trunc B x) y)))
where

dependent-universal-property-total-truncated-fam-trunc :
is-contr
( Σ ( (t : total-truncated-fam-trunc B) → type-Truncated-Type (C t))
( λ h →
(x : A) (y : type-Truncated-Type (B x)) →
Id
( h (unit-trunc x , map-compute-truncated-fam-trunc B x y))
( f x y)))
dependent-universal-property-total-truncated-fam-trunc =
is-contr-equiv _
( equiv-Σ
( λ g →
(x : A) →
Id
( g (unit-trunc x))
( map-equiv-Π
( λ u → type-Truncated-Type (C (unit-trunc x , u)))
( compute-truncated-fam-trunc B x)
( λ u → id-equiv)
( f x)))
( equiv-ev-pair)
( λ g →
equiv-Π-equiv-family
( λ x →
( inv-equiv equiv-funext) ∘e
( equiv-Π
( λ y →
Id
( g (unit-trunc x , y))
( map-equiv-Π
( λ u →
type-Truncated-Type (C (unit-trunc x , u)))
( compute-truncated-fam-trunc B x)
( λ u → id-equiv)
( f x)
( y)))
( compute-truncated-fam-trunc B x)
( λ y →
equiv-concat'
( g (unit-trunc x , map-compute-truncated-fam-trunc B x y))
( inv
( compute-map-equiv-Π
( λ u → type-Truncated-Type (C (unit-trunc x , u)))
( compute-truncated-fam-trunc B x)
( λ y → id-equiv)
( f x)
( y))))))))
( unique-dependent-function-trunc
( λ y →
truncated-type-succ-Truncated-Type k
( Π-Truncated-Type k
( truncated-fam-trunc B y)
( λ u → C (y , u))))
( λ y →
map-equiv-Π
( λ u → type-Truncated-Type (C (unit-trunc y , u)))
( compute-truncated-fam-trunc B y)
( λ u → id-equiv)
( f y)))

function-dependent-universal-property-total-truncated-fam-trunc :
(t : total-truncated-fam-trunc B) → type-Truncated-Type (C t)
function-dependent-universal-property-total-truncated-fam-trunc =
pr1 (center dependent-universal-property-total-truncated-fam-trunc)

htpy-dependent-universal-property-total-truncated-fam-trunc :
(x : A) (y : type-Truncated-Type (B x)) →
Id
( function-dependent-universal-property-total-truncated-fam-trunc
( unit-trunc x , map-compute-truncated-fam-trunc B x y))
( f x y)
htpy-dependent-universal-property-total-truncated-fam-trunc =
pr2 (center dependent-universal-property-total-truncated-fam-trunc)


### An n-truncated type is equivalent to its n-truncation

module _
{l : Level} {k : 𝕋} (A : Truncated-Type l k)
where

map-inv-unit-trunc :
type-trunc k (type-Truncated-Type A) → type-Truncated-Type A
map-inv-unit-trunc = map-universal-property-trunc A id

is-retraction-map-inv-unit-trunc :
( map-inv-unit-trunc ∘ unit-trunc) ~ id
is-retraction-map-inv-unit-trunc = triangle-universal-property-trunc A id

is-section-map-inv-unit-trunc :
( unit-trunc ∘ map-inv-unit-trunc) ~ id
is-section-map-inv-unit-trunc =
htpy-eq
( pr1
( pair-eq-Σ
( eq-is-prop'
( is-trunc-succ-is-trunc
( neg-two-𝕋)
( universal-property-trunc
( k)
( type-Truncated-Type A)
( trunc k (type-Truncated-Type A))
( unit-trunc)))
( unit-trunc ∘ map-inv-unit-trunc ,
unit-trunc ·l is-retraction-map-inv-unit-trunc)
( id , refl-htpy))))

is-equiv-unit-trunc : is-equiv unit-trunc
is-equiv-unit-trunc =
is-equiv-is-invertible
map-inv-unit-trunc
is-section-map-inv-unit-trunc
is-retraction-map-inv-unit-trunc

equiv-unit-trunc :
type-Truncated-Type A ≃ type-trunc k (type-Truncated-Type A)
pr1 equiv-unit-trunc = unit-trunc
pr2 equiv-unit-trunc = is-equiv-unit-trunc


### A contractible type is equivalent to its k-truncation

module _
{l : Level} (k : 𝕋) (A : UU l)
where

is-equiv-unit-trunc-is-contr : is-contr A → is-equiv unit-trunc
is-equiv-unit-trunc-is-contr c =
is-equiv-unit-trunc (A , is-trunc-is-contr k c)


### Truncation is idempotent

module _
{l : Level} (k : 𝕋) (A : UU l)
where

idempotent-trunc : type-trunc k (type-trunc k A) ≃ type-trunc k A
idempotent-trunc = inv-equiv (equiv-unit-trunc (trunc k A))


### Characterization of the identity types of truncations

module _
{l : Level} (k : 𝕋) {A : UU l} (a : A)
where

Eq-trunc-Truncated-Type : type-trunc (succ-𝕋 k) A → Truncated-Type l k
Eq-trunc-Truncated-Type = truncated-fam-trunc (λ y → trunc k (a ＝ y))

Eq-trunc : type-trunc (succ-𝕋 k) A → UU l
Eq-trunc x = type-Truncated-Type (Eq-trunc-Truncated-Type x)

compute-Eq-trunc : (x : A) → type-trunc k (a ＝ x) ≃ Eq-trunc (unit-trunc x)
compute-Eq-trunc = compute-truncated-fam-trunc (λ y → trunc k (a ＝ y))

map-compute-Eq-trunc :
(x : A) → type-trunc k (a ＝ x) → Eq-trunc (unit-trunc x)
map-compute-Eq-trunc x = map-equiv (compute-Eq-trunc x)

refl-Eq-trunc : Eq-trunc (unit-trunc a)
refl-Eq-trunc = map-compute-Eq-trunc a (unit-trunc refl)

refl-compute-Eq-trunc :
map-compute-Eq-trunc a (unit-trunc refl) ＝ refl-Eq-trunc
refl-compute-Eq-trunc = refl

is-torsorial-Eq-trunc : is-torsorial Eq-trunc
pr1 (pr1 is-torsorial-Eq-trunc) = unit-trunc a
pr2 (pr1 is-torsorial-Eq-trunc) = refl-Eq-trunc
pr2 is-torsorial-Eq-trunc =
function-dependent-universal-property-total-truncated-fam-trunc
( λ y → trunc k (a ＝ y))
( Id-Truncated-Type
( Σ-Truncated-Type
( trunc (succ-𝕋 k) A)
( λ b →
truncated-type-succ-Truncated-Type k
( Eq-trunc-Truncated-Type b)))
( unit-trunc a , refl-Eq-trunc))
( λ y →
function-dependent-universal-property-trunc
( λ q →
Id-Truncated-Type
( Σ-Truncated-Type
( trunc (succ-𝕋 k) A)
( λ y →
truncated-type-succ-Truncated-Type k
( Eq-trunc-Truncated-Type y)))
( unit-trunc a , refl-Eq-trunc)
( unit-trunc y , map-compute-Eq-trunc y q))
( r y))
where
r :
(y : A) (p : a ＝ y) →
Id
{ A = Σ (type-trunc (succ-𝕋 k) A) Eq-trunc}
( unit-trunc a , refl-Eq-trunc)
( unit-trunc y , (map-compute-Eq-trunc y (unit-trunc p)))
r .a refl = refl

Eq-eq-trunc : (x : type-trunc (succ-𝕋 k) A) → (unit-trunc a ＝ x) → Eq-trunc x
Eq-eq-trunc .(unit-trunc a) refl = refl-Eq-trunc

is-equiv-Eq-eq-trunc :
(x : type-trunc (succ-𝕋 k) A) → is-equiv (Eq-eq-trunc x)
is-equiv-Eq-eq-trunc =
fundamental-theorem-id
( is-torsorial-Eq-trunc)
( Eq-eq-trunc)

extensionality-trunc :
(x : type-trunc (succ-𝕋 k) A) → (unit-trunc a ＝ x) ≃ Eq-trunc x
pr1 (extensionality-trunc x) = Eq-eq-trunc x
pr2 (extensionality-trunc x) = is-equiv-Eq-eq-trunc x

effectiveness-trunc :
(x : A) →
type-trunc k (a ＝ x) ≃ (unit-trunc {k = succ-𝕋 k} a ＝ unit-trunc x)
effectiveness-trunc x =
inv-equiv (extensionality-trunc (unit-trunc x)) ∘e compute-Eq-trunc x

map-effectiveness-trunc :
(x : A) →
type-trunc k (a ＝ x) → (unit-trunc {k = succ-𝕋 k} a ＝ unit-trunc x)
map-effectiveness-trunc x = map-equiv (effectiveness-trunc x)

refl-effectiveness-trunc :
map-effectiveness-trunc a (unit-trunc refl) ＝ refl
refl-effectiveness-trunc =
is-retraction-map-inv-equiv (extensionality-trunc (unit-trunc a)) refl


### Truncations of Σ-types

module _
{l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : A → UU l2}
where

map-trunc-Σ :
type-trunc k (Σ A B) → type-trunc k (Σ A (λ x → type-trunc k (B x)))
map-trunc-Σ =
map-universal-property-trunc
( trunc k (Σ A (λ x → type-trunc k (B x))))
( λ (a , b) → unit-trunc (a , unit-trunc b))

map-inv-trunc-Σ :
type-trunc k (Σ A (λ x → type-trunc k (B x))) → type-trunc k (Σ A B)
map-inv-trunc-Σ =
map-universal-property-trunc
( trunc k (Σ A B))
( λ (a , |b|) →
map-universal-property-trunc
( trunc k (Σ A B))
( λ b → unit-trunc (a , b))
( |b|))

is-retraction-map-inv-trunc-Σ :
( map-inv-trunc-Σ ∘ map-trunc-Σ) ~ id
is-retraction-map-inv-trunc-Σ =
function-dependent-universal-property-trunc
( λ |ab| →
Id-Truncated-Type'
( trunc k (Σ A B))
( map-inv-trunc-Σ (map-trunc-Σ |ab|))
( |ab|))
( λ (a , b) →
( ap
( map-inv-trunc-Σ)
( triangle-universal-property-trunc _
( λ (a' , b') → unit-trunc (a' , unit-trunc b'))
( a , b))) ∙
( triangle-universal-property-trunc _
( λ (a' , |b'|) →
map-universal-property-trunc
( trunc k (Σ A B))
( λ b' → unit-trunc (a' , b'))
( |b'|))
( a , unit-trunc b) ∙
triangle-universal-property-trunc _
( λ b' → unit-trunc (a , b'))
( b)))

is-section-map-inv-trunc-Σ :
( map-trunc-Σ ∘ map-inv-trunc-Σ) ~ id
is-section-map-inv-trunc-Σ =
function-dependent-universal-property-trunc
( λ |a|b|| →
Id-Truncated-Type'
( trunc k (Σ A (λ x → type-trunc k (B x))))
( map-trunc-Σ (map-inv-trunc-Σ |a|b||))
( |a|b||))
( λ (a , |b|) →
function-dependent-universal-property-trunc
(λ |b'| →
Id-Truncated-Type'
( trunc k (Σ A (λ x → type-trunc k (B x))))
(map-trunc-Σ (map-inv-trunc-Σ (unit-trunc (a , |b'|))))
(unit-trunc (a , |b'|)))
(λ b →
ap map-trunc-Σ
(triangle-universal-property-trunc _
( λ (a' , |b'|) →
map-universal-property-trunc
( trunc k (Σ A B))
( λ b' → unit-trunc (a' , b'))
( |b'|))
( a , unit-trunc b)) ∙
(ap map-trunc-Σ
(triangle-universal-property-trunc
( trunc k (Σ A B))
( λ b' → unit-trunc (a , b'))
( b)) ∙
triangle-universal-property-trunc _
( λ (a' , b') → unit-trunc (a' , unit-trunc b'))
( a , b)))
( |b|))

equiv-trunc-Σ :
type-trunc k (Σ A B) ≃ type-trunc k (Σ A (λ x → type-trunc k (B x)))
pr1 equiv-trunc-Σ = map-trunc-Σ
pr2 equiv-trunc-Σ =
is-equiv-is-invertible
map-inv-trunc-Σ
is-section-map-inv-trunc-Σ
is-retraction-map-inv-trunc-Σ

inv-equiv-trunc-Σ :
type-trunc k (Σ A (λ x → type-trunc k (B x))) ≃ type-trunc k (Σ A B)
pr1 inv-equiv-trunc-Σ = map-inv-trunc-Σ
pr2 inv-equiv-trunc-Σ =
is-equiv-is-invertible
map-trunc-Σ
is-retraction-map-inv-trunc-Σ
is-section-map-inv-trunc-Σ