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


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 α

decreasing-is-hprop : ∀{α : ₂ℕ}  hprop(decreasing α)
decreasing-is-hprop {α} p q = funext fact₂
  fact₀ : ∀{i}  ∀(f g : α(succ i)    α i  )  f  g
  fact₀ f g = funext fact₁
    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')
  α' : ₂ℕ
  α' 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)
  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)
  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)
  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(funext(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(funext 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)) 

Order on ℕ∞:


_≼_ : 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
  t : decreasing  i  max₂ (α i) (β i))
  t i p = max₂-lemma-converse (α i) (β i) (f (max₂-lemma(α(succ i)) (β(succ i)) p))
     f : α(succ i)   + β(succ i)    α i   + β i  
     f (in₀ p) = in₀ (r i p)
     f (in₁ p) = in₁ (s i p)


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