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 2025-04-25.

module foundation.decidable-propositions where

open import foundation-core.decidable-propositions public
Imports
open import foundation.action-on-identifications-functions
open import foundation.booleans
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.equivalences
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
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.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 (Prop l)  Q  pr1 Q)  Q  ¬ (pr1 Q))) ∘e
  ( inv-associative-Σ (UU l) is-prop  X  is-decidable (pr1 X)))

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)

  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 (pair P (pair 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 (pair P (pair 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 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