Martin Escardo 2011.

\begin{code}

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

module Exhaustible where

open import CurryHoward
open import Equality
open import Two

\end{code}

Definition:

\begin{code}

exhaustible : Set  Prp
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' : Set  Prp
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 : Set} 

 exhaustible X  exhaustible' X

exhaustible-implies-exhaustible' {X} φ = ∃-intro A lemma
 where A : (X  )  
       A p = ∃-witness(φ p)

       lemma : ∀(p : X  )  A p    (∀(x : X)  p x  )
       lemma p = ∃-elim(φ p)

open import Searchable

searchable-implies-exhaustible : {X : Set} 

 searchable X  exhaustible X

searchable-implies-exhaustible {X} ε p = ∃-intro y (∧-intro lemma₀ lemma₁)
 where 
  x₀ : X
  x₀ = ∃-witness(ε p)

  y :  
  y = p x₀

  lemma₀ :  y    ∀(x : X)  p x  
  lemma₀ = ∃-elim(ε p)

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

\end{code}