Decidable propositions

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Louis Wasserman, Eléonore Mangel and Szumi Xie.

Created on 2022-02-10.
Last modified on 2026-05-02.

module foundation.decidable-propositions where

open import foundation-core.decidable-propositions public
Imports 
open import foundation.0-connected-types
open import foundation.action-on-identifications-functions
open import foundation.booleans
open import foundation.decidable-equality
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.dependent-products-propositions
open import foundation.discrete-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.equivalences
open import foundation.equivalences-contractible-types
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositional-extensionality
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.raising-universe-levels-unit-type
open import foundation.type-arithmetic-coproduct-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.coproduct-types
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.raising-universe-levels
open import foundation-core.retracts-of-types
open import foundation-core.sets
open import foundation-core.small-types
open import foundation-core.subtypes
open import foundation-core.transport-along-identifications

open import univalent-combinatorics.counting
open import univalent-combinatorics.finite-types

Idea

A decidable proposition is a proposition that has a decidable underlying type.

Properties

The forgetful map from decidable propositions to propositions is an embedding

is-emb-prop-Decidable-Prop : {l : Level} → is-emb (prop-Decidable-Prop {l})
is-emb-prop-Decidable-Prop =
  is-emb-tot
    ( λ X →
      is-emb-inclusion-subtype
        ( λ H → pair (is-decidable X) (is-prop-is-decidable H)))

emb-prop-Decidable-Prop : {l : Level} → Decidable-Prop l ↪ Prop l
pr1 emb-prop-Decidable-Prop = prop-Decidable-Prop
pr2 emb-prop-Decidable-Prop = is-emb-prop-Decidable-Prop

The type of decidable propositions is equivalent to the coproduct of the type of true propositions and the type of false propositions

split-Decidable-Prop :
  {l : Level} →
  Decidable-Prop l ≃
  ((Σ (Prop l) type-Prop) + (Σ (Prop l) (λ Q → ¬ (type-Prop Q))))
split-Decidable-Prop {l} =
  left-distributive-Σ-coproduct ∘e inv-associative-Σ

The type of decidable propositions in universe level l is equivalent to the type of booleans

module _
  {l : Level}
  where

  map-equiv-bool-Decidable-Prop : Decidable-Prop l → bool
  map-equiv-bool-Decidable-Prop P =
    rec-coproduct (λ _ → true) (λ _ → false) (is-decidable-Decidable-Prop P)

  map-inv-equiv-bool-Decidable-Prop : bool → Decidable-Prop l
  map-inv-equiv-bool-Decidable-Prop true =
    ( raise-unit l , is-prop-raise-unit , inl raise-star)
  map-inv-equiv-bool-Decidable-Prop false =
    ( raise-empty l , is-prop-raise-empty , inr map-inv-raise)

  is-section-map-inv-equiv-bool-Decidable-Prop :
    (map-equiv-bool-Decidable-Prop ∘ map-inv-equiv-bool-Decidable-Prop) ~ id
  is-section-map-inv-equiv-bool-Decidable-Prop false = refl
  is-section-map-inv-equiv-bool-Decidable-Prop true = refl

  is-retraction-map-inv-equiv-bool-Decidable-Prop :
    (map-inv-equiv-bool-Decidable-Prop ∘ map-equiv-bool-Decidable-Prop) ~ id
  is-retraction-map-inv-equiv-bool-Decidable-Prop prop@(_ , _ , inl _) =
    ap
      ( λ ((t' , is-prop-t') , type-t') → (t' , is-prop-t' , inl type-t'))
      ( eq-is-contr is-torsorial-true-Prop)
  is-retraction-map-inv-equiv-bool-Decidable-Prop prop@(_ , _ , inr _) =
    ap
      ( λ ((t' , is-prop-t') , type-t') → (t' , is-prop-t' , inr type-t'))
      ( eq-is-contr is-torsorial-false-Prop)

  is-equiv-map-equiv-bool-Decidable-Prop :
    is-equiv map-equiv-bool-Decidable-Prop
  is-equiv-map-equiv-bool-Decidable-Prop =
    is-equiv-is-invertible
      ( map-inv-equiv-bool-Decidable-Prop)
      ( is-section-map-inv-equiv-bool-Decidable-Prop)
      ( is-retraction-map-inv-equiv-bool-Decidable-Prop)

  equiv-bool-Decidable-Prop : Decidable-Prop l ≃ bool
  equiv-bool-Decidable-Prop =
    ( map-equiv-bool-Decidable-Prop ,
      is-equiv-map-equiv-bool-Decidable-Prop)

  bool-Decidable-Prop : Decidable-Prop l → bool
  bool-Decidable-Prop = map-equiv equiv-bool-Decidable-Prop

  abstract
    compute-equiv-bool-Decidable-Prop :
      (P : Decidable-Prop l) →
      type-Decidable-Prop P ≃ (map-equiv equiv-bool-Decidable-Prop P ＝ true)
    compute-equiv-bool-Decidable-Prop (P , H , inl p) =
      equiv-is-contr
        ( is-proof-irrelevant-is-prop H p)
        ( is-proof-irrelevant-is-prop (is-set-bool true true) refl)
    compute-equiv-bool-Decidable-Prop (P , H , inr np) =
      equiv-is-empty np neq-false-true-bool

Types of decidable propositions of any universe level are equivalent

equiv-universes-Decidable-Prop :
  (l l' : Level) → Decidable-Prop l ≃ Decidable-Prop l'
equiv-universes-Decidable-Prop l l' =
  inv-equiv equiv-bool-Decidable-Prop ∘e equiv-bool-Decidable-Prop

iff-universes-Decidable-Prop :
  (l l' : Level) (P : Decidable-Prop l) →
  ( type-Decidable-Prop P) ↔
  ( type-Decidable-Prop (map-equiv (equiv-universes-Decidable-Prop l l') P))
pr1 (iff-universes-Decidable-Prop l l' P) p =
  map-inv-equiv
    ( compute-equiv-bool-Decidable-Prop
      ( map-equiv (equiv-universes-Decidable-Prop l l') P))
    ( tr
      ( λ e → map-equiv e (map-equiv equiv-bool-Decidable-Prop P) ＝ true)
      ( inv (right-inverse-law-equiv equiv-bool-Decidable-Prop))
      ( map-equiv (compute-equiv-bool-Decidable-Prop P) p))
pr2 (iff-universes-Decidable-Prop l l' P) p =
  map-inv-equiv
    ( compute-equiv-bool-Decidable-Prop P)
    ( tr
      ( λ e → map-equiv e (map-equiv equiv-bool-Decidable-Prop P) ＝ true)
      ( right-inverse-law-equiv equiv-bool-Decidable-Prop)
      ( map-equiv
        ( compute-equiv-bool-Decidable-Prop
          ( map-equiv (equiv-universes-Decidable-Prop l l') P))
        ( p)))

The type of decidable propositions in any universe is discrete

has-decidable-equality-Decidable-Prop :
  {l : Level} → has-decidable-equality (Decidable-Prop l)
has-decidable-equality-Decidable-Prop =
  has-decidable-equality-equiv
    ( equiv-bool-Decidable-Prop)
    ( has-decidable-equality-bool)

Decidable-Prop-Discrete-Type : (l : Level) → Discrete-Type (lsuc l)
Decidable-Prop-Discrete-Type l =
  ( Decidable-Prop l , has-decidable-equality-Decidable-Prop)

The type of decidable propositions in any universe is a set

is-set-Decidable-Prop : {l : Level} → is-set (Decidable-Prop l)
is-set-Decidable-Prop {l} =
  is-set-equiv bool equiv-bool-Decidable-Prop is-set-bool

Decidable-Prop-Set : (l : Level) → Set (lsuc l)
pr1 (Decidable-Prop-Set l) = Decidable-Prop l
pr2 (Decidable-Prop-Set l) = is-set-Decidable-Prop

Extensionality of decidable propositions

module _
  {l : Level} (P Q : Decidable-Prop l)
  where

  extensionality-Decidable-Prop :
    (P ＝ Q) ≃ (type-Decidable-Prop P ↔ type-Decidable-Prop Q)
  extensionality-Decidable-Prop =
    ( propositional-extensionality
      ( prop-Decidable-Prop P)
      ( prop-Decidable-Prop Q)) ∘e
    ( equiv-ap-emb emb-prop-Decidable-Prop)

  iff-eq-Decidable-Prop :
    P ＝ Q → type-Decidable-Prop P ↔ type-Decidable-Prop Q
  iff-eq-Decidable-Prop = map-equiv extensionality-Decidable-Prop

  eq-iff-Decidable-Prop :
    (type-Decidable-Prop P → type-Decidable-Prop Q) →
    (type-Decidable-Prop Q → type-Decidable-Prop P) → P ＝ Q
  eq-iff-Decidable-Prop f g =
    map-inv-equiv extensionality-Decidable-Prop (pair f g)

The type of decidable propositions in any universe is small

abstract
  is-small-Decidable-Prop :
    (l1 l2 : Level) → is-small l2 (Decidable-Prop l1)
  pr1 (is-small-Decidable-Prop l1 l2) = raise l2 bool
  pr2 (is-small-Decidable-Prop l1 l2) =
    compute-raise l2 bool ∘e equiv-bool-Decidable-Prop

Decidable propositions have a count

count-is-decidable-Prop :
    {l : Level} (P : Prop l) →
    is-decidable (type-Prop P) → count (type-Prop P)
count-is-decidable-Prop P (inl x) =
  count-is-contr (is-proof-irrelevant-is-prop (is-prop-type-Prop P) x)
count-is-decidable-Prop P (inr x) =
  count-is-empty x

Decidable propositions are finite

abstract
  is-finite-is-decidable-Prop :
    {l : Level} (P : Prop l) →
    is-decidable (type-Prop P) → is-finite (type-Prop P)
  is-finite-is-decidable-Prop P x =
    is-finite-count (count-is-decidable-Prop P x)

is-finite-type-Decidable-Prop :
  {l : Level} (P : Decidable-Prop l) → is-finite (type-Decidable-Prop P)
is-finite-type-Decidable-Prop P =
  is-finite-is-decidable-Prop
    ( prop-Decidable-Prop P)
    ( is-decidable-Decidable-Prop P)

The type of decidable propositions of any universe level is finite

count-Decidable-Prop :
  {l : Level} → count (Decidable-Prop l)
pr1 count-Decidable-Prop = 2
pr2 count-Decidable-Prop =
  inv-equiv equiv-bool-Decidable-Prop ∘e equiv-bool-Fin-2

is-finite-Decidable-Prop : {l : Level} → is-finite (Decidable-Prop l)
is-finite-Decidable-Prop {l} = unit-trunc-Prop count-Decidable-Prop

number-of-elements-Decidable-Prop :
  {l : Level} → number-of-elements-is-finite (is-finite-Decidable-Prop {l}) ＝ 2
number-of-elements-Decidable-Prop =
  inv
    ( compute-number-of-elements-is-finite
      ( count-Decidable-Prop)
      ( is-finite-Decidable-Prop))

Decidable-Prop-Finite-Type : (l : Level) → Finite-Type (lsuc l)
Decidable-Prop-Finite-Type l = (Decidable-Prop l , is-finite-Decidable-Prop)

Decidable propositions are closed under retracts

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  is-decidable-prop-retract-of :
    A retract-of B → is-decidable-prop B → is-decidable-prop A
  is-decidable-prop-retract-of R (p , d) =
    ( is-prop-retract-of R p , is-decidable-retract-of R d)

Decidable propositions are closed under equivalences

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  is-decidable-prop-equiv :
    A ≃ B → is-decidable-prop B → is-decidable-prop A
  is-decidable-prop-equiv e =
    is-decidable-prop-retract-of (retract-equiv e)

  is-decidable-prop-equiv' :
    B ≃ A → is-decidable-prop B → is-decidable-prop A
  is-decidable-prop-equiv' e =
    is-decidable-prop-retract-of (retract-inv-equiv e)

Negation has no fixed points on decidable propositions

abstract
  no-fixed-points-neg-Decidable-Prop :
    {l : Level} (P : Decidable-Prop l) →
    ¬ (type-Decidable-Prop P ↔ ¬ (type-Decidable-Prop P))
  no-fixed-points-neg-Decidable-Prop P =
    no-fixed-points-neg (type-Decidable-Prop P)

Raising the universe level of decidable propositions

raise-Decidable-Prop :
  {l0 : Level} → (l : Level) → Decidable-Prop l0 → Decidable-Prop (l0 ⊔ l)
raise-Decidable-Prop l (t , is-prop-t , is-dec-t) =
  ( raise l t ,
    is-prop-type-Prop (raise-Prop l (t , is-prop-t)) ,
    rec-coproduct (inl ∘ map-raise) (λ ¬t → inr (¬t ∘ map-inv-raise)) is-dec-t)

Recent changes