Martin Escardo 2011.

\begin{code}

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

module NotionsOfDecidability.Decidable where

open import MLTT.Spartan

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

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

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

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

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

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

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

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

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

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

    h : decidable(Y x) β†’ 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 : π“₯ Μ‡ }
                         β†’ decidable A
                         β†’ decidable B
                         β†’ 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 : π“₯ Μ‡ }
                         β†’ decidable A
                         β†’ decidable B
                         β†’ 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 : π“₯ Μ‡ }
                         β†’ decidable A
                         β†’ decidable B
                         β†’ 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 β†’  decidable A)
                          β†’ decidable B
                          β†’ decidable (A β†’ B)
β†’-preserves-decidability' Ο† (inl b) = inl (Ξ» _ β†’ b)
β†’-preserves-decidability' {𝓀} {π“₯} {A} {B} Ο† (inr v) = Ξ³ (Ο† v)
 where
  Ξ³ : decidable A β†’ decidable (A β†’ B)
  Ξ³ (inl a) = inr (Ξ» f β†’ v (f a))
  Ξ³ (inr u) = inl (Ξ» a β†’ 𝟘-elim (u a))

β†’-preserves-decidability'' : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ }
                           β†’ decidable A
                           β†’ (A β†’ decidable B)
                           β†’ decidable (A β†’ B)
β†’-preserves-decidability'' {𝓀} {π“₯} {A} {B} (inl a) Ο† = Ξ³ (Ο† a)
 where
  Ξ³ : decidable B β†’ 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 : 𝓀 Μ‡ }
                         β†’ decidable A
                         β†’ decidable(Β¬ A)
Β¬-preserves-decidability d = β†’-preserves-decidability d 𝟘-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 : 𝓀 Μ‡ }
              β†’ 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}