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 --exact-split --safe #-}

open import SpartanMLTT
open import UF-FunExt

module ADecidableQuantificationOverTheNaturals (fe : funext U₀ U₀) where

open import Two
open import GenericConvergentSequence
open import SearchableTypes
open import GenericConvergentSequence
open import ConvergentSequenceSearchable fe
open import DecidableAndDetachable
open import DiscreteAndSeparated
open import UF-PropTrunc

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

   (Σ \(x : ℕ∞)  (x  ) × (p x  )) + ((n : )  p(under n)  )

Lemma-8·1 p = cases claim₀ claim₁ claim₂
 where
  claim₀ : (Σ \(y : ℕ∞)  p y  p(Succ y))
           (Σ \(x : ℕ∞)  (x  ) × (p x  )) + ((n : )  p(under n)  )
  claim₀ e = inl (𝟚-equality-cases case₀ case₁)
   where
    x : ℕ∞
    x = pr₁ e
    ne : p x  p(Succ x)
    ne = pr₂ e
    case₀ : p x    Σ \(x : ℕ∞)  (x  ) × (p x  )
    case₀ r = x , (s , r)
     where
      s : x  
      s t = ne(ap p (t  (Succ-∞-is-∞ fe)⁻¹  (ap Succ t)⁻¹))
    case₁ : p x    Σ \(x : ℕ∞)  (x  ) × (p x  )
    case₁ r = (Succ x) , (s , s')
     where
      s : Succ x  
      s t = ne (ap p (Succ-lc (t  (Succ-∞-is-∞ fe)⁻¹)  t ⁻¹))
      s' : p(Succ x)  
      s' = Lemma[b≢₁→b≡₀]  t  ne (r  t ⁻¹))

  claim₁ : ((y : ℕ∞)  p y  p(Succ y)) 
            (Σ \(x : ℕ∞)  (x  ) × (p x  )) + ((n : )  p(under n)  )
  claim₁ f = 𝟚-equality-cases case₀ case₁
   where
    case₀ : p Zero   
            (Σ \(x : ℕ∞)  (x  ) × (p x  )) + ((n : )  p(under n)  )
    case₀ r = inl(Zero , (s , r))
     where
      s : Zero  
      s t = ∞-is-not-ℕ 0 (t ⁻¹)
    case₁ : p Zero   
            (Σ \(x : ℕ∞)  (x  ) × (p x  )) + ((n : )  p(under n)  )
    case₁ r = inr by-induction
     where
      by-induction : (n : )  p(under n)  
      by-induction 0 = r
      by-induction (succ n) = (f(under n))⁻¹  by-induction n

  claim₂ : (Σ \(y : ℕ∞)  p y  p(Succ y)) + ((y : ℕ∞)  p y  p(Succ y))
  claim₂ = g(ℕ∞-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 = pr₁ f
    g : (Σ \(y : ℕ∞)  q y  ) + ((y : ℕ∞)  q y  )
      (Σ \(y : ℕ∞)  p y  p(Succ y)) + ((y : ℕ∞)  p y  p(Succ y))
    g(inl(y , r)) = inl(y , (pr₁ (pr₂ f y) r))
    g(inr h ) = inr y  discrete-is-separated
                           𝟚-discrete
                           (p y) (p(Succ y))
                           (pr₂ (pr₂ f y) (h y)))


Theorem-8·2 : (p : ℕ∞  𝟚)  decidable((n : )  p(under n)  )
Theorem-8·2 p = cases claim₀ claim₁ (Lemma-8·1 p)
 where
  claim₀ : (Σ \(x : ℕ∞)  (x  ) × (p x  )) 
            decidable((n : )  p(under n)  )
  claim₀ e = inr c₁
   where
    x : ℕ∞
    x = pr₁ e
    c₀ : ¬((n : )  x  under n)
    c₀ = λ g  pr₁(pr₂ e) (not-ℕ-is-∞ fe g)
    c₁ : ¬((n : )  p(under n)  )
    c₁ g = c₀ d
     where
      d : (n : )  x  under n
      d n r = Lemma[b≡₀→b≢₁] (pr₂(pr₂ e)) (ap p r  g n)
  claim₁ : ((n : )  p(under n)  )  decidable((n : )  p(under n)  )
  claim₁ f = inl f

\end{code}

Some examples:

\begin{code}

module examples where

    to-ℕ :  {U} {A : U ̇}  decidable A  
    to-ℕ (inl _) = 0
    to-ℕ (inr _) = 1

\end{code}

    0 means that (n : ℕ) → p(under n) ≡ ₁
    1 means that ¬((n : ℕ) → p(under n) ≡ ₁)

\begin{code}

    eval : (ℕ∞  𝟚)  
    eval p = to-ℕ (Theorem-8·2 p)

    p₀ : ℕ∞  𝟚
    p₀ _ = 

    p₁ : ℕ∞  𝟚
    p₁ _ = 

\end{code}

    If the first boolean is less than or equal to the second
    then it has value ₁; otherwise, it has value ₀.

\begin{code}

    _<=_ : 𝟚  𝟚  𝟚
     <= y = 
     <=  = 
     <=  = 

\end{code}

    If the two booleans are equal then it has value ₁;
    otherwise, it has value ₀.

\begin{code}

    _==_ : 𝟚  𝟚  𝟚
     ==  = 
     ==  = 
     ==  = 
     ==  = 

    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 (inl f) = inl (f 17)
    to-something p (inr _) = inr 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.