Propositional truncations

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

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

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.logical-equivalences
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.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-𝕋

║_║₋₁ : {l : Level} → UU l → UU l
║_║₋₁ = type-trunc-Prop

Notation. The box drawings double vertical symbol ║ in the propositional truncation notation ║_║₋₁ can be inserted with agda-input using the escape sequence \--= and selecting the second item in the list.

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-has-converse-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-has-converse-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 =
    is-equiv-has-converse-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 =
    is-equiv-has-converse-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-has-converse-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-has-converse-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

Table of files about propositional logic

The following table gives an overview of basic constructions in propositional logic and related considerations.

Concept	File
Propositions (foundation-core)	`foundation-core.propositions`
Propositions (foundation)	`foundation.propositions`
Subterminal types	`foundation.subterminal-types`
Subsingleton induction	`foundation.subsingleton-induction`
Empty types (foundation-core)	`foundation-core.empty-types`
Empty types (foundation)	`foundation.empty-types`
Unit type	`foundation.unit-type`
Logical equivalences	`foundation.logical-equivalences`
Propositional extensionality	`foundation.propositional-extensionality`
Mere logical equivalences	`foundation.mere-logical-equivalences`
Conjunction	`foundation.conjunction`
Disjunction	`foundation.disjunction`
Exclusive disjunction	`foundation.exclusive-disjunction`
Existential quantification	`foundation.existential-quantification`
Uniqueness quantification	`foundation.uniqueness-quantification`
Universal quantification	`foundation.universal-quantification`
Negation	`foundation.negation`
Double negation	`foundation.double-negation`
Propositional truncations	`foundation.propositional-truncations`
Universal property of propositional truncations	`foundation.universal-property-propositional-truncation`
The induction principle of propositional truncations	`foundation.induction-principle-propositional-truncation`
Functoriality of propositional truncations	`foundation.functoriality-propositional-truncations`
Propositional resizing	`foundation.propositional-resizing`
Impredicative encodings of the logical operations	`foundation.impredicative-encodings`

External links

bracket type at $n$ Lab

Recent changes

2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
2024-03-02. Fredrik Bakke. Factor out standard pullbacks (#1042).
2024-02-06. Fredrik Bakke. Rename (co)prod to (co)product (#1017).
2024-01-25. Fredrik Bakke. Basic properties of orthogonal maps (#979).
2023-12-10. Fredrik Bakke. Refactor universal properties for various limits (#963).