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}