# The universal property of set truncations

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Elisabeth Stenholm, Daniel Gratzer, Julian KG, fernabnor and louismntnu.

Created on 2022-02-17.

module foundation.universal-property-set-truncation where

Imports
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.mere-equality
open import foundation.reflecting-maps-equivalence-relations
open import foundation.sets
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universal-property-equivalences
open import foundation.universal-property-set-quotients
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.propositions
open import foundation-core.type-theoretic-principle-of-choice


## Idea

A map f : A → B into a set B satisfies the universal property of the set truncation of A if any map A → C into a set C extends uniquely along f to a map B → C.

## Definition

### The condition for a map into a set to be a set truncation

is-set-truncation :
{l1 l2 : Level} {A : UU l1} (B : Set l2) → (A → type-Set B) → UUω
is-set-truncation B f =
{l : Level} (C : Set l) → is-equiv (precomp-Set f C)


### The universal property of set truncations

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


### The dependent universal property of set truncations

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

dependent-universal-property-set-truncation :
{l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) → UUω
dependent-universal-property-set-truncation B f =
{l : Level} (X : type-Set B → Set l) → is-equiv (precomp-Π-Set f X)


## Properties

### A map into a set is a set truncation if it satisfies the universal property

abstract
is-set-truncation-universal-property :
{l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) →
universal-property-set-truncation B f →
is-set-truncation B f
is-set-truncation-universal-property B f up-f C =
is-equiv-is-contr-map
( λ g → is-contr-equiv
( Σ (hom-Set B C) (λ h → h ∘ f ~ g))
( equiv-tot (λ h → equiv-funext))
( up-f C g))


### A map into a set satisfies the universal property if it is a set truncation

abstract
universal-property-is-set-truncation :
{l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) →
is-set-truncation B f → universal-property-set-truncation B f
universal-property-is-set-truncation B f is-settr-f C g =
is-contr-equiv'
( Σ (hom-Set B C) (λ h → (h ∘ f) ＝ g))
( equiv-tot (λ h → equiv-funext))
( is-contr-map-is-equiv (is-settr-f C) g)

map-is-set-truncation :
{l1 l2 l3 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) →
is-set-truncation B f → (C : Set l3) (g : A → type-Set C) → hom-Set B C
map-is-set-truncation B f is-settr-f C g =
pr1 (center (universal-property-is-set-truncation B f is-settr-f C g))

triangle-is-set-truncation :
{l1 l2 l3 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) →
(is-settr-f : is-set-truncation B f) →
(C : Set l3) (g : A → type-Set C) →
map-is-set-truncation B f is-settr-f C g ∘ f ~ g
triangle-is-set-truncation B f is-settr-f C g =
pr2 (center (universal-property-is-set-truncation B f is-settr-f C g))


### The identity function on any set is a set truncation

abstract
is-set-truncation-id :
{l1 l2 : Level} {A : UU l1} (H : is-set A) → is-set-truncation (A , H) id
is-set-truncation-id H B =
is-equiv-precomp-is-equiv id is-equiv-id (type-Set B)


### Any equivalence into a set is a set truncation

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


### Any set truncation satisfies the dependent universal property of the set truncation

abstract
dependent-universal-property-is-set-truncation :
{l1 l2 l3 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) →
is-set-truncation B f →
dependent-universal-property-set-truncation B f
dependent-universal-property-is-set-truncation {A = A} B f H X =
is-fiberwise-equiv-is-equiv-map-Σ
( λ (h : A → type-Set B) → (a : A) → type-Set (X (h a)))
( λ (g : type-Set B → type-Set B) → g ∘ f)
( λ g (s : (b : type-Set B) → type-Set (X (g b))) (a : A) → s (f a))
( H B)
( is-equiv-equiv
( inv-distributive-Π-Σ)
( inv-distributive-Π-Σ)
( ind-Σ (λ g s → refl))
( H (Σ-Set B X)))
( id)


### Any map satisfying the dependent universal property of set truncations is a set truncation

abstract
is-set-truncation-dependent-universal-property :
{l1 l2 l3 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) →
dependent-universal-property-set-truncation B f →
is-set-truncation B f
is-set-truncation-dependent-universal-property B f H X =
H (λ b → X)


### Any set quotient of the mere equality equivalence relation is a set truncation

abstract
is-set-truncation-is-set-quotient :
{l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) →
is-set-quotient
( mere-eq-equivalence-relation A)
( B)
( reflecting-map-mere-eq B f) →
is-set-truncation B f
is-set-truncation-is-set-quotient {A = A} B f H X =
is-equiv-comp
( pr1)
( precomp-Set-Quotient
( mere-eq-equivalence-relation A)
( B)
( reflecting-map-mere-eq B f)
( X))
( H X)
( is-equiv-pr1-is-contr
( λ h →
is-proof-irrelevant-is-prop
( is-prop-reflects-equivalence-relation
( mere-eq-equivalence-relation A) X h)
( reflects-mere-eq X h)))


### Any set truncation is a quotient of the mere equality equivalence relation

abstract
is-set-quotient-is-set-truncation :
{l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) →
is-set-truncation B f →
is-set-quotient
( mere-eq-equivalence-relation A)
( B)
( reflecting-map-mere-eq B f)
is-set-quotient-is-set-truncation {A = A} B f H X =
is-equiv-right-factor
( pr1)
( precomp-Set-Quotient
( mere-eq-equivalence-relation A)
( B)
( reflecting-map-mere-eq B f)
( X))
( is-equiv-pr1-is-contr
( λ h →
is-proof-irrelevant-is-prop
( is-prop-reflects-equivalence-relation
( mere-eq-equivalence-relation A) X h)
( reflects-mere-eq X h)))
( H X)