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 --exact-split --safe #-}

module GenericConvergentSequence where

open import SpartanMLTT
open import Naturals
open import Two
open import FirstProjectionInjective
open import Injection
open import Embedding
open import Sets 
open import DiscreteAndSeparated

\end{code}

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

\begin{code}

decreasing : (  𝟚)  U
decreasing α = (i : )  α i  α(succ i)

ℕ∞ : U
ℕ∞ = Σ \(α :   𝟚)  decreasing α

decreasing-is-prop : {α :   𝟚}  isProp(decreasing α)
decreasing-is-prop {α} p q = funext fact₂
 where
  open import FunExt
  fact₀ : (i : ) (f g : α(succ i)    α i  )  f  g
  fact₀ i f g = funext fact₁
   where
    fact₁ : (r : α (succ i)  )  f r  g r
    fact₁ r = 𝟚-is-set (f r) (g r)
  fact₂ : (i : )  p i  q i
  fact₂ i = fact₀ i (p i) (q i) 

incl : ℕ∞  (   𝟚)
incl = pr₁

incl-mono : left-cancellable incl
incl-mono = pr₁-mono decreasing-is-prop

Cantor-separated : separated (  𝟚)
Cantor-separated = separated-ideal _  𝟚-separated)

ℕ∞-separated : separated ℕ∞
ℕ∞-separated = subtype-of-separated-is-separated pr₁ incl-mono Cantor-separated

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

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

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 : ℕ∞  U
isZero u = positivity u  

positive : ℕ∞  U
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(ap positivity r)

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

Succ-∞-is-∞ : Succ   
Succ-∞-is-∞ = incl-mono(funext lemma) 
 where
   open import FunExt
   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
  open import FunExt
  fact : (i : )  incl u i  incl(Succ u) i 
  fact i = ap  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 = ap Pred

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

_≣_ : ℕ∞    U
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 = ap 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((r₀ ⁻¹ ) r₁))
 (ℕ∞-hset (transport  n  x  under n) (under-mono {x₀} ((r₀ ⁻¹)  r₁)) r₀) r₁) 

under-mono-refl : (k : )  under-mono refl  (refl {_} {} {k})
under-mono-refl 0 = refl
under-mono-refl (succ k) = ap (ap 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
  open import FunExt
  lemma : (i : )  incl u i  incl Zero i
  lemma 0 = base
  lemma (succ i) = Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] (pr₂ 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
  open import FunExt
  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≢₁](ap 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
  open import FunExt
  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≡₀] (pr₂ 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 (pr₂ 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 (ap  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
  open import FunExt
  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(ap p s) (f n))(Lemma[b≡₀→b≢₁] g)

  claim-∞ : p u    u  
  claim-∞ = (contra-positive  s  trans(ap 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 = inl(isZero-equal-Zero r)
  lemma₁ : positive u  u  Zero + u  Zero
  lemma₁ r = inr(contra-positive fact (Lemma[b≡₁→b≢₀] r))
    where fact : u  Zero  isZero u
          fact r = ap  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 = inr(contra-positive lemma (Lemma[b≡₀→b≢₁] r))
   where
    lemma : u  under(succ n)  incl u n  
    lemma r = trans (ap  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 = inl(Succ-criterion r s)
    lemma₁₁ :  incl u (succ n)    u  under(succ n) + u  under(succ n) 
    lemma₁₁ s = inr (contra-positive lemma (Lemma[b≡₁→b≢₀] s))
     where
      lemma : u  under(succ n)  incl u (succ n)  
      lemma r = trans (ap  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 (inl p) = inl (r i p)
     f (inr p) = inr (s i p)

\end{code}

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

\begin{code}

_⊏_ :   ℕ∞  U
n  u = incl u n  

infix  30 _⊏_

_≺_ : bin-rel ℕ∞
u  v = Σ (\(n : )  u  under n × n  v)

{-

≺-OK-founded : (p : ℕ∞ → 𝟚) → ((v : ℕ∞) → ((u : ℕ∞) → u ≺ v → p u ≡ ₁) → p v ≡ ₁) → (v : ℕ∞) → p v ≡ ₁
≺-OK-founded p φ = ℕ∞-density a b
 where
  a : (n : ℕ) → p(under n) ≡ ₁
  a zero = φ (under zero) f
   where
    f : (u : ℕ∞) → u ≺ under zero → p u ≡ ₁
    f u (_ , _ , ())
  a (succ n) = {!!}

  b : p ∞ ≡ ₁
  b = {!!}

-}
\end{code}