Decidable propositions

module foundation.decidable-propositions where
Imports
open import foundation-core.decidable-propositions public

open import foundation.booleans
open import foundation.decidable-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.equivalences
open import foundation.negation
open import foundation.propositional-extensionality
open import foundation.raising-universe-levels
open import foundation.type-arithmetic-coproduct-types
open import foundation.unit-type

open import foundation-core.contractible-types
open import foundation-core.coproduct-types
open import foundation-core.dependent-pair-types
open import foundation-core.functions
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.logical-equivalences
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.small-types
open import foundation-core.subtypes
open import foundation-core.type-arithmetic-dependent-pair-types
open import foundation-core.universe-levels

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 in universe level l is equivalent to the type of booleans

module _
  {l : Level}
  where

  split-Decidable-Prop :
    Decidable-Prop l 
    ((Σ (Prop l) type-Prop) + (Σ (Prop l)  Q  ¬ (type-Prop Q))))
  split-Decidable-Prop =
    ( left-distributive-Σ-coprod (Prop l)  Q  pr1 Q)  Q  ¬ (pr1 Q))) ∘e
    ( inv-associative-Σ (UU l) is-prop  X  is-decidable (pr1 X)))

  map-equiv-bool-Decidable-Prop' :
    (Σ (Prop l) type-Prop) + (Σ (Prop l)  Q  ¬ (type-Prop Q))) 
    bool
  map-equiv-bool-Decidable-Prop' (inl x) = true
  map-equiv-bool-Decidable-Prop' (inr x) = false

  map-inv-equiv-bool-Decidable-Prop' :
    bool 
    (Σ (Prop l) type-Prop) + (Σ (Prop l)  Q  ¬ (type-Prop Q)))
  map-inv-equiv-bool-Decidable-Prop' true =
    inl (pair (raise-unit-Prop l) raise-star)
  map-inv-equiv-bool-Decidable-Prop' false =
    inr (pair (raise-empty-Prop l) is-empty-raise-empty)

  issec-map-inv-equiv-bool-Decidable-Prop' :
    (map-equiv-bool-Decidable-Prop'  map-inv-equiv-bool-Decidable-Prop') ~ id
  issec-map-inv-equiv-bool-Decidable-Prop' true = refl
  issec-map-inv-equiv-bool-Decidable-Prop' false = refl

  isretr-map-inv-equiv-bool-Decidable-Prop' :
    (map-inv-equiv-bool-Decidable-Prop'  map-equiv-bool-Decidable-Prop') ~ id
  isretr-map-inv-equiv-bool-Decidable-Prop' (inl x) =
    ap inl (eq-is-contr is-contr-total-true-Prop)
  isretr-map-inv-equiv-bool-Decidable-Prop' (inr x) =
    ap inr (eq-is-contr is-contr-total-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-has-inverse
      map-inv-equiv-bool-Decidable-Prop'
      issec-map-inv-equiv-bool-Decidable-Prop'
      isretr-map-inv-equiv-bool-Decidable-Prop'

  equiv-bool-Decidable-Prop' :
    ((Σ (Prop l) type-Prop) + (Σ (Prop l)  Q  ¬ (type-Prop Q)))) 
    bool
  pr1 equiv-bool-Decidable-Prop' = map-equiv-bool-Decidable-Prop'
  pr2 equiv-bool-Decidable-Prop' = is-equiv-map-equiv-bool-Decidable-Prop'

  equiv-bool-Decidable-Prop : Decidable-Prop l  bool
  equiv-bool-Decidable-Prop = equiv-bool-Decidable-Prop' ∘e split-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) 
  ( prop-Decidable-Prop P 
    prop-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

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)

The type of decidable propositions of any universe level is finite

is-finite-Decidable-Prop : {l : Level}  is-finite (Decidable-Prop l)
is-finite-Decidable-Prop {l} =
  is-finite-equiv' equiv-bool-Decidable-Prop is-finite-bool

decidable-Prop-𝔽 : (l : Level)  𝔽 (lsuc l)
pr1 (decidable-Prop-𝔽 l) = Decidable-Prop l
pr2 (decidable-Prop-𝔽 l) = is-finite-Decidable-Prop

The negation of a decidable proposition is a decidable proposition

neg-Decidable-Prop :
  {l : Level}  Decidable-Prop l  Decidable-Prop l
pr1 (neg-Decidable-Prop P) = ¬ (type-Decidable-Prop P)
pr1 (pr2 (neg-Decidable-Prop P)) = is-prop-neg
pr2 (pr2 (neg-Decidable-Prop P)) =
  is-decidable-neg (is-decidable-Decidable-Prop P)