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
Imports 
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

Idea

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.

Definition

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 =
  ap
    ( 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

Properties

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

abstract
  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) =
    eq-type-subtype
      ( λ 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)))

abstract
  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 =
    is-prop-all-elements-equal
      ( 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

abstract
  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 =
    ap
      ( 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) =
    eq-type-subtype
      ( 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 =
    eq-htpy
      ( 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 =
    is-equiv-is-invertible
      ( 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