# The universal property of truncations

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-07-17.

module foundation-core.universal-property-truncation where

Imports
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.universal-property-equivalences
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.precomposition-functions
open import foundation-core.sections
open import foundation-core.truncated-types
open import foundation-core.truncation-levels
open import foundation-core.type-theoretic-principle-of-choice


## Idea

We say that a map f : A → B into a k-truncated type B is a k-truncation of A -- or that it satisfies the universal property of the k-truncation of A -- if any map g : A → C into a k-truncated type C extends uniquely along f to a map B → C.

## Definition

### The condition on a map to be a truncation

precomp-Trunc :
{l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : A → B)
(C : Truncated-Type l3 k) →
(B → type-Truncated-Type C) → (A → type-Truncated-Type C)
precomp-Trunc f C = precomp f (type-Truncated-Type C)

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

is-truncation : UUω
is-truncation =
{l : Level} (C : Truncated-Type l k) → is-equiv (precomp-Trunc f C)

equiv-is-truncation :
{l3 : Level} (H : is-truncation) (C : Truncated-Type l3 k) →
( type-Truncated-Type B → type-Truncated-Type C) ≃
( A → type-Truncated-Type C)
pr1 (equiv-is-truncation H C) = precomp-Trunc f C
pr2 (equiv-is-truncation H C) = H C


### The universal property of truncations

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

universal-property-truncation : UUω
universal-property-truncation =
{l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) →
is-contr (Σ (type-hom-Truncated-Type k B C) (λ h → h ∘ f ~ g))


### The dependent universal property of truncations

precomp-Π-Truncated-Type :
{l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : A → B)
(C : B → Truncated-Type l3 k) →
((b : B) → type-Truncated-Type (C b)) →
((a : A) → type-Truncated-Type (C (f a)))
precomp-Π-Truncated-Type f C h a = h (f a)

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

dependent-universal-property-truncation : UUω
dependent-universal-property-truncation =
{l : Level} (X : type-Truncated-Type B → Truncated-Type l k) →
is-equiv (precomp-Π-Truncated-Type f X)


## Properties

### Equivalences into k-truncated types are truncations

abstract
is-truncation-id :
{l1 : Level} {k : 𝕋} {A : UU l1} (H : is-trunc k A) →
is-truncation (A , H) id
is-truncation-id H B =
is-equiv-precomp-is-equiv id is-equiv-id (type-Truncated-Type B)

abstract
is-truncation-equiv :
{l1 l2 : Level} {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 k)
(e : A ≃ type-Truncated-Type B) →
is-truncation B (map-equiv e)
is-truncation-equiv B e C =
is-equiv-precomp-is-equiv
( map-equiv e)
( is-equiv-map-equiv e)
( type-Truncated-Type C)


### A map into a truncated type is a truncation if and only if it satisfies the universal property of the truncation

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

abstract
is-truncation-universal-property-truncation :
universal-property-truncation B f → is-truncation B f
is-truncation-universal-property-truncation H C =
is-equiv-is-contr-map
( λ g →
is-contr-equiv
( Σ (type-hom-Truncated-Type k B C) (λ h → (h ∘ f) ~ g))
( equiv-tot (λ h → equiv-funext))
( H C g))

abstract
universal-property-truncation-is-truncation :
is-truncation B f → universal-property-truncation B f
universal-property-truncation-is-truncation H C g =
is-contr-equiv'
( Σ (type-hom-Truncated-Type k B C) (λ h → (h ∘ f) ＝ g))
( equiv-tot (λ h → equiv-funext))
( is-contr-map-is-equiv (H C) g)

map-is-truncation :
is-truncation B f →
{l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) →
type-hom-Truncated-Type k B C
map-is-truncation H C g =
pr1 (center (universal-property-truncation-is-truncation H C g))

triangle-is-truncation :
(H : is-truncation B f) →
{l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) →
map-is-truncation H C g ∘ f ~ g
triangle-is-truncation H C g =
pr2 (center (universal-property-truncation-is-truncation H C g))


### A map into a truncated type is a truncation if and only if it satisfies the dependent universal property of the truncation

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

abstract
dependent-universal-property-truncation-is-truncation :
is-truncation B f →
dependent-universal-property-truncation B f
dependent-universal-property-truncation-is-truncation H X =
is-fiberwise-equiv-is-equiv-map-Σ
( λ (h : A → type-Truncated-Type B) →
(a : A) → type-Truncated-Type (X (h a)))
( λ (g : type-Truncated-Type B → type-Truncated-Type B) → g ∘ f)
( λ g (s : (b : type-Truncated-Type B) →
type-Truncated-Type (X (g b))) (a : A) → s (f a))
( H B)
( is-equiv-equiv
( inv-distributive-Π-Σ)
( inv-distributive-Π-Σ)
( ind-Σ (λ g s → refl))
( H (Σ-Truncated-Type B X)))
( id)

abstract
is-truncation-dependent-universal-property-truncation :
dependent-universal-property-truncation B f → is-truncation B f
is-truncation-dependent-universal-property-truncation H X = H (λ _ → X)

section-is-truncation :
is-truncation B f →
{l3 : Level} (C : Truncated-Type l3 k)
(h : A → type-Truncated-Type C) (g : type-hom-Truncated-Type k C B) →
f ~ g ∘ h → section g
section-is-truncation H C h g K =
map-distributive-Π-Σ
( map-inv-is-equiv
( dependent-universal-property-truncation-is-truncation H
( fiber-Truncated-Type C B g))
( λ a → (h a , inv (K a))))