Martin Escardo 2011.

\begin{code}

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

module NotionsOfDecidability.Decidable where

open import MLTT.Spartan
open import MLTT.Two-Properties
open import UF.Equiv
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.Logic

¬¬-elim : {A : 𝓀 Μ‡ } β†’ is-decidable A β†’ ¬¬ A β†’ A
¬¬-elim (inl a) f = a
¬¬-elim (inr g) f = 𝟘-elim(f g)

map-decidable : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ }
              β†’ (A β†’ B)
              β†’ (B β†’ A)
              β†’ is-decidable A
              β†’ is-decidable B
map-decidable f g (inl x) = inl (f x)
map-decidable f g (inr h) = inr (Ξ» y β†’ h (g y))

map-decidable-↔ : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ }
                β†’ (A ↔ B)
                β†’ (is-decidable A ↔ is-decidable B)
map-decidable-↔ (f , g) = map-decidable f g ,
                          map-decidable g f

decidability-is-closed-under-≃ : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ }
                               β†’ (A ≃ B)
                               β†’ is-decidable A
                               β†’ is-decidable B
decidability-is-closed-under-≃ (f , e) = map-decidable f (inverse f e)

map-decidable' : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ }
               β†’ (A β†’ Β¬ B)
               β†’ (Β¬ A β†’ B)
               β†’ is-decidable A
               β†’ is-decidable B
map-decidable' f g (inl x) = inr (f x)
map-decidable' f g (inr h) = inl (g h)

empty-is-decidable : {X : 𝓀 Μ‡ } β†’ is-empty X β†’ is-decidable X
empty-is-decidable = inr

𝟘-is-decidable : is-decidable (𝟘 {𝓀})
𝟘-is-decidable = empty-is-decidable 𝟘-elim

pointed-is-decidable : {X : 𝓀 Μ‡ } β†’ X β†’ is-decidable X
pointed-is-decidable = inl

πŸ™-is-decidable : is-decidable (πŸ™ {𝓀})
πŸ™-is-decidable = pointed-is-decidable ⋆

equivs-are-decidable : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (𝕗 : X ≃ Y)
                     β†’ each-fiber-of ⌜ 𝕗 ⌝ is-decidable
equivs-are-decidable 𝕗 y = inl (⌜ 𝕗 ⌝⁻¹ y , inverses-are-sections' 𝕗 y)

id-is-decidable : {X : 𝓀 Μ‡ } β†’ each-fiber-of (id {𝓀} {X}) is-decidable
id-is-decidable x = inl (x , refl)

decidable-closed-under-Ξ£ : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ }
                         β†’ is-prop X
                         β†’ is-decidable X
                         β†’ ((x : X) β†’ is-decidable (Y x))
                         β†’ is-decidable (Ξ£ Y)
decidable-closed-under-Ξ£ {𝓀} {π“₯} {X} {Y} isp d e = g d
 where
  g : is-decidable X β†’ is-decidable (Ξ£ Y)
  g (inl x) = h (e x)
   where
    Ο† : Ξ£ Y β†’ Y x
    Ο† (x' , y) = transport Y (isp x' x) y

    h : is-decidable(Y x) β†’ is-decidable (Ξ£ Y)
    h (inl y) = inl (x , y)
    h (inr v) = inr (contrapositive Ο† v)

  g (inr u) = inr (contrapositive pr₁ u)

Γ—-preserves-decidability : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ }
                         β†’ is-decidable A
                         β†’ is-decidable B
                         β†’ is-decidable (A Γ— B)
Γ—-preserves-decidability (inl a) (inl b) = inl (a , b)
Γ—-preserves-decidability (inl a) (inr v) = inr (Ξ» c β†’ v (prβ‚‚ c))
Γ—-preserves-decidability (inr u) _       = inr (Ξ» c β†’ u (pr₁ c))


+-preserves-decidability : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ }
                         β†’ is-decidable A
                         β†’ is-decidable B
                         β†’ is-decidable (A + B)
+-preserves-decidability (inl a) _       = inl (inl a)
+-preserves-decidability (inr u) (inl b) = inl (inr b)
+-preserves-decidability (inr u) (inr v) = inr (cases u v)

\end{code}

The following was added by Ayberk Tosun on 2024-05-28.

\begin{code}

module _ (pt : propositional-truncations-exist) where

 open Disjunction pt
 open PropositionalTruncation pt using (∣_∣; βˆ₯βˆ₯-rec)

 ∨-preserves-decidability : (P : Ξ© 𝓀) (Q : Ξ© π“₯)
                          β†’ is-decidable (P holds)
                          β†’ is-decidable (Q holds)
                          β†’ is-decidable ((P ∨ Q) holds)
 ∨-preserves-decidability P Q Ο† ψ =
  cases case₁ caseβ‚‚ (+-preserves-decidability Ο† ψ)
   where
    case₁ : P holds + Q holds β†’ is-decidable ((P ∨ Q) holds)
    case₁ (inl p) = inl ∣ inl p ∣
    case₁ (inr q) = inl ∣ inr q ∣

    caseβ‚‚ : Β¬ (P holds + Q holds) β†’ is-decidable ((P ∨ Q) holds)
    caseβ‚‚ = inr ∘ βˆ₯βˆ₯-rec 𝟘-is-prop

\end{code}

End of addition.

\begin{code}

β†’-preserves-decidability : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ }
                         β†’ is-decidable A
                         β†’ is-decidable B
                         β†’ is-decidable (A β†’ B)
β†’-preserves-decidability d       (inl b) = inl (Ξ» _ β†’ b)
β†’-preserves-decidability (inl a) (inr v) = inr (Ξ» f β†’ v (f a))
β†’-preserves-decidability (inr u) (inr v) = inl (Ξ» a β†’ 𝟘-elim (u a))

β†’-preserves-decidability' : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ }
                          β†’ (Β¬ B β†’  is-decidable A)
                          β†’ is-decidable B
                          β†’ is-decidable (A β†’ B)
β†’-preserves-decidability' Ο† (inl b) = inl (Ξ» _ β†’ b)
β†’-preserves-decidability' {𝓀} {π“₯} {A} {B} Ο† (inr v) = Ξ³ (Ο† v)
 where
  Ξ³ : is-decidable A β†’ is-decidable (A β†’ B)
  Ξ³ (inl a) = inr (Ξ» f β†’ v (f a))
  Ξ³ (inr u) = inl (Ξ» a β†’ 𝟘-elim (u a))

β†’-preserves-decidability'' : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ }
                           β†’ is-decidable A
                           β†’ (A β†’ is-decidable B)
                           β†’ is-decidable (A β†’ B)
β†’-preserves-decidability'' {𝓀} {π“₯} {A} {B} (inl a) Ο† = Ξ³ (Ο† a)
 where
  Ξ³ : is-decidable B β†’ is-decidable (A β†’ B)
  Ξ³ (inl b) = inl (Ξ» _ β†’ b)
  Ξ³ (inr v) = inr (Ξ» f β†’ v (f a))

β†’-preserves-decidability'' (inr u) Ο† = inl (Ξ» a β†’ 𝟘-elim (u a))

Β¬-preserves-decidability : {A : 𝓀 Μ‡ }
                         β†’ is-decidable A
                         β†’ is-decidable(Β¬ A)
Β¬-preserves-decidability d = β†’-preserves-decidability d 𝟘-is-decidable

which-of : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ }
         β†’ A + B
         β†’ Ξ£ b κž‰ 𝟚 , (b ＝ β‚€ β†’ A)
                   Γ— (b ＝ ₁ β†’ B)
which-of (inl a) = β‚€ ,
                   (Ξ» (r : β‚€ ＝ β‚€) β†’ a) ,
                   (Ξ» (p : β‚€ ＝ ₁) β†’ 𝟘-elim (zero-is-not-one p))
which-of (inr b) = ₁ ,
                   (Ξ» (p : ₁ ＝ β‚€) β†’ 𝟘-elim (zero-is-not-one (p ⁻¹))) ,
                   (Ξ» (r : ₁ ＝ ₁) β†’ b)

\end{code}

The following is a special case we are interested in:

\begin{code}

boolean-value : {A : 𝓀 Μ‡ }
              β†’ is-decidable A
              β†’ Ξ£ b κž‰ 𝟚 , (b ＝ β‚€ β†’   A)
                        Γ— (b ＝ ₁ β†’ Β¬ A)
boolean-value = which-of

module _ {X : 𝓀 Μ‡ } {Aβ‚€ : X β†’ π“₯ Μ‡ } {A₁ : X β†’ 𝓦 Μ‡ }
         (h : (x : X) β†’ Aβ‚€ x + A₁ x)
       where

 indicator : Ξ£ p κž‰ (X β†’ 𝟚) , ((x : X) β†’ (p x ＝ β‚€ β†’ Aβ‚€ x)
                                      Γ— (p x ＝ ₁ β†’ A₁ x))
 indicator = (Ξ» x β†’ pr₁(lemma₁ x)) , (Ξ» x β†’ prβ‚‚(lemma₁ x))
  where
   lemmaβ‚€ : (x : X) β†’ (Aβ‚€ x + A₁ x) β†’ Ξ£ b κž‰ 𝟚 , (b ＝ β‚€ β†’ Aβ‚€ x)
                                              Γ— (b ＝ ₁ β†’ A₁ x)
   lemmaβ‚€ x = which-of

   lemma₁ : (x : X) β†’ Ξ£ b κž‰ 𝟚 , (b ＝ β‚€ β†’ Aβ‚€ x) Γ— (b ＝ ₁ β†’ A₁ x)
   lemma₁ x = lemmaβ‚€ x (h x)

 indicator-map : X β†’ 𝟚
 indicator-map = pr₁ indicator

 indicator-property : (x : X) β†’ (indicator-map x ＝ β‚€ β†’ Aβ‚€ x)
                              Γ— (indicator-map x ＝ ₁ β†’ A₁ x)
 indicator-property = prβ‚‚ indicator

 indicator-propertyβ‚€ : (x : X) β†’ indicator-map x ＝ β‚€ β†’ Aβ‚€ x
 indicator-propertyβ‚€ x = pr₁ (indicator-property x)

 indicator-property₁ : (x : X) β†’ indicator-map x ＝ ₁ β†’ A₁ x
 indicator-property₁ x = prβ‚‚ (indicator-property x)

module _ {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
         (Ξ΄ : (x : X) β†’ A x + Β¬ A x)
       where

 private
  f : (x : X) β†’ is-decidable (A x) β†’ 𝟚
  f x (inl a) = β‚€
  f x (inr Ξ½) = ₁

  fβ‚€ : (x : X) (d : is-decidable (A x)) β†’ f x d ＝ β‚€ β†’ A x
  fβ‚€ x (inl a) e = a
  fβ‚€ x (inr Ξ½) e = 𝟘-elim (one-is-not-zero e)

  f₁ : (x : X) (d : is-decidable (A x)) β†’ f x d ＝ ₁ β†’ Β¬ A x
  f₁ x (inl a) e = 𝟘-elim (zero-is-not-one e)
  f₁ x (inr Ξ½) e = Ξ½

  fβ‚€-back : (x : X) (d : is-decidable (A x)) β†’ A x β†’ f x d ＝ β‚€
  fβ‚€-back x (inl a) a' = refl
  fβ‚€-back x (inr Ξ½) a' = 𝟘-elim (Ξ½ a')

  f₁-back : (x : X) (d : is-decidable (A x)) β†’ Β¬ A x β†’ f x d ＝ ₁
  f₁-back x (inl a) Ξ½' = 𝟘-elim (Ξ½' a)
  f₁-back x (inr Ξ½) Ξ½' = refl

  Ο‡ : X β†’ 𝟚
  Ο‡ x = f x (Ξ΄ x)

 characteristic-map : X β†’ 𝟚
 characteristic-map = Ο‡

 characteristic-map-propertyβ‚€ : (x : X) β†’ Ο‡ x ＝ β‚€ β†’ A x
 characteristic-map-propertyβ‚€ x = fβ‚€ x (Ξ΄ x)

 characteristic-map-property₁ : (x : X) β†’ Ο‡ x ＝ ₁ β†’ Β¬ A x
 characteristic-map-property₁ x = f₁ x (Ξ΄ x)

 characteristic-map-propertyβ‚€-back : (x : X) β†’ A x β†’ Ο‡ x ＝ β‚€
 characteristic-map-propertyβ‚€-back x = fβ‚€-back x (Ξ΄ x)

 characteristic-map-property₁-back : (x : X) β†’ Β¬ A x β†’ Ο‡ x ＝ ₁
 characteristic-map-property₁-back x = f₁-back x (Ξ΄ 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}

Added by Martin Escardo 17th September 2024. The propositional
truncation of a decidable type can be constructed with no assumptions
and it has split support.

\begin{code}

βˆ₯_βˆ₯⟨_⟩ : (X : 𝓀 Μ‡) β†’ is-decidable X β†’ 𝓀₀ Μ‡
βˆ₯ X βˆ₯⟨ inl x ⟩ = πŸ™
βˆ₯ X βˆ₯⟨ inr Ξ½ ⟩ = 𝟘

βˆ₯βˆ₯⟨_⟩-is-prop : {X : 𝓀 Μ‡ } (Ξ΄ : is-decidable X) β†’ is-prop βˆ₯ X βˆ₯⟨ Ξ΄ ⟩
βˆ₯βˆ₯⟨ inl x ⟩-is-prop = πŸ™-is-prop
βˆ₯βˆ₯⟨ inr Ξ½ ⟩-is-prop = 𝟘-is-prop

βˆ₯βˆ₯⟨_⟩-is-decidable : {X : 𝓀 Μ‡ } (Ξ΄ : is-decidable X) β†’ is-decidable βˆ₯ X βˆ₯⟨ Ξ΄ ⟩
βˆ₯βˆ₯⟨ inl x ⟩-is-decidable = πŸ™-is-decidable
βˆ₯βˆ₯⟨ inr Ξ½ ⟩-is-decidable = 𝟘-is-decidable

∣_∣⟨_⟩ : {X : 𝓀 Μ‡ } β†’ X β†’ (Ξ΄ : is-decidable X) β†’ βˆ₯ X βˆ₯⟨ Ξ΄ ⟩
∣ x ∣⟨ inl _ ⟩ = ⋆
∣ x ∣⟨ inr ν ⟩ = ν x

\end{code}

Notice that the induction principle doesn't require the family A to be
prop-valued.

\begin{code}

βˆ₯βˆ₯⟨_⟩-induction : {X : 𝓀 Μ‡ } (Ξ΄ : is-decidable X)
                 (A : βˆ₯ X βˆ₯⟨ Ξ΄ ⟩ β†’ π“₯ Μ‡ )
               β†’ ((x : X) β†’ A ∣ x ∣⟨ Ξ΄ ⟩)
               β†’ (s : βˆ₯ X βˆ₯⟨ Ξ΄ ⟩) β†’ A s
βˆ₯βˆ₯⟨ inl x ⟩-induction A f ⋆ = f x
βˆ₯βˆ₯⟨ inr Ξ½ ⟩-induction A f s = 𝟘-elim s

\end{code}

But the induction equation does.

\begin{code}

βˆ₯βˆ₯⟨_⟩-induction-equation : {X : 𝓀 Μ‡ }
                          (Ξ΄ : is-decidable X)
                          (A : βˆ₯ X βˆ₯⟨ Ξ΄ ⟩ β†’ π“₯ Μ‡ )
                        β†’ ((s : βˆ₯ X βˆ₯⟨ Ξ΄ ⟩) β†’ is-prop (A s))
                        β†’ (f : (x : X) β†’ A ∣ x ∣⟨ Ξ΄ ⟩)
                          (x : X)
                        β†’ βˆ₯βˆ₯⟨ Ξ΄ ⟩-induction A f ∣ x ∣⟨ Ξ΄ ⟩ ＝ f x
βˆ₯βˆ₯⟨ inl x ⟩-induction-equation A A-is-prop f x' = A-is-prop ⋆ (f x) (f x')
βˆ₯βˆ₯⟨ inr Ξ½ ⟩-induction-equation A A-is-prop f x  = 𝟘-elim (Ξ½ x)

βˆ₯βˆ₯⟨_⟩-rec : {X : 𝓀 Μ‡ } (Ξ΄ : is-decidable X) {A : π“₯ Μ‡ }
          β†’ (X β†’ A) β†’ βˆ₯ X βˆ₯⟨ Ξ΄ ⟩ β†’ A
βˆ₯βˆ₯⟨ Ξ΄ ⟩-rec {A} = βˆ₯βˆ₯⟨ Ξ΄ ⟩-induction (Ξ» _ β†’ A)

∣∣⟨_⟩-exit : {X : 𝓀 Μ‡} (Ξ΄ : is-decidable X) β†’ βˆ₯ X βˆ₯⟨ Ξ΄ ⟩ β†’ X
∣∣⟨ Ξ΄ ⟩-exit = βˆ₯βˆ₯⟨ Ξ΄ ⟩-rec id

∣∣⟨_⟩-exit-is-section : {X : 𝓀 Μ‡} (Ξ΄ : is-decidable X) (s : βˆ₯ X βˆ₯⟨ Ξ΄ ⟩)
                     β†’ ∣ ∣∣⟨ Ξ΄ ⟩-exit s ∣⟨ Ξ΄ ⟩ ＝ s
∣∣⟨ inl x ⟩-exit-is-section ⋆ = refl
∣∣⟨ inr ν ⟩-exit-is-section s = 𝟘-elim s

infix 0 βˆ₯_βˆ₯⟨_⟩
infix 0 ∣_∣⟨_⟩

module propositional-truncation-of-decidable-type
        (pt : propositional-truncations-exist)
       where

 open propositional-truncations-exist pt public

 module _ {X : 𝓀 Μ‡ } (Ξ΄ : is-decidable X) where

  βˆ₯βˆ₯⟨_⟩-to-βˆ₯βˆ₯ : βˆ₯ X βˆ₯⟨ Ξ΄ ⟩ β†’ βˆ₯ X βˆ₯
  βˆ₯βˆ₯⟨_⟩-to-βˆ₯βˆ₯ = βˆ₯βˆ₯⟨ Ξ΄ ⟩-rec ∣_∣

  βˆ₯βˆ₯-to-βˆ₯βˆ₯⟨_⟩ : βˆ₯ X βˆ₯ β†’ βˆ₯ X βˆ₯⟨ Ξ΄ ⟩
  βˆ₯βˆ₯-to-βˆ₯βˆ₯⟨_⟩ = βˆ₯βˆ₯-rec (βˆ₯βˆ₯⟨ Ξ΄ ⟩-is-prop) ∣_∣⟨ Ξ΄ ⟩

  decidable-types-have-split-support : βˆ₯ X βˆ₯ β†’ X
  decidable-types-have-split-support s = ∣∣⟨ Ξ΄ ⟩-exit (βˆ₯βˆ₯-to-βˆ₯βˆ₯⟨_⟩ s)

\end{code}