Martin Escardo 2011.

\begin{code}

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

module DecidableAndDetachable where

open import SpartanMLTT

open import Plus-Properties
open import Two-Properties
open import UF-Subsingletons
open import UF-PropTrunc

\end{code}

We look at decidable propositions and subsets (using the terminogy
"detachable" for the latter").

\begin{code}

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

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

\end{code}

Digression: https://twitter.com/EgbertRijke/status/1429443868450295810

"decidable" is almost a monad, except that it is not even functorial:

\begin{code}

module EgbertRijkeTwitterDiscussion-22-August-2021-not-a-monad where

  open import UF-Equiv

  T : 𝓀 Μ‡ β†’ 𝓀 Μ‡
  T = decidable

  Ξ· : (X : 𝓀 Μ‡ ) β†’ X β†’ T X
  Ξ· X = pointed-decidable

  ΞΌ : (X : 𝓀 Μ‡ ) β†’ T (T X) β†’ T X
  ΞΌ X (inl Ξ΄) = Ξ΄
  ΞΌ X (inr u) = inr (Ξ» x β†’ u (inl x))

  ΞΌΞ· : (X : 𝓀 Μ‡ ) β†’ ΞΌ X ∘ Ξ· (T X) ∼ id
  ΞΌΞ· X (inl x) = refl
  ΞΌΞ· X (inr u) = refl

  Ξ·ΞΌ : (X : 𝓀 Μ‡ ) β†’ Ξ· (T X) ∘ ΞΌ X ∼ id
  Ξ·ΞΌ X (inl (inl x)) = refl
  Ξ·ΞΌ X (inl (inr u)) = refl
  Ξ·ΞΌ X (inr u) = 𝟘-elim (u (inr (Ξ» x β†’ u (inl x))))

  ΞΌ-is-invertible : (X : 𝓀 Μ‡ ) β†’ invertible (ΞΌ X)
  ΞΌ-is-invertible X = Ξ· (T X) , Ξ·ΞΌ X , ΞΌΞ· X

  ΞΌ-≃ : (X : 𝓀 Μ‡ ) β†’ T (T X) ≃ T X
  ΞΌ-≃ X = qinveq (ΞΌ X) (ΞΌ-is-invertible X)

  raw-T-algebras-are-non-empty : {X : 𝓀 Μ‡ } (Ξ± : T X β†’ X) β†’ is-nonempty X
  raw-T-algebras-are-non-empty Ξ± u = u (Ξ± (inr u))

  retraction-of-Ξ·-is-section : {A : 𝓀 Μ‡ } (Ξ± : T A β†’ A)
                             β†’ Ξ± ∘ Ξ· A ∼ id
                             β†’ Ξ· A ∘ Ξ± ∼ id
  retraction-of-Ξ·-is-section Ξ± h (inl a) = ap inl (h a)
  retraction-of-η-is-section α h (inr u) = 𝟘-elim (raw-T-algebras-are-non-empty α u)

  section-of-Ξ·-is-retraction : {A : 𝓀 Μ‡ } (Ξ± : T A β†’ A)
                             β†’ Ξ· A ∘ Ξ± ∼ id
                             β†’ Ξ± ∘ Ξ· A ∼ id
  section-of-Ξ·-is-retraction Ξ± k a = inl-lc (k (inl a))

  η⁻¹ : {A : 𝓀 Μ‡ } β†’ is-nonempty A β†’ (T A β†’ A)
  η⁻¹ Ο• (inl a) = a
  η⁻¹ Ο• (inr u) = 𝟘-elim (Ο• u)

  η⁻¹-is-retraction : {A : 𝓀 Μ‡ } (Ο• : is-nonempty A) β†’ η⁻¹ Ο• ∘ Ξ· A ∼ id
  η⁻¹-is-retraction Ο• a = refl

  η⁻¹-is-section : {A : 𝓀 Μ‡ } (Ο• : is-nonempty A) β†’ Ξ· A ∘ η⁻¹ Ο• ∼ id
  η⁻¹-is-section Ο• = retraction-of-Ξ·-is-section (η⁻¹ Ο•) (η⁻¹-is-retraction Ο•)

  Ξ·-invertible-gives-non-empty : {X : 𝓀 Μ‡ } β†’ invertible (Ξ· X) β†’ is-nonempty X
  Ξ·-invertible-gives-non-empty (Ξ± , _ , _) = raw-T-algebras-are-non-empty Ξ±

  non-empty-gives-Ξ·-invertible : {X : 𝓀 Μ‡ } β†’ is-nonempty X β†’ invertible (Ξ· X)
  non-empty-gives-Ξ·-invertible {𝓀} {X} Ο• = η⁻¹ Ο• , η⁻¹-is-retraction Ο• , η⁻¹-is-section Ο•

  Ξ·-≃ : (X : 𝓀 Μ‡ ) β†’ is-nonempty X β†’ X ≃ T X
  Ξ·-≃ X Ο• = qinveq (Ξ· X) (non-empty-gives-Ξ·-invertible Ο•)

  retractions-of-Ξ·-are-invertible : {A : 𝓀 Μ‡ } (Ξ± : T A β†’ A)
                                  β†’ Ξ± ∘ Ξ· A ∼ id
                                  β†’ invertible Ξ±
  retractions-of-Ξ·-are-invertible {𝓀} {A} Ξ± h = Ξ· A , retraction-of-Ξ·-is-section Ξ± h , h

  retractions-of-Ξ·-are-unique : {A : 𝓀 Μ‡ } (Ξ± : T A β†’ A)
                              β†’ Ξ± ∘ Ξ· A ∼ id
                              β†’ (Ο• : is-nonempty A) β†’ Ξ± ∼ η⁻¹ Ο•
  retractions-of-Ξ·-are-unique Ξ± h Ο• (inl a) = h a
  retractions-of-Ξ·-are-unique Ξ± h Ο• (inr u) = 𝟘-elim (Ο• u)

  is-proto-algebra : 𝓀 Μ‡ β†’ 𝓀 Μ‡
  is-proto-algebra A = Ξ£ Ξ± κž‰ (T A β†’ A) , Ξ± ∘ Ξ· A ∼ id

  proto-algebras-are-non-empty : {A : 𝓀 Μ‡ } β†’ is-proto-algebra A β†’ is-nonempty A
  proto-algebras-are-non-empty (Ξ± , _) = raw-T-algebras-are-non-empty Ξ±

  nonempty-types-are-proto-algebras : {A : 𝓀 Μ‡ } β†’ is-nonempty A β†’ is-proto-algebra A
  nonempty-types-are-proto-algebras Ο• = η⁻¹ Ο• , η⁻¹-is-retraction Ο•

\end{code}

End of digression.

\begin{code}

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

Γ—-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:

\begin{code}

indicator : {X : 𝓀 Μ‡ } β†’ {A 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}

We again have a particular case of interest.  Detachable subsets,
defined below, are often known as decidable subsets. Agda doesn't
allow overloading of terminology, and hence we gladly accept the
slighly non-universal terminology.

\begin{code}

detachable : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡
detachable A = βˆ€ x β†’ decidable(A x)

characteristic-function : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
                        β†’ detachable A
                        β†’ Ξ£ p κž‰ (X β†’ 𝟚) , ((x : X) β†’ (p x ≑ β‚€ β†’   A x)
                                                   Γ— (p x ≑ ₁ β†’ Β¬ (A x)))
characteristic-function = indicator

co-characteristic-function : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
                           β†’ detachable A
                           β†’ Ξ£ p κž‰ (X β†’ 𝟚) , ((x : X) β†’ (p x ≑ β‚€ β†’ Β¬ (A x))
                                                      Γ— (p x ≑ ₁ β†’   A x))
co-characteristic-function d = indicator(Ξ» x β†’ +-commutative(d x))

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)

\end{code}

Notice that p is unique (Agda exercise - you will need function
extensionality).

Don't really have a good place to put this:

\begin{code}

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

 open PropositionalTruncation pt

 not-existsβ‚€-implies-forall₁ : {X : 𝓀 Μ‡ } (p : X β†’ 𝟚)
                            β†’ Β¬ (βˆƒ x κž‰ X , p x ≑ β‚€)
                            β†’ βˆ€ (x : X) β†’ p x ≑ ₁
 not-existsβ‚€-implies-forall₁ p u x = different-from-β‚€-equal-₁ (not-Ξ£-implies-Ξ -not (u ∘ ∣_∣) x)

 forall₁-implies-not-existsβ‚€ : {X : 𝓀 Μ‡ } (p : X β†’ 𝟚)
                            β†’ (βˆ€ (x : X) β†’ p x ≑ ₁)
                            β†’ Β¬ (βˆƒ x κž‰ X , p x ≑ β‚€)
 forall₁-implies-not-existsβ‚€ {𝓀} {X} p Ξ± = βˆ₯βˆ₯-rec 𝟘-is-prop h
  where
   h : (Ξ£ x κž‰ X , p x ≑ β‚€) β†’ 𝟘
   h (x , r) = zero-is-not-one (r ⁻¹ βˆ™ Ξ± x)

\end{code}