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 hiding (_+_) hiding (_≣_)
open import Two
open import Cantor
open import SetsAndFunctions
open import FirstProjectionInjective
open import Injection
open import Embedding
open import HSets 
open import DiscreteAndSeparated

\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 α

decreasing-is-hprop : ∀{α : ₂ℕ}  hprop(decreasing α)
decreasing-is-hprop {α} p q = funext fact₂
 where
  fact₀ : ∀{i}  ∀(f g : α(succ i)    α i  )  f  g
  fact₀ f g = funext fact₁
   where
    fact₁ :  r  f r  g r
    fact₁ r = ₂-hset (f r) (g r)
  fact₂ :  i  p i  q i
  fact₂ i = fact₀ (p i) (q i) 

incl : ℕ∞  ₂ℕ
incl = π₀

incl-mono : left-cancellable incl
incl-mono = π₀-mono decreasing-is-hprop

ℕ∞-separated : separated ℕ∞
ℕ∞-separated = subtype-of-separated-is-separated π₀ incl-mono ₂ℕ-separated

ℕ∞-hset : hset ℕ∞
ℕ∞-hset = separated-is-hset ℕ∞-separated

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(funext 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(funext 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 : left-cancellable Succ
Succ-mono = cong Pred

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

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

under-mono : left-cancellable 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-embedding : embedding under
under-embedding x (x₀ , r₀) (x₁ , r₁) = 
 Σ-≡ x₀ x₁ r₀ r₁ (under-mono(trans (sym r₀) r₁)) (ℕ∞-hset (subst {}  n  x  under n} (under-mono {x₀} (trans (sym r₀) r₁)) r₀) r₁) 

under-mono-refl :  k  under-mono refl  (refl {} {k})
under-mono-refl 0 = refl
under-mono-refl (succ k) = cong (cong succ) (under-mono-refl k)

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(funext 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(funext 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(funext(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(funext 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}

Order on ℕ∞:

\begin{code}

_≼_ : bin-rel ℕ∞
u  v =  n  incl u n  incl v n

∞-greatest : ∀(u : ℕ∞)  u  
∞-greatest u = λ n _  refl

max : ℕ∞  ℕ∞  ℕ∞
max (α , r) (β , s) =  i  max₂ (α i) (β i)) , t
 where
  t : decreasing  i  max₂ (α i) (β i))
  t i p = max₂-lemma-converse (α i) (β i) (f (max₂-lemma(α(succ i)) (β(succ i)) p))
    where
     f : α(succ i)   + β(succ i)    α i   + β i  
     f (in₀ p) = in₀ (r i p)
     f (in₁ p) = in₁ (s i p)

\end{code}

More lemmas about order should be added, but I will do this on demand
as the need arises.