Martin Escardo 2012.

See my paper "Infinite sets that satisfy the principle of
omniscience" for a discussion of the type ℕ∞ defined here. 
Essentially, ℕ∞ is ℕ with an added point ∞.

\begin{code}

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

module GenericConvergentSequence where

open import CurryHoward
open import Equality
open import Extensionality
open import Naturals
open import Two
open import Cantor
open import SetsAndFunctions
open import FirstProjectionInjective
open import Injection

\end{code}

Definition (The generic convergent sequence).
We use u,v to range over ℕ∞ and α,β to range over ₂ℕ:

\begin{code}

decreasing : ₂ℕ  Prp
decreasing α = ∀(i : )  α i  α(succ i)

ℕ∞ : Set
ℕ∞ = Σ \(α : ₂ℕ)  decreasing α

incl : ℕ∞  ₂ℕ
incl = π₀

incl-mono : injective incl
incl-mono = π₀-mono at-most-one 
 where 
  at-most-one : ∀{α : ₂ℕ}  ∀(p q : decreasing α)  p  q
  at-most-one {α} p q = extensionality fact₂
   where 
    open import UIP
    fact₀ : ∀{i}  ∀(f g : α(succ i)    α i  )  f  g
    fact₀ f g = extensionality fact₁
     where
      fact₁ :  r  f r  g r
      fact₁ r = UIP  (f r) (g r)
    fact₂ :  i  p i  q i
    fact₂ i = fact₀ (p i) (q i) 


Zero : ℕ∞
Zero = ((λ i  ) , λ i  id {  })

Succ : ℕ∞  ℕ∞
Succ (α , reason) = (α' , reason')
 where 
  α' : ₂ℕ
  α' 0 = 
  α'(succ n) = α n
  reason' : decreasing α'
  reason' 0 = λ r  refl
  reason' (succ i) = reason i

positivity : ℕ∞  
positivity u = incl u 0 

isZero : ℕ∞  Prp
isZero u = positivity u  

positive : ℕ∞  Prp
positive u = positivity u  

isZero-Zero : isZero Zero
isZero-Zero = refl

Zero-not-Succ : ∀{u : ℕ∞}  Zero  Succ u
Zero-not-Succ {u} r = zero-is-not-one(cong positivity r)


 : ℕ∞
 = ((λ i  ) , λ i  id {  })

Succ-∞-is-∞ : Succ   
Succ-∞-is-∞ = incl-mono(extensionality lemma) 
 where lemma :  i  incl(Succ ) i  incl  i
       lemma 0 = refl
       lemma (succ i) = refl


unique-fixed-point-of-Succ :  u  u  Succ u  u  
unique-fixed-point-of-Succ u r = incl-mono(extensionality lemma)
 where
  fact :  i  incl u i  incl(Succ u) i 
  fact i = cong  w  incl w i) r
  lemma :  i  incl u i  
  lemma 0 = fact 0
  lemma (succ i) = trans (fact(succ i)) (lemma i) 



Pred : ℕ∞  ℕ∞
Pred (α , reason) = (α  succ , reason  succ)

Pred-Zero-is-Zero : Pred Zero  Zero
Pred-Zero-is-Zero = refl 

Pred-Succ-u-is-u : ∀{u : ℕ∞}  Pred(Succ u)  u
Pred-Succ-u-is-u {u} = refl

Pred-∞-is-∞ : Pred   
Pred-∞-is-∞ = refl

Succ-mono : injective Succ
Succ-mono = cong Pred

under :   ℕ∞
under 0 = Zero
under (succ n) = Succ(under n)

_≣_ : ℕ∞    Prp
u  n = u  under n


under-mono : injective under
under-mono {0} {0} r = refl
under-mono {0} {succ n} r = ⊥-elim(Zero-not-Succ r)
under-mono {succ m} {0} r = ⊥-elim(Zero-not-Succ (sym r))
under-mono {succ m} {succ n} r = cong succ (under-mono {m} {n} (Succ-mono r))


under-diagonal₀ : 

  ∀(n : )  incl(under n) n  

under-diagonal₀ 0 = refl
under-diagonal₀ (succ n) = under-diagonal₀ n


under-diagonal₁ : 

  ∀(n : )  incl(under(succ n)) n  

under-diagonal₁ 0 = refl
under-diagonal₁ (succ n) = under-diagonal₁ n
 

isZero-equal-Zero : 

  ∀{u : ℕ∞}  isZero u  u  Zero

isZero-equal-Zero {u} base = incl-mono(extensionality lemma)
 where 
  lemma : ∀(i : )  incl u i  incl Zero i
  lemma 0 = base
  lemma (succ i) = Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] (π₁ u i) (lemma i)

not-Zero-is-Succ : ∀{u : ℕ∞}  u  Zero  u  Succ(Pred u)
not-Zero-is-Succ {u} f = incl-mono(extensionality lemma)
 where 
  lemma :  i  incl u i  incl(Succ(Pred u)) i 
  lemma 0 = Lemma[b≠₀→b≡₁](f  isZero-equal-Zero)
  lemma (succ i) = refl

positive-is-not-Zero : ∀{u : ℕ∞}  positive u  u  Zero
positive-is-not-Zero {u} r s = lemma r
 where
  lemma : ¬(positive u)
  lemma = Lemma[b≡₀→b≠₁](cong positivity s)

positive-equal-Succ : 

  ∀{u : ℕ∞}  positive u  u  Succ(Pred u)

positive-equal-Succ r = 
 not-Zero-is-Succ (positive-is-not-Zero r)


Succ-criterion :

  ∀{u : ℕ∞}  ∀{n}  incl u n    incl u(succ n)    u  Succ(under n)

Succ-criterion {u} {n} r s = incl-mono(extensionality(lemma u n r s))
 where 
  lemma :  u   n  incl u n    incl u(succ n)   
          i  incl u i  incl (Succ(under n)) i
  lemma u 0 r s 0 = r
  lemma u 0 r s (succ i) = lemma₀ i
     where 
      lemma₀ :  i  incl u (succ i)   
      lemma₀ 0 = s
      lemma₀ (succ i) = Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] (π₁ u (succ i)) (lemma₀ i)
  lemma u (succ n) r s 0 = lemma₁ (succ n) r
     where 
      lemma₁ :  n  incl u n    positive u
      lemma₁ 0 t = t
      lemma₁ (succ n) t = lemma₁ n (π₁ u n t)
  lemma u (succ n) r s (succ i) = lemma (Pred u) n r s i


∞-is-not-ℕ : ∀(n : )    under n
∞-is-not-ℕ n s = 
 zero-is-not-one (sym(trans (cong  w  incl w n) s) (under-diagonal₀ n)))



not-ℕ-is-∞ : 

  ∀{u : ℕ∞}  (∀(n : )  u  under n)  u  

not-ℕ-is-∞ {u} f = incl-mono(extensionality lemma)
 where 
  lemma : ∀(n : )  incl u n  
  lemma 0 = Lemma[b≠₀→b≡₁] r  f 0 (isZero-equal-Zero r))
  lemma (succ n) = Lemma[b≠₀→b≡₁] r  f(succ n)(Succ-criterion (lemma n) r))


ℕ∞-density : 

  ∀{p : ℕ∞  }  (∀ n  p(under n)  )  p      u  p u  

ℕ∞-density {p} f r u = Lemma[b≠₀→b≡₁] lemma
 where 
  claim : p u    ∀(n : )  u  under n
  claim g n = contra-positive  s  trans(cong p s) (f n))(Lemma[b≡₀→b≠₁] g)

  claim-∞ : p u    u  
  claim-∞ = (contra-positive  s  trans(cong p s) r))  Lemma[b≡₀→b≠₁]

  lemma : p u  
  lemma t = claim-∞ t (not-ℕ-is-∞(claim t))

\end{code}

There should be a better proof of the following. The idea is simple:
by the above development, u = under 0 if and only if incl u 0 ≡ 0, and
u ≡ under(n+1) if and only incl u n ≡ ₁ and incl u (n+1) ≡ ₀.

\begin{code}

finite-isolated : 

 ∀(u : ℕ∞)  ∀(n : )  u  under n    u  under n

finite-isolated u 0 = two-equality-cases lemma₀ lemma₁
 where 
  lemma₀ : isZero u  u  Zero  u  Zero
  lemma₀ r = in₀(isZero-equal-Zero r)
  lemma₁ : positive u  u  Zero  u  Zero
  lemma₁ r = in₁(contra-positive fact (Lemma[b≡₁→b≠₀] r))
    where fact : u  Zero  isZero u
          fact r = cong  u  incl u 0) r
finite-isolated u (succ n) = two-equality-cases lemma₀ lemma₁
 where
  lemma₀ :  incl u n    u  under(succ n)  u  under(succ n) 
  lemma₀ r = in₁(contra-positive lemma (Lemma[b≡₀→b≠₁] r))
   where
    lemma : u  under(succ n)  incl u n  
    lemma r = trans (cong  v  incl v n) r) (under-diagonal₁ n)
  lemma₁ :  incl u n    u  under(succ n)  u  under(succ n)
  lemma₁ r = two-equality-cases lemma₁₀ lemma₁₁
   where
    lemma₁₀ :  incl u (succ n)    u  under(succ n)  u  under(succ n) 
    lemma₁₀ s = in₀(Succ-criterion r s)
    lemma₁₁ :  incl u (succ n)    u  under(succ n)  u  under(succ n) 
    lemma₁₁ s = in₁ (contra-positive lemma (Lemma[b≡₁→b≠₀] s))
     where
      lemma : u  under(succ n)  incl u (succ n)  
      lemma r = trans (cong  v  incl v (succ n)) r) (under-diagonal₀(succ n)) 
\end{code}