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 ∞.


{-# 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


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


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

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

incl : ℕ∞  ₂ℕ
incl = π₀

incl-mono : injective incl
incl-mono = π₀-mono at-most-one 
  at-most-one : ∀{α : ₂ℕ}  ∀(p q : decreasing α)  p  q
  at-most-one {α} p q = extensionality fact₂
    open import UIP
    fact₀ : ∀{i}  ∀(f g : α(succ i)    α i  )  f  g
    fact₀ f g = extensionality fact₁
      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')
  α' : ₂ℕ
  α' 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)
  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)
  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)
  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
  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))
  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
      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
      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)
  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
  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))


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) ≡ ₀.


finite-isolated : 

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

finite-isolated u 0 = two-equality-cases lemma₀ lemma₁
  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₁
  lemma₀ :  incl u n    u  under(succ n)  u  under(succ n) 
  lemma₀ r = in₁(contra-positive lemma (Lemma[b≡₀→b≠₁] r))
    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₁₁
    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))
      lemma : u  under(succ n)  incl u (succ n)  
      lemma r = trans (cong  v  incl v (succ n)) r) (under-diagonal₀(succ n))