Martin Escardo 2011.

\begin{code}

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

module Exhaustible where

open import SpartanMLTT
open import Two

\end{code}

Definition:

\begin{code}

exhaustible : U  U
exhaustible X = (p : X  𝟚)  Σ \(y : 𝟚)  y    ((x : X)  p x  )

\end{code}

Closer to the original definition of exhaustibility in LICS'2007 amd LMCS'2008:

\begin{code}

exhaustible' : U  U
exhaustible' X = 
 Σ \(A : (X  𝟚)  𝟚)  (p : X  𝟚)  A p    ((x : X)  p x  )

\end{code}

Because the axiom of choice holds in MLTT:

\begin{code}

exhaustible-implies-exhaustible' : {X : U} 

 exhaustible X  exhaustible' X

exhaustible-implies-exhaustible' {X} φ = A , lemma
 where A : (X  𝟚)  𝟚
       A p = pr₁(φ p)

       lemma : (p : X  𝟚)  A p    ((x : X)  p x  )
       lemma p = pr₂(φ p)

open import Searchable

searchable-implies-exhaustible : {X : U} 

 searchable X  exhaustible X

searchable-implies-exhaustible {X} ε p = y , (lemma₀ , lemma₁)
 where 
  x₀ : X
  x₀ = pr₁(ε p)

  y : 𝟚 
  y = p x₀

  lemma₀ :  y    (x : X)  p x  
  lemma₀ = pr₂(ε p)

  lemma₁ : ((x : X)  p x  )  y  
  lemma₁ h = h x₀

\end{code}