Martin Escardo 2011.

\begin{code}

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

module NotionsOfDecidability.Decidable where

open import MLTT.Spartan
open import MLTT.Two-Properties
open import UF.Equiv
open import UF.Subsingletons

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

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

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

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

map-is-decidable' : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ } β†’ (A β†’ Β¬ B) β†’ (Β¬ A β†’ B) β†’ is-decidable A β†’ is-decidable B
map-is-decidable' f g (inl x) = inr (f x)
map-is-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)

β†’-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

\end{code}

Notice that this b is unique (Agda exercise) and that the converse
also holds. In classical mathematics it is posited that all
propositions have binary truth values, irrespective of whether they
have BHK-style witnesses. And this is precisely the role of the
principle of excluded middle in classical mathematics.  The following
requires choice, which holds in BHK-style constructive mathematics:
s
\begin{code}

indicator : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ }
          β†’ ((x : X) β†’ A x + B x)
          β†’ Ξ£ p κž‰ (X β†’ 𝟚) , ((x : X) β†’ (p x ＝ β‚€ β†’ A x)
                                     Γ— (p x ＝ ₁ β†’ B x))
indicator {𝓀} {π“₯} {𝓦} {X} {A} {B} h = (Ξ» x β†’ pr₁(lemma₁ x)) , (Ξ» x β†’ prβ‚‚(lemma₁ x))
 where
  lemmaβ‚€ : (x : X) β†’ (A x + B x) β†’ Ξ£ b κž‰ 𝟚 , (b ＝ β‚€ β†’ A x) Γ— (b ＝ ₁ β†’ B x)
  lemmaβ‚€ x = which-of

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

\end{code}