Propositional truncations

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

Created on 2022-02-08.
Last modified on 2024-03-02.

module foundation.propositional-truncations where
Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.functoriality-cartesian-product-types
open import foundation.propositions
open import foundation.truncations
open import foundation.universal-property-propositional-truncation
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.contractible-types
open import foundation-core.coproduct-types
open import foundation-core.equivalences
open import foundation-core.function-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.sections
open import foundation-core.sets
open import foundation-core.transport-along-identifications
open import foundation-core.truncated-types
open import foundation-core.truncation-levels

Idea

We have specified what it means to be a propositional truncation in the file foundation.universal-property-propositional-truncation. Here we use the postulate of the existence of truncations at all levels, found in the file foundation.truncations, to show that propositional truncations exist.

Definition

type-trunc-Prop : {l : Level}  UU l  UU l
type-trunc-Prop = type-trunc neg-one-𝕋

unit-trunc-Prop : {l : Level} {A : UU l}  A  type-trunc-Prop A
unit-trunc-Prop = unit-trunc

is-prop-type-trunc-Prop : {l : Level} {A : UU l}  is-prop (type-trunc-Prop A)
is-prop-type-trunc-Prop = is-trunc-type-trunc

all-elements-equal-type-trunc-Prop :
  {l : Level} {A : UU l}  all-elements-equal (type-trunc-Prop A)
all-elements-equal-type-trunc-Prop {l} {A} =
  eq-is-prop' (is-prop-type-trunc-Prop {l} {A})

trunc-Prop : {l : Level}  UU l  Prop l
trunc-Prop = trunc neg-one-𝕋

Properties

The condition in the induction principle is a property

abstract
  is-prop-condition-ind-trunc-Prop' :
    {l1 l2 : Level} {A : UU l1} {P : type-trunc-Prop A  UU l2} 
    ( (x y : type-trunc-Prop A) (u : P x) (v : P y) 
      tr P (all-elements-equal-type-trunc-Prop x y) u  v) 
    (x : type-trunc-Prop A)  is-prop (P x)
  is-prop-condition-ind-trunc-Prop' {P = P} H x =
    is-prop-all-elements-equal
      ( λ u v 
        ( ap
          ( λ γ  tr P γ u)
          ( eq-is-contr (is-prop-type-trunc-Prop x x))) 
        ( H x x u v))

The induction principle for propositional truncations

ind-trunc-Prop' :
  {l l1 : Level} {A : UU l1} (P : type-trunc-Prop A  UU l)
  (f : (x : A)  P (unit-trunc-Prop x))
  (H :
    (x y : type-trunc-Prop A) (u : P x) (v : P y) 
    tr P (all-elements-equal-type-trunc-Prop x y) u  v) 
  (x : type-trunc-Prop A)  P x
ind-trunc-Prop' P f H =
  function-dependent-universal-property-trunc
    ( λ x  pair (P x) (is-prop-condition-ind-trunc-Prop' H x))
    ( f)

The propositional induction principle for propositional truncations

module _
  {l l1 : Level} {A : UU l1} (P : type-trunc-Prop A  Prop l)
  where

  abstract
    ind-trunc-Prop :
      ((x : A)  type-Prop (P (unit-trunc-Prop x))) 
      (( y : type-trunc-Prop A)  type-Prop (P y))
    ind-trunc-Prop f =
      ind-trunc-Prop' (type-Prop  P) f
        ( λ x y u v  eq-is-prop (is-prop-type-Prop (P y)))

    compute-ind-trunc-Prop :
        is-section (precomp-Π unit-trunc-Prop (type-Prop  P)) (ind-trunc-Prop)
    compute-ind-trunc-Prop h =
      eq-is-prop (is-prop-Π  x  is-prop-type-Prop (P (unit-trunc-Prop x))))

The propositional recursion principle for propositional truncations

module _
  {l l1 : Level} {A : UU l1} (P : Prop l)
  where

  abstract
    rec-trunc-Prop :
      (A  type-Prop P)  (type-trunc-Prop A  type-Prop P)
    rec-trunc-Prop = ind-trunc-Prop  _  P)

    compute-rec-trunc-Prop :
      is-section (precomp unit-trunc-Prop (type-Prop P)) (rec-trunc-Prop)
    compute-rec-trunc-Prop = compute-ind-trunc-Prop  _  P)

The defined propositional truncations are propositional truncations

abstract
  is-propositional-truncation-trunc-Prop :
    {l : Level} (A : UU l) 
    is-propositional-truncation (trunc-Prop A) unit-trunc-Prop
  is-propositional-truncation-trunc-Prop A =
    is-propositional-truncation-extension-property
      ( trunc-Prop A)
      ( unit-trunc-Prop)
      ( λ Q  ind-trunc-Prop  x  Q))

The defined propositional truncations satisfy the universal property of propositional truncations

abstract
  universal-property-trunc-Prop :
    {l : Level} (A : UU l) 
    universal-property-propositional-truncation
      ( trunc-Prop A)
      ( unit-trunc-Prop)
  universal-property-trunc-Prop A =
    universal-property-is-propositional-truncation
      ( trunc-Prop A)
      ( unit-trunc-Prop)
      ( is-propositional-truncation-trunc-Prop A)

abstract
  map-universal-property-trunc-Prop :
    {l1 l2 : Level} {A : UU l1} (P : Prop l2) 
    (A  type-Prop P)  type-hom-Prop (trunc-Prop A) P
  map-universal-property-trunc-Prop {A = A} P f =
    map-is-propositional-truncation
      ( trunc-Prop A)
      ( unit-trunc-Prop)
      ( is-propositional-truncation-trunc-Prop A)
      ( P)
      ( f)

abstract
  apply-universal-property-trunc-Prop :
    {l1 l2 : Level} {A : UU l1} (t : type-trunc-Prop A) (P : Prop l2) 
    (A  type-Prop P)  type-Prop P
  apply-universal-property-trunc-Prop t P f =
    map-universal-property-trunc-Prop P f t

abstract
  apply-twice-universal-property-trunc-Prop :
    {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (u : type-trunc-Prop A)
    (v : type-trunc-Prop B) (P : Prop l3) 
    (A  B  type-Prop P)  type-Prop P
  apply-twice-universal-property-trunc-Prop u v P f =
    apply-universal-property-trunc-Prop u P
      ( λ x  apply-universal-property-trunc-Prop v P (f x))

abstract
  apply-three-times-universal-property-trunc-Prop :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
    (u : type-trunc-Prop A) (v : type-trunc-Prop B) (w : type-trunc-Prop C) 
    (P : Prop l4)  (A  B  C  type-Prop P)  type-Prop P
  apply-three-times-universal-property-trunc-Prop u v w P f =
    apply-universal-property-trunc-Prop u P
      ( λ x  apply-twice-universal-property-trunc-Prop v w P (f x))

The propositional truncation of a type is k+1-truncated

is-trunc-trunc-Prop :
  {l : Level} (k : 𝕋) {A : UU l}  is-trunc (succ-𝕋 k) (type-trunc-Prop A)
is-trunc-trunc-Prop k = is-trunc-is-prop k is-prop-type-trunc-Prop

truncated-type-trunc-Prop :
  {l : Level} (k : 𝕋)  UU l  Truncated-Type l (succ-𝕋 k)
pr1 (truncated-type-trunc-Prop k A) = type-trunc-Prop A
pr2 (truncated-type-trunc-Prop k A) = is-trunc-trunc-Prop k

set-trunc-Prop : {l : Level}  UU l  Set l
set-trunc-Prop = truncated-type-trunc-Prop neg-one-𝕋

A proposition is equivalent to its propositional truncation

module _
  {l : Level} (A : Prop l)
  where

  equiv-unit-trunc-Prop : type-Prop A  type-trunc-Prop (type-Prop A)
  equiv-unit-trunc-Prop = equiv-unit-trunc A

The propositional truncation is idempotent

module _
  {l : Level} (A : UU l)
  where

  abstract
    map-idempotent-trunc-Prop :
      type-trunc-Prop (type-trunc-Prop A)  type-trunc-Prop A
    map-idempotent-trunc-Prop =
      map-universal-property-trunc-Prop (trunc-Prop A) id

  abstract
    is-equiv-map-idempotent-trunc-Prop : is-equiv map-idempotent-trunc-Prop
    is-equiv-map-idempotent-trunc-Prop =
      is-equiv-is-prop
        ( is-prop-type-trunc-Prop)
        ( is-prop-type-trunc-Prop)
        ( unit-trunc-Prop)

  idempotent-trunc-Prop :
    type-trunc-Prop (type-trunc-Prop A)  type-trunc-Prop A
  pr1 idempotent-trunc-Prop = map-idempotent-trunc-Prop
  pr2 idempotent-trunc-Prop = is-equiv-map-idempotent-trunc-Prop

  abstract
    is-equiv-map-inv-idempotent-trunc-Prop :
      is-equiv (unit-trunc-Prop {A = type-trunc-Prop A})
    is-equiv-map-inv-idempotent-trunc-Prop =
      is-equiv-is-prop
        ( is-prop-type-trunc-Prop)
        ( is-prop-type-trunc-Prop)
        ( map-idempotent-trunc-Prop)

  inv-idempotent-trunc-Prop :
    type-trunc-Prop A  type-trunc-Prop (type-trunc-Prop A)
  pr1 inv-idempotent-trunc-Prop = unit-trunc-Prop
  pr2 inv-idempotent-trunc-Prop = is-equiv-map-inv-idempotent-trunc-Prop

Propositional truncations satisfy the dependent universal property of the propositional truncation

abstract
  dependent-universal-property-trunc-Prop :
    {l : Level} {A : UU l} 
      dependent-universal-property-propositional-truncation
      ( trunc-Prop A)
      ( unit-trunc-Prop)
  dependent-universal-property-trunc-Prop {A = A} =
    dependent-universal-property-is-propositional-truncation
      ( trunc-Prop A)
      ( unit-trunc-Prop)
      ( is-propositional-truncation-trunc-Prop A)

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

  equiv-dependent-universal-property-trunc-Prop :
    ((y : type-trunc-Prop A)  type-Prop (P y)) 
    ((x : A)  type-Prop (P (unit-trunc-Prop x)))
  pr1 equiv-dependent-universal-property-trunc-Prop =
    precomp-Π unit-trunc-Prop (type-Prop  P)
  pr2 equiv-dependent-universal-property-trunc-Prop =
    dependent-universal-property-trunc-Prop P

  apply-dependent-universal-property-trunc-Prop :
    (y : type-trunc-Prop A)  ((x : A)  type-Prop (P (unit-trunc-Prop x))) 
    type-Prop (P y)
  apply-dependent-universal-property-trunc-Prop y f =
    map-inv-equiv equiv-dependent-universal-property-trunc-Prop f y

Propositional truncations distribute over cartesian products

equiv-product-trunc-Prop :
  {l1 l2 : Level} (A : UU l1) (A' : UU l2) 
  type-equiv-Prop
    ( trunc-Prop (A × A'))
    ( product-Prop (trunc-Prop A) (trunc-Prop A'))
equiv-product-trunc-Prop A A' =
  pr1
    ( center
      ( is-uniquely-unique-propositional-truncation
        ( trunc-Prop (A × A'))
        ( product-Prop (trunc-Prop A) (trunc-Prop A'))
        ( unit-trunc-Prop)
        ( map-product unit-trunc-Prop unit-trunc-Prop)
        ( is-propositional-truncation-trunc-Prop (A × A'))
        ( is-propositional-truncation-product
          ( trunc-Prop A)
          ( unit-trunc-Prop)
          ( trunc-Prop A')
          ( unit-trunc-Prop)
          ( is-propositional-truncation-trunc-Prop A)
          ( is-propositional-truncation-trunc-Prop A'))))

map-distributive-trunc-product-Prop :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  type-trunc-Prop (A × B)  type-trunc-Prop A × type-trunc-Prop B
map-distributive-trunc-product-Prop {l1} {l2} {A} {B} =
  map-universal-property-trunc-Prop
    ( pair
      ( type-trunc-Prop A × type-trunc-Prop B)
      ( is-prop-product is-prop-type-trunc-Prop is-prop-type-trunc-Prop))
    ( map-product unit-trunc-Prop unit-trunc-Prop)

map-inv-distributive-trunc-product-Prop :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  type-trunc-Prop A × type-trunc-Prop B  type-trunc-Prop (A × B)
map-inv-distributive-trunc-product-Prop {l1} {l2} {A} {B} t =
  map-universal-property-trunc-Prop
    ( trunc-Prop (A × B))
    ( λ x 
      map-universal-property-trunc-Prop
        ( trunc-Prop (A × B))
        ( unit-trunc-Prop  (pair x))
        ( pr2 t))
    ( pr1 t)

abstract
  is-equiv-map-distributive-trunc-product-Prop :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} 
    is-equiv (map-distributive-trunc-product-Prop {A = A} {B = B})
  is-equiv-map-distributive-trunc-product-Prop {l1} {l2} {A} {B} =
    is-equiv-is-prop
      ( is-prop-type-trunc-Prop)
      ( is-prop-product is-prop-type-trunc-Prop is-prop-type-trunc-Prop)
      ( map-inv-distributive-trunc-product-Prop)

distributive-trunc-product-Prop :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  type-trunc-Prop (A × B)  (type-trunc-Prop A × type-trunc-Prop B)
pr1 distributive-trunc-product-Prop = map-distributive-trunc-product-Prop
pr2 distributive-trunc-product-Prop =
  is-equiv-map-distributive-trunc-product-Prop

abstract
  is-equiv-map-inv-distributive-trunc-product-Prop :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} 
    is-equiv (map-inv-distributive-trunc-product-Prop {A = A} {B = B})
  is-equiv-map-inv-distributive-trunc-product-Prop {l1} {l2} {A} {B} =
    is-equiv-is-prop
      ( is-prop-product is-prop-type-trunc-Prop is-prop-type-trunc-Prop)
      ( is-prop-type-trunc-Prop)
      ( map-distributive-trunc-product-Prop)

inv-distributive-trunc-product-Prop :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  ( type-trunc-Prop A × type-trunc-Prop B)  type-trunc-Prop (A × B)
pr1 inv-distributive-trunc-product-Prop =
  map-inv-distributive-trunc-product-Prop
pr2 inv-distributive-trunc-product-Prop =
  is-equiv-map-inv-distributive-trunc-product-Prop

Propositional truncations of coproducts of types with themselves

module _
  {l : Level} {A : UU l} where
  map-trunc-Prop-diagonal-coproduct :
    type-trunc-Prop (A + A)  type-trunc-Prop A
  map-trunc-Prop-diagonal-coproduct =
    map-universal-property-trunc-Prop
      ( trunc-Prop A)
      ( unit-trunc  rec-coproduct id id)

  map-inv-trunc-Prop-diagonal-coproduct :
    type-trunc-Prop A  type-trunc-Prop (A + A)
  map-inv-trunc-Prop-diagonal-coproduct =
    map-universal-property-trunc-Prop
      ( trunc-Prop (A + A))
      ( unit-trunc  (inl  id))

  abstract
    is-equiv-map-trunc-Prop-diagonal-coproduct :
      is-equiv map-trunc-Prop-diagonal-coproduct
    is-equiv-map-trunc-Prop-diagonal-coproduct =
      is-equiv-is-prop
        is-prop-type-trunc-Prop
        is-prop-type-trunc-Prop
        map-inv-trunc-Prop-diagonal-coproduct

    is-equiv-map-inv-trunc-Prop-diagonal-coproduct :
      is-equiv map-inv-trunc-Prop-diagonal-coproduct
    is-equiv-map-inv-trunc-Prop-diagonal-coproduct =
      is-equiv-is-prop
        is-prop-type-trunc-Prop
        is-prop-type-trunc-Prop
        map-trunc-Prop-diagonal-coproduct

  equiv-trunc-Prop-diagonal-coproduct :
    (type-trunc-Prop (A + A))  type-trunc-Prop A
  pr1 equiv-trunc-Prop-diagonal-coproduct = map-trunc-Prop-diagonal-coproduct
  pr2 equiv-trunc-Prop-diagonal-coproduct =
    is-equiv-map-trunc-Prop-diagonal-coproduct

  inv-equiv-trunc-Prop-diagonal-coproduct :
    (type-trunc-Prop A)  type-trunc-Prop (A + A)
  pr1 inv-equiv-trunc-Prop-diagonal-coproduct =
    map-inv-trunc-Prop-diagonal-coproduct
  pr2 inv-equiv-trunc-Prop-diagonal-coproduct =
    is-equiv-map-inv-trunc-Prop-diagonal-coproduct

Recent changes