By Martin Escardo, 2 September 2011.

Modified in December 2011 assuming the axiom of extensionality (which
is not used directly in this module, but instead in
GenericConvergentSequence).

We prove that the generic convergent sequence ℕ∞ is searchable, which
amounts to Theorem-3·6 of the paper

   http://www.cs.bham.ac.uk/~mhe/papers/omniscient.pdf, 
   http://www.cs.bham.ac.uk/~mhe/.talks/dagstuhl2011/omniscient.pdf

and conclude as a corollary that it is searchable and satisfies the
principle of omniscience.

\begin{code}

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

\end{code}


(Continuity axioms and the fan principle are not assumed.)

\begin{code}

open import SpartanMLTT
open import UF-FunExt
open import UF-PropTrunc
open import GenericConvergentSequence
open import SearchableTypes

module ConvergentSequenceSearchable (fe : FunExt U₀ U₀) where

\end{code}

This is the main theorem proved in this module:

\begin{code}

ℕ∞-is-searchable : searchable ℕ∞
ℕ∞-is-searchable p = a , Lemma
 where 
  α :   𝟚
  α 0       = p(under 0)
  α(succ n) = min𝟚 (α n) (p(under(succ n)))

  a : ℕ∞
  a = (α , λ i  Lemma[minab≤a])

  Dagger₀ : (n : )  a  under n  p(under n)  
  Dagger₀ 0 r =  ap  w  incl w 0) r
  Dagger₀ (succ n) r = w ⁻¹  t  under-diagonal₀ n
   where 
    s : α n  incl (under (succ n)) n
    s = ap  w  incl w n) r

    t : α(succ n)  incl (under (succ n)) (succ n)
    t = ap  w  incl w (succ n)) r

    w : α(succ n)  p(under(succ n)) 
    w = ap  b  min𝟚 b (p(under(succ n)))) (s under-diagonal₁ n)

  Dagger₁ : a    (n : )  p(under n)  
  Dagger₁ r 0 = ap  w  incl w 0) r
  Dagger₁ r (succ n) = w ⁻¹  t
   where 
    s : α n  
    s = ap  w  incl w n) r

    t : α(succ n)  
    t = ap  w  incl w (succ n)) r

    w : α(succ n)  p(under(succ n))
    w = ap  b  min𝟚 b (p(under(succ n)))) s

  Claim₀ : p a    (n : )  a  under n
  Claim₀ r n s = Lemma[b≡₁→b≢₀] r (Lemma s)
   where 
    Lemma : a  under n  p a  
    Lemma t = ap p t  Dagger₀ n t

  Claim₁ : p a    a  
  Claim₁ r = not-ℕ-is-∞ fe (Claim₀ r) 

  Claim₂ : p a    (n : )  p(under n)  
  Claim₂ r = Dagger₁(Claim₁ r)

  Claim₃ : p a    p   
  Claim₃ r = (ap p (Claim₁ r))⁻¹  r

  Lemma : p a    (v : ℕ∞)  p v  
  Lemma r = ℕ∞-density fe (Claim₂ r) (Claim₃ r)

\end{code}

Corollaries:

\begin{code}

open import OmniscientTypes
open import DiscreteAndSeparated

ℕ∞-is-omniscient : omniscient ℕ∞
ℕ∞-is-omniscient = searchable-implies-omniscient (ℕ∞-is-searchable)

ℕ∞→ℕ-discrete : discrete(ℕ∞  )
ℕ∞→ℕ-discrete = omniscient-discrete-discrete fe ℕ∞-is-omniscient  u  ℕ-discrete)

ℕ∞→𝟚-discrete : discrete(ℕ∞  𝟚)
ℕ∞→𝟚-discrete = omniscient-discrete-discrete fe ℕ∞-is-omniscient  u  𝟚-discrete)

module _ (fe' :  U V  FunExt U V) (pt : PropTrunc) where

 open import 2CompactTypes (fe') (pt)
  
 ℕ∞-is-strongly-𝟚-overt : strongly-𝟚-overt ℕ∞
 ℕ∞-is-strongly-𝟚-overt = omniscient-Compact ℕ∞-is-omniscient

 ℕ∞-is-𝟚-compact : 𝟚-compact ℕ∞
 ℕ∞-is-𝟚-compact = 𝟚-so-c ℕ∞-is-strongly-𝟚-overt


\end{code}