The universal property of propositional truncations with respect to sets

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

Created on 2022-02-09.
Last modified on 2024-04-17.

module foundation.universal-property-propositional-truncation-into-sets where
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.propositional-truncations
open import foundation.universe-levels
open import foundation.weakly-constant-maps

open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.subtypes


The propositional truncation of A can be thought of as the quotient of A by the full equivalence relation, i.e., the equivalence relation by which all elements of A are considered to be equivalent. This idea leads to the universal property of the propositional truncations with respect to sets.


The precomposition map that is used to state the universal property

is-weakly-constant-precomp-unit-trunc-Prop :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (g : type-trunc-Prop A  B) 
  is-weakly-constant (g  unit-trunc-Prop)
is-weakly-constant-precomp-unit-trunc-Prop g x y =
    ( g)
    ( eq-is-prop (is-prop-type-trunc-Prop))

precomp-universal-property-set-quotient-trunc-Prop :
  {l1 l2 : Level} {A : UU l1} (B : Set l2) 
  (type-trunc-Prop A  type-Set B)  Σ (A  type-Set B) is-weakly-constant
pr1 (precomp-universal-property-set-quotient-trunc-Prop B g) =
  g  unit-trunc-Prop
pr2 (precomp-universal-property-set-quotient-trunc-Prop B g) =
  is-weakly-constant-precomp-unit-trunc-Prop g


The image of the propositional truncation into a set is a proposition

  all-elements-equal-image-is-weakly-constant :
    {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A  type-Set B) 
    is-weakly-constant f 
    all-elements-equal (Σ (type-Set B)  b  type-trunc-Prop (fiber f b)))
  all-elements-equal-image-is-weakly-constant B f H (x , s) (y , t) =
      ( λ b  trunc-Prop (fiber f b))
      ( apply-universal-property-trunc-Prop s
        ( Id-Prop B x y)
        ( λ u 
          apply-universal-property-trunc-Prop t
            ( Id-Prop B x y)
            ( λ v  inv (pr2 u)  H (pr1 u) (pr1 v)  pr2 v)))

  is-prop-image-is-weakly-constant :
    {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A  type-Set B) 
    is-weakly-constant f 
    is-prop (Σ (type-Set B)  b  type-trunc-Prop (fiber f b)))
  is-prop-image-is-weakly-constant B f H =
      ( all-elements-equal-image-is-weakly-constant B f H)

image-weakly-constant-map-Prop :
  {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A  type-Set B) 
  is-weakly-constant f  Prop (l1  l2)
pr1 (image-weakly-constant-map-Prop B f H) =
  Σ (type-Set B)  b  type-trunc-Prop (fiber f b))
pr2 (image-weakly-constant-map-Prop B f H) =
  is-prop-image-is-weakly-constant B f H

The universal property

map-universal-property-set-quotient-trunc-Prop :
  {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A  type-Set B) 
  is-weakly-constant f  type-trunc-Prop A  type-Set B
map-universal-property-set-quotient-trunc-Prop B f H =
  ( pr1) 
  ( map-universal-property-trunc-Prop
    ( image-weakly-constant-map-Prop B f H)
    ( λ a  (f a , unit-trunc-Prop (a , refl))))

map-universal-property-set-quotient-trunc-Prop' :
  {l1 l2 : Level} {A : UU l1} (B : Set l2) 
  Σ (A  type-Set B) is-weakly-constant  type-trunc-Prop A  type-Set B
map-universal-property-set-quotient-trunc-Prop' B (f , H) =
  map-universal-property-set-quotient-trunc-Prop B f H

  htpy-universal-property-set-quotient-trunc-Prop :
    {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A  type-Set B) 
    (H : is-weakly-constant f) 
    map-universal-property-set-quotient-trunc-Prop B f H  unit-trunc-Prop ~ f
  htpy-universal-property-set-quotient-trunc-Prop B f H a =
      ( pr1)
      ( eq-is-prop'
        ( is-prop-image-is-weakly-constant B f H)
        ( map-universal-property-trunc-Prop
          ( image-weakly-constant-map-Prop B f H)
          ( λ x  (f x , unit-trunc-Prop (x , refl)))
          ( unit-trunc-Prop a))
        ( f a , unit-trunc-Prop (a , refl)))

  is-section-map-universal-property-set-quotient-trunc-Prop :
    {l1 l2 : Level} {A : UU l1} (B : Set l2) 
    ( ( precomp-universal-property-set-quotient-trunc-Prop {A = A} B) 
      ( map-universal-property-set-quotient-trunc-Prop' B)) ~ id
  is-section-map-universal-property-set-quotient-trunc-Prop B (f , H) =
      ( is-weakly-constant-prop-Set B)
      ( eq-htpy (htpy-universal-property-set-quotient-trunc-Prop B f H))

  is-retraction-map-universal-property-set-quotient-trunc-Prop :
    {l1 l2 : Level} {A : UU l1} (B : Set l2) 
    ( ( map-universal-property-set-quotient-trunc-Prop' B) 
      ( precomp-universal-property-set-quotient-trunc-Prop {A = A} B)) ~ id
  is-retraction-map-universal-property-set-quotient-trunc-Prop B g =
      ( ind-trunc-Prop
        ( λ x 
          Id-Prop B
            ( map-universal-property-set-quotient-trunc-Prop' B
              ( precomp-universal-property-set-quotient-trunc-Prop B g)
              ( x))
            ( g x))
        ( htpy-universal-property-set-quotient-trunc-Prop B
          ( g  unit-trunc-Prop)
          ( is-weakly-constant-precomp-unit-trunc-Prop g)))

  universal-property-set-quotient-trunc-Prop :
    {l1 l2 : Level} {A : UU l1} (B : Set l2) 
    is-equiv (precomp-universal-property-set-quotient-trunc-Prop {A = A} B)
  universal-property-set-quotient-trunc-Prop B =
      ( map-universal-property-set-quotient-trunc-Prop' B)
      ( is-section-map-universal-property-set-quotient-trunc-Prop B)
      ( is-retraction-map-universal-property-set-quotient-trunc-Prop B)

Recent changes