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
open import Two
open import Cantor
open import SetsAndFunctions
open import FirstProjectionInjective
open import Injection

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

incl : ℕ∞ → ₂ℕ
incl = π₀

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