# The universal property of propositional truncations

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

Created on 2022-02-08.
Last modified on 2024-04-11.

module foundation.universal-property-propositional-truncation where

Imports
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.functoriality-cartesian-product-types
open import foundation.logical-equivalences
open import foundation.precomposition-functions-into-subuniverses
open import foundation.subtype-identity-principle
open import foundation.unit-type
open import foundation.universal-property-dependent-pair-types
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.function-types
open import foundation-core.functoriality-dependent-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-dependent-functions
open import foundation-core.precomposition-functions
open import foundation-core.propositions
open import foundation-core.type-theoretic-principle-of-choice


## Idea

A map f : A → P into a proposition P is said to satisfy the universal property of the propositional truncation of A, or is said to be a propositional truncation of A, if any map g : A → Q into a proposition Q extends uniquely along f.

## Definition

### The condition of being a propositional truncation

module _
{l1 l2 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P)
where

precomp-Prop :
{l3 : Level} (Q : Prop l3) →
type-hom-Prop P Q → A → type-Prop Q
precomp-Prop Q g = g ∘ f

is-propositional-truncation : UUω
is-propositional-truncation =
{l : Level} (Q : Prop l) → is-equiv (precomp-Prop Q)


### The universal property of the propositional truncation

module _
{l1 l2 : Level} {A : UU l1}
(P : Prop l2) (f : A → type-Prop P)
where

universal-property-propositional-truncation : UUω
universal-property-propositional-truncation =
{l : Level} (Q : Prop l) (g : A → type-Prop Q) →
is-contr (Σ (type-hom-Prop P Q) (λ h → h ∘ f ~ g))


### Extension property of the propositional truncation

This is a simplified form of the universal properties, that works because we're mapping into propositions.

module _
{l1 l2 : Level} {A : UU l1}
(P : Prop l2) (f : A → type-Prop P)
where

extension-property-propositional-truncation : UUω
extension-property-propositional-truncation =
{l : Level} (Q : Prop l) → (A → type-Prop Q) → type-hom-Prop P Q


### The dependent universal property of the propositional truncation

module _
{l1 l2 : Level} {A : UU l1}
(P : Prop l2) (f : A → type-Prop P)
where

dependent-universal-property-propositional-truncation : UUω
dependent-universal-property-propositional-truncation =
{l : Level} → (Q : type-Prop P → Prop l) →
is-equiv (precomp-Π f (type-Prop ∘ Q))


## Properties

### Being a propositional trunction is equivalent to satisfying the universal property of the propositional truncation

abstract
universal-property-is-propositional-truncation :
{l1 l2 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) →
is-propositional-truncation P f →
universal-property-propositional-truncation P f
universal-property-is-propositional-truncation P f is-ptr-f Q g =
is-contr-equiv'
( Σ (type-hom-Prop P Q) (λ h → h ∘ f ＝ g))
( equiv-tot (λ _ → equiv-funext))
( is-contr-map-is-equiv (is-ptr-f Q) g)

abstract
map-is-propositional-truncation :
{l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) →
is-propositional-truncation P f →
(Q : Prop l3) (g : A → type-Prop Q) → type-hom-Prop P Q
map-is-propositional-truncation P f is-ptr-f Q g =
pr1
( center
( universal-property-is-propositional-truncation P f is-ptr-f Q g))

htpy-is-propositional-truncation :
{l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) →
(is-ptr-f : is-propositional-truncation P f) →
(Q : Prop l3) (g : A → type-Prop Q) →
map-is-propositional-truncation P f is-ptr-f Q g ∘ f ~ g
htpy-is-propositional-truncation P f is-ptr-f Q g =
pr2
( center
( universal-property-is-propositional-truncation P f is-ptr-f Q g))

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


### Being a propositional truncation is equivalent to satisfying the extension property of propositional truncations

abstract
is-propositional-truncation-extension-property :
{ l1 l2 : Level} {A : UU l1} (P : Prop l2)
( f : A → type-Prop P) →
extension-property-propositional-truncation P f →
is-propositional-truncation P f
is-propositional-truncation-extension-property P f up-P Q =
is-equiv-has-converse-is-prop
( is-prop-Π (λ x → is-prop-type-Prop Q))
( is-prop-Π (λ x → is-prop-type-Prop Q))
( up-P Q)


### Uniqueness of propositional truncations

abstract
is-equiv-is-ptruncation-is-ptruncation :
{l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (P' : Prop l3)
(f : A → type-Prop P) (f' : A → type-Prop P')
(h : type-hom-Prop P P') (H : (h ∘ f) ~ f') →
is-propositional-truncation P f →
is-propositional-truncation P' f' →
is-equiv h
is-equiv-is-ptruncation-is-ptruncation P P' f f' h H is-ptr-P is-ptr-P' =
is-equiv-has-converse-is-prop
( is-prop-type-Prop P)
( is-prop-type-Prop P')
( map-inv-is-equiv (is-ptr-P' P) f)

abstract
is-ptruncation-is-ptruncation-is-equiv :
{l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (P' : Prop l3)
(f : A → type-Prop P) (f' : A → type-Prop P') (h : type-hom-Prop P P') →
is-equiv h → is-propositional-truncation P f →
is-propositional-truncation P' f'
is-ptruncation-is-ptruncation-is-equiv P P' f f' h is-equiv-h is-ptr-f =
is-propositional-truncation-extension-property P' f'
( λ R g →
( map-is-propositional-truncation P f is-ptr-f R g) ∘
( map-inv-is-equiv is-equiv-h))

abstract
is-ptruncation-is-equiv-is-ptruncation :
{l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (P' : Prop l3)
(f : A → type-Prop P) (f' : A → type-Prop P') (h : type-hom-Prop P P') →
is-propositional-truncation P' f' → is-equiv h →
is-propositional-truncation P f
is-ptruncation-is-equiv-is-ptruncation P P' f f' h is-ptr-f' is-equiv-h =
is-propositional-truncation-extension-property P f
( λ R g → (map-is-propositional-truncation P' f' is-ptr-f' R g) ∘ h)

abstract
is-uniquely-unique-propositional-truncation :
{l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (P' : Prop l3)
(f : A → type-Prop P) (f' : A → type-Prop P') →
is-propositional-truncation P f →
is-propositional-truncation P' f' →
is-contr (Σ (type-equiv-Prop P P') (λ e → (map-equiv e ∘ f) ~ f'))
is-uniquely-unique-propositional-truncation P P' f f' is-ptr-f is-ptr-f' =
is-torsorial-Eq-subtype
( universal-property-is-propositional-truncation P f is-ptr-f P' f')
( is-property-is-equiv)
( map-is-propositional-truncation P f is-ptr-f P' f')
( htpy-is-propositional-truncation P f is-ptr-f P' f')
( is-equiv-is-ptruncation-is-ptruncation P P' f f'
( map-is-propositional-truncation P f is-ptr-f P' f')
( htpy-is-propositional-truncation P f is-ptr-f P' f')
( λ {l} → is-ptr-f)
( λ {l} → is-ptr-f'))


### A map f : A → P is a propositional truncation if and only if it satisfies the dependent universal property of the propositional truncation

abstract
dependent-universal-property-is-propositional-truncation :
{ l1 l2 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) →
is-propositional-truncation P f →
dependent-universal-property-propositional-truncation P f
dependent-universal-property-is-propositional-truncation
{l1} {l2} {A} P f is-ptr-f Q =
is-fiberwise-equiv-is-equiv-map-Σ
( λ (g : A → type-Prop P) → (x : A) → type-Prop (Q (g x)))
( precomp f (type-Prop P))
( λ h → precomp-Π f (λ p → type-Prop (Q (h p))))
( is-ptr-f P)
( is-equiv-top-is-equiv-bottom-square
( map-inv-distributive-Π-Σ
{ C = λ (x : type-Prop P) (p : type-Prop P) → type-Prop (Q p)})
( map-inv-distributive-Π-Σ
{ C = λ (x : A) (p : type-Prop P) → type-Prop (Q p)})
( map-Σ
( λ (g : A → type-Prop P) → (x : A) → type-Prop (Q (g x)))
( precomp f (type-Prop P))
( λ h → precomp-Π f (λ p → type-Prop (Q (h p)))))
( precomp f (Σ (type-Prop P) (λ p → type-Prop (Q p))))
( ind-Σ (λ h h' → refl))
( is-equiv-map-inv-distributive-Π-Σ)
( is-equiv-map-inv-distributive-Π-Σ)
( is-ptr-f (Σ-Prop P Q)))
( id {A = type-Prop P})

abstract
is-propositional-truncation-dependent-universal-property :
{ l1 l2 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) →
dependent-universal-property-propositional-truncation P f →
is-propositional-truncation P f
is-propositional-truncation-dependent-universal-property P f dup-f Q =
dup-f (λ p → Q)


### Any map f : A → P that has a section is a propositional truncation

abstract
is-propositional-truncation-has-section :
{l1 l2 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) →
(g : type-Prop P → A) → is-propositional-truncation P f
is-propositional-truncation-has-section {A = A} P f g Q =
is-equiv-has-converse-is-prop
( is-prop-function-type (is-prop-type-Prop Q))
( is-prop-function-type (is-prop-type-Prop Q))
( λ h → h ∘ g)


### If A is a pointed type, then the map A → unit is a propositional truncation

abstract
is-propositional-truncation-terminal-map :
{ l1 : Level} (A : UU l1) (a : A) →
is-propositional-truncation unit-Prop (terminal-map A)
is-propositional-truncation-terminal-map A a =
is-propositional-truncation-has-section
( unit-Prop)
( terminal-map A)
( ind-unit a)


### Any map between propositions is a propositional truncation if and only if it is an equivalence

abstract
is-propositional-truncation-is-equiv :
{l1 l2 : Level} (P : Prop l1) (Q : Prop l2)
{f : type-hom-Prop P Q} →
is-equiv f → is-propositional-truncation Q f
is-propositional-truncation-is-equiv P Q {f} is-equiv-f R =
is-equiv-precomp-is-equiv f is-equiv-f (type-Prop R)

abstract
is-propositional-truncation-map-equiv :
{ l1 l2 : Level} (P : Prop l1) (Q : Prop l2)
(e : type-equiv-Prop P Q) →
is-propositional-truncation Q (map-equiv e)
is-propositional-truncation-map-equiv P Q e R =
is-equiv-precomp-is-equiv (map-equiv e) (is-equiv-map-equiv e) (type-Prop R)

abstract
is-equiv-is-propositional-truncation :
{l1 l2 : Level} (P : Prop l1) (Q : Prop l2) {f : type-hom-Prop P Q} →
is-propositional-truncation Q f → is-equiv f
is-equiv-is-propositional-truncation P Q {f} H =
is-equiv-is-equiv-precomp-Prop P Q f H


### The identity map on a proposition is a propositional truncation

abstract
is-propositional-truncation-id :
{ l1 : Level} (P : Prop l1) →
is-propositional-truncation P id
is-propositional-truncation-id P Q = is-equiv-id


### A product of propositional truncations is a propositional truncation

abstract
is-propositional-truncation-product :
{l1 l2 l3 l4 : Level}
{A : UU l1} (P : Prop l2) (f : A → type-Prop P)
{A' : UU l3} (P' : Prop l4) (f' : A' → type-Prop P') →
is-propositional-truncation P f →
is-propositional-truncation P' f' →
is-propositional-truncation (product-Prop P P') (map-product f f')
is-propositional-truncation-product P f P' f' is-ptr-f is-ptr-f' Q =
is-equiv-top-is-equiv-bottom-square
( ev-pair)
( ev-pair)
( precomp (map-product f f') (type-Prop Q))
( λ h a a' → h (f a) (f' a'))
( refl-htpy)
( is-equiv-ev-pair)
( is-equiv-ev-pair)
( is-equiv-comp
( λ h a a' → h a (f' a'))
( λ h a p' → h (f a) p')
( is-ptr-f (pair (type-hom-Prop P' Q) (is-prop-hom-Prop P' Q)))
( is-equiv-map-Π-is-fiberwise-equiv
( λ a → is-ptr-f' Q)))