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.