Tom de Jong, 1 November 2021.

We show that 𝟚 classifies decidable subsets.

We start by defining the type Ωᡈ 𝓀 of decidable propositions in a type
universe 𝓀 and we show that 𝟚 ≃ Ωᡈ 𝓀 (for any universe 𝓀).

\begin{code}

{-# OPTIONS --safe --without-K #-}

module NotionsOfDecidability.DecidableClassifier where

open import MLTT.Spartan

open import MLTT.Plus-Properties
open import MLTT.Two-Properties
open import UF.Subsingletons
open import UF.SubtypeClassifier

open import NotionsOfDecidability.Decidable
open import NotionsOfDecidability.Complemented

boolean-value' : {A : 𝓀 Μ‡ }
               β†’ is-decidable A
               β†’ Ξ£ b κž‰ 𝟚 , (b = β‚€ ↔ Β¬ A)
                         Γ— (b = ₁ ↔   A)
boolean-value' {𝓀} {A} (inl a ) = (₁ , Ο• , ψ)
 where
  Ο• : ₁ = β‚€ ↔ Β¬ A
  Ο• = (Ξ» p β†’ 𝟘-elim (one-is-not-zero p))
    , (Ξ» na β†’ 𝟘-elim (na a))
  ψ : ₁ = ₁ ↔ A
  ψ = (Ξ» _ β†’ a) , (Ξ» _ β†’ refl)
boolean-value' {𝓀} {A} (inr na) = β‚€ , Ο• , ψ
 where
  Ο• : β‚€ = β‚€ ↔ Β¬ A
  Ο• = (Ξ» _ β†’ na) , (Ξ» _ β†’ refl)
  ψ : β‚€ = ₁ ↔ A
  ψ = (Ξ» p β†’ 𝟘-elim (zero-is-not-one p))
    , (Ξ» a β†’ 𝟘-elim (na a))

private
 Ωᡈ : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
 Ωᡈ 𝓀 = Ξ£ P κž‰ Ξ© 𝓀 , is-decidable (P holds)

 ⟨_⟩ : Ωᡈ 𝓀 β†’ 𝓀 Μ‡
 ⟨ (P , i) , δ ⟩ = P

open import UF.Equiv
open import UF.Subsingletons-FunExt
open import UF.FunExt
open import UF.Lower-FunExt

module _
        {𝓀 : Universe}
        (fe : funext 𝓀 𝓀)
        (pe : propext 𝓀)
       where

 to-Ωᡈ-equality : (P Q : Ωᡈ 𝓀)
                β†’ (⟨ P ⟩ β†’ ⟨ Q ⟩)
                β†’ (⟨ Q ⟩ β†’ ⟨ P ⟩)
                β†’ P = Q
 to-Ωᡈ-equality ((P , i) , δ) ((Q , j) , Ρ) α β =
  to-subtype-= Οƒ (to-subtype-= Ο„ (pe i j Ξ± Ξ²))
  where
   Οƒ : (P : Ξ© 𝓀) β†’ is-prop (is-decidable (P holds))
   Οƒ P = decidability-of-prop-is-prop (lower-funext 𝓀 𝓀 fe) (holds-is-prop P)
   Ο„ : (X : 𝓀 Μ‡ )β†’ is-prop (is-prop X)
   Ο„ _ = being-prop-is-prop fe

 𝟚-is-the-type-of-decidable-propositions : 𝟚 ≃ Ωᡈ 𝓀
 𝟚-is-the-type-of-decidable-propositions = qinveq f (g , η , Ρ)
  where
   f : 𝟚 β†’ Ωᡈ 𝓀
   f β‚€ = ((𝟘 , 𝟘-is-prop) , inr 𝟘-elim)
   f ₁ = ((πŸ™ , πŸ™-is-prop) , inl ⋆)
   g : Ωᡈ 𝓀 β†’ 𝟚
   g (P , Ξ΄) = pr₁ (boolean-value' Ξ΄)
   η : g ∘ f ∼ id
   Ξ· β‚€ = refl
   Ξ· ₁ = refl
   Ρ : f ∘ g ∼ id
   Ξ΅ P = 𝟚-equality-cases Ξ΅β‚€ Ρ₁
    where
     lemma : (g P = β‚€ ↔ Β¬ ⟨ P ⟩)
           Γ— (g P = ₁ ↔   ⟨ P ⟩)
     lemma = prβ‚‚ (boolean-value' (prβ‚‚ P))
     Ξ΅β‚€ : g P = β‚€
        β†’ (f ∘ g) P = P
     Ξ΅β‚€ e = to-Ωᡈ-equality (f (g P)) P
             (Ξ» (q : ⟨ f (g P) ⟩) β†’ 𝟘-elim (transport (Ξ» b β†’ ⟨ f b ⟩) e q))
             (Ξ» (p : ⟨ P ⟩) β†’ 𝟘-elim (lr-implication (pr₁ lemma) e p))
     Ρ₁ : g P = ₁
        β†’ (f ∘ g) P = P
     Ρ₁ e = to-Ωᡈ-equality (f (g P)) P
             (Ξ» _ β†’ lr-implication (prβ‚‚ lemma) e)
             (Ξ» _ β†’ transport⁻¹ (Ξ» (b : 𝟚) β†’ ⟨ f b ⟩) e ⋆)

\end{code}

The promised result now follows promptly using two general lemmas on
equivalences.

(Note that one direction of the equivalence Ξ Ξ£-distr-≃ is sometimes known as
"type-theoretic axiom of choice".)

\begin{code}

open import UF.Powerset
open import UF.EquivalenceExamples

is-complemented-subset : {X : 𝓀 Μ‡ } β†’ (X β†’ Ξ© 𝓣) β†’ 𝓀 βŠ” 𝓣 Μ‡
is-complemented-subset {𝓀} {𝓣} {X} A = (x : X) β†’ is-decidable (x ∈ A)

module _
        (fe  : funext 𝓀 (𝓣 ⁺))
        (fe' : funext 𝓣 𝓣)
        (pe : propext 𝓣)
       where

 𝟚-classifies-decidable-subsets : {X : 𝓀 Μ‡ }
                                β†’ (X β†’ 𝟚)
                                ≃ (Ξ£ A κž‰ (X β†’ Ξ© 𝓣) , is-complemented-subset A)
 𝟚-classifies-decidable-subsets {X} =
  (X β†’ 𝟚)                                      β‰ƒβŸ¨ Ξ³          ⟩
  (X β†’ Ωᡈ 𝓣)                                   β‰ƒβŸ¨ Ξ Ξ£-distr-≃ ⟩
  (Ξ£ A κž‰ (X β†’ Ξ© 𝓣) , is-complemented-subset A) β– 
   where
    Ξ³ = β†’cong' fe (lower-funext 𝓀 (𝓣 ⁺) fe)
         (𝟚-is-the-type-of-decidable-propositions fe' pe)

 𝟚-classifies-decidable-subsets-values :
   {X : 𝓀 Μ‡ }
   (A : X β†’ Ξ© 𝓣)
   (Ξ΄ : is-complemented-subset A)
   (x : X)
   β†’ ((⌜ 𝟚-classifies-decidable-subsets ⌝⁻¹ (A , Ξ΄) x = β‚€) ↔ Β¬ (x ∈ A))
   Γ— ((⌜ 𝟚-classifies-decidable-subsets ⌝⁻¹ (A , Ξ΄) x = ₁) ↔   (x ∈ A))
 𝟚-classifies-decidable-subsets-values {X} A δ x = γ
  where
   Ο‡ : (Ξ£ A κž‰ (X β†’ Ξ© 𝓣) , is-complemented-subset A) β†’ (X β†’ 𝟚)
   Ο‡ = ⌜ 𝟚-classifies-decidable-subsets ⌝⁻¹
   Ξ³ : (Ο‡ (A , Ξ΄) x = β‚€ ↔ Β¬ (x ∈ A))
     Γ— (Ο‡ (A , Ξ΄) x = ₁ ↔   (x ∈ A))
   Ξ³ = prβ‚‚ (boolean-value' (Ξ΄ x))

\end{code}

Added by Tom de Jong, November 2021.

\begin{code}

decidable-↔ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
            β†’ X ↔ Y
            β†’ is-decidable X
            β†’ is-decidable Y
decidable-↔ {𝓀} {π“₯} {X} {Y} (f , g) (inl  x) = inl (f x)
decidable-↔ {𝓀} {π“₯} {X} {Y} (f , g) (inr nx) = inr (nx ∘ g)

decidable-cong : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
               β†’ X ≃ Y
               β†’ is-decidable X
               β†’ is-decidable Y
decidable-cong e = decidable-↔ (⌜ e ⌝ , ⌜ e ⌝⁻¹)

\end{code}

Added by Tom de Jong in January 2022.

\begin{code}

all-types-are-¬¬-decidable : (X : 𝓀 Μ‡ ) β†’ ¬¬ (is-decidable X)
all-types-are-¬¬-decidable X h = claimβ‚‚ claim₁
 where
  claim₁ : Β¬ X
  claim₁ x = h (inl x)
  claimβ‚‚ : ¬¬ X
  claimβ‚‚ nx = h (inr nx)

¬¬-stable-if-decidable : (X : 𝓀 Μ‡ ) β†’ is-decidable X β†’ ¬¬-stable X
¬¬-stable-if-decidable X (inl  x) = Ξ» _ β†’ x
¬¬-stable-if-decidable X (inr nx) = Ξ» h β†’ 𝟘-elim (h nx)

\end{code}