Chuangjie Xu, 2012. 

This is an Agda formalization of Theorem 8.2 of the extended version
of Escardo's paper "Infinite sets that satisfy the principle of
omniscience in all varieties of constructive mathematics", Journal of
Symbolic Logic, volume 78, number 3, September 2013, pages 764-784.

The theorem says that, for any p : ℕ∞ → ₂, the proposition
∀(n : ℕ) → p(under n) ≡ ₁ is decidable. 

\begin{code}

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

module ADecidableQuantificationOverTheNaturals where

open import CurryHoward
open import Equality
open import Naturals
open import Two 
open import Cantor
open import GenericConvergentSequence
open import ConvergentSequenceSearchable
open import DecidableAndDetachable
open import SetsAndFunctions
open import DiscreteAndSeparated

Lemma-8·1 : ∀(p : ℕ∞  )  

   ( \(x : ℕ∞)  x    p x  ) 
  (∀(n : )  p(under n)  )

Lemma-8·1 p = ∨-elim claim₀ claim₁ claim₂
 where
  claim₀ : ( \(y : ℕ∞)  p y  p(Succ y))
           ( \(x : ℕ∞)  x    p x  ) 
           (∀(n : )  p(under n)  )
  claim₀ e = ∨-intro₀ (two-equality-cases case₀ case₁)
   where
    x : ℕ∞
    x = ∃-witness e
    ne : p x  p(Succ x)
    ne = ∃-elim e
    case₀ : p x     \(x : ℕ∞)  x    p x  
    case₀ r = ∃-intro x (∧-intro s r)
     where 
      s : x  
      s t = ne(cong p (Lemma[x≡z→y≡z→x≡y]
                         t (trans (cong Succ t) Succ-∞-is-∞)))
    case₁ : p x     \(x : ℕ∞)  x    p x  
    case₁ r = ∃-intro (Succ x) (∧-intro s s')
     where 
      s : Succ x  
      s t = ne (cong p (Lemma[x≡z→y≡z→x≡y] 
                         (Succ-mono (Lemma[x≡z→y≡z→x≡y] t Succ-∞-is-∞)) t))
      s' : p(Succ x)  
      s' = Lemma[b≢₁→b≡₀]  t  ne (Lemma[x≡z→y≡z→x≡y] r t))

  claim₁ : (∀(y : ℕ∞)  p y  p(Succ y)) 
            ( \(x : ℕ∞)  x    p x  ) 
            (∀(n : )  p(under n)  )
  claim₁ f = two-equality-cases case₀ case₁
   where
    case₀ : p Zero   
            ( \(x : ℕ∞)  x    p x  ) 
            (∀(n : )  p(under n)  )
    case₀ r = ∨-intro₀(∃-intro Zero (∧-intro s r))
     where
      s : Zero  
      s t = ∞-is-not-ℕ 0 (sym t)
    case₁ : p Zero   
            ( \(x : ℕ∞)  x    p x  ) 
            (∀(n : )  p(under n)  )
    case₁ r = ∨-intro₁ by-induction
     where
      by-induction : ∀(n : )  p(under n)  
      by-induction 0 = r
      by-induction (succ n) = trans (sym(f(under n))) (by-induction n)

  claim₂ : ( \(y : ℕ∞)  p y  p(Succ y)) 
           (∀ (y : ℕ∞)  p y  p(Succ y))
  claim₂ = g(ℕ∞-is-omniscient q)
   where
    fact : ∀(y : ℕ∞)  p y  p(Succ y)  ¬(p y  p(Succ y))
    fact y = negation-preserves-decidability(₂-discrete (p y) (p(Succ y)))

    f :  \(q : ℕ∞  )   y  (q y    p y  p(Succ y))
                                 (q y    ¬(p y  p(Succ y)))
    f = characteristic-function fact
    q : ℕ∞  
    q = ∃-witness f
    g : ( \(y : ℕ∞)  q y  )  (∀(y : ℕ∞)  q y  ) 
      ( \(y : ℕ∞)  p y  p(Succ y))  (∀(y : ℕ∞)  p y  p(Succ y))
    g(in₀(y , r)) = in₀(∃-intro y (∧-elim₀ (∃-elim f y) r))
    g(in₁ h ) = in₁ y  discrete-is-separated 
                           ₂-discrete 
                           (p y) (p(Succ y)) 
                           (∧-elim₁ (∃-elim f y) (h y)))


Theorem-8·2 : ∀(p : ℕ∞  )  decidable(∀(n : )  p(under n)  )
Theorem-8·2 p = ∨-elim claim₀ claim₁ (Lemma-8·1 p)
 where
  claim₀ : ( \(x : ℕ∞)  x    p x  ) 
            decidable(∀(n : )  p(under n)  )
  claim₀ e = ∨-intro₁ c₁
   where
    x : ℕ∞
    x = ∃-witness e
    c₀ : ¬(∀(n : )  x  under n)
    c₀ = λ g  ∧-elim₀(∃-elim e) (not-ℕ-is-∞ g)
    c₁ : ¬(∀(n : )  p(under n)  )
    c₁ g = c₀ d
     where
      d : ∀(n : )  x  under n
      d n r = Lemma[b≡₀→b≢₁] (∧-elim₁(∃-elim e)) (trans (cong p r) (g n))
  claim₁ : (∀(n : )  p(under n)  )  decidable(∀(n : )  p(under n)  )
  claim₁ f = ∨-intro₀ f

\end{code}

Some examples:

\begin{code}

to-ℕ : {A : Set}  decidable A  
to-ℕ (in₀ _) = 0
to-ℕ (in₁ _) = 1

-- 0 means that ∀(n : ℕ) → p(under n) ≡ ₁
-- 1 means that ¬(∀(n : ℕ) → p(under n) ≡ ₁)
eval : (ℕ∞  )  
eval p = to-ℕ (Theorem-8·2 p)

p₀ : ℕ∞  
p₀ _ = 

p₁ : ℕ∞  
p₁ _ = 

-- If the first boolean is less than or equal to the second#
-- then it returns ₁; otherwise, it returns ₀.
_<=_ :     
 <= _ = 
_ <=  = 
_ <= _ = 

-- If the two booleans are equal then it returns ₁;
-- otherwise, it returns ₀.
_==_ :     
 ==  = 
 ==  = 
_ == _ = 

p₂ : ℕ∞  
p₂ (α , _) = α 10 <= α 1

p₃ : ℕ∞  
p₃ (α , _) = α 0 <= α 1

p₄ : ℕ∞  
p₄ (α , _) = α 5 == α 100

to-something : (p : ℕ∞  )  decidable (∀(n : )  p(under n)  )  p(under 17)    
to-something p (in₀ f) = in₀ (f 17)
to-something p (in₁ _) = in₁ 1070

eval1 : (p : ℕ∞  )  p(under 17)    
eval1 p = to-something p (Theorem-8·2 p)

\end{code}

Despite the fact that we use function extensionality, eval pi
evaluates to a numeral for i=0,...,4.