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

(Added December 2017. What we knew for a long time: The ℕ∞ is a
retract of the Cantor type ℕ → 𝟚. This required adding a number of
lemmas.)

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module GenericConvergentSequence where

open import SpartanMLTT
open import Two
open import NaturalsAddition renaming (_+_ to _∔_)
open import NaturalsOrder
open import DiscreteAndSeparated
open import UF-Base
open import UF-Subsingletons
open import UF-Subsingletons-FunExt
open import UF-FunExt
open import UF-Embedding
open import UF-Equiv
open import UF-Retracts
open import UF-Miscelanea

funext₀ : U₁ ̇
funext₀ = funext U₀ U₀

\end{code}

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

\begin{code}

decreasing : (  𝟚)  U₀ ̇
decreasing α = (i : )  α(succ i) ≤₂ α i

decreasing-is-prop : funext₀  (α :   𝟚)  is-prop(decreasing α)
decreasing-is-prop fe α = Π-is-prop fe
                             i  Π-is-prop fe  p  𝟚-is-set))

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

decreasing-is-prop-old : funext₀  {α :   𝟚}  is-prop(decreasing α)
decreasing-is-prop-old fe {α} p q = dfunext fe fact₂
 where
  fact₀ : (i : ) (f g : α(succ i)    α i  )  f  g
  fact₀ i f g = nfunext fe 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-lc : funext₀  left-cancellable incl
incl-lc fe = pr₁-lc (decreasing-is-prop fe _)

force-decreasing : (  𝟚)  (  𝟚)
force-decreasing β 0 = β 0
force-decreasing β (succ i) = min𝟚 (β(succ i)) (force-decreasing β i)

force-decreasing-is-decreasing : (β :   𝟚)  decreasing(force-decreasing β)
force-decreasing-is-decreasing β zero     = Lemma[min𝟚ab≡₁→b≡₁] {β 1} {β zero}
force-decreasing-is-decreasing β (succ i) = Lemma[minab≤₂b] {β (succ (succ i))}
                                                             {force-decreasing β (succ i)}

force-decreasing-unchanged : (α :   𝟚)  decreasing α  force-decreasing α  α
force-decreasing-unchanged α d zero     = refl
force-decreasing-unchanged α d (succ i) = g
  where
    IH : force-decreasing α i  α i
    IH = force-decreasing-unchanged α d i
    p : α (succ i) ≤₂ α i
    p = d i
    h : min𝟚 (α (succ i)) (α i)  α (succ i)
    h = Lemma[a≤₂b→min𝟚ab≡a] p
    g' : min𝟚 (α (succ i)) (force-decreasing α i)  α (succ i)
    g' = transport  b  min𝟚 (α (succ i)) b  α (succ i)) (IH ⁻¹) h
    g : force-decreasing α (succ i)  α (succ i)
    g = g'

lcni : (   𝟚)  ℕ∞
lcni β = force-decreasing β , force-decreasing-is-decreasing β

lcni-incl : funext₀  (x : ℕ∞)  lcni(incl x)  x
lcni-incl fe (α , d) = to-Σ-≡ (dfunext fe (force-decreasing-unchanged α d) ,
                                  decreasing-is-prop fe α _ _)

ℕ∞-retract-of-Cantor : funext₀  retract ℕ∞ of (  𝟚)
ℕ∞-retract-of-Cantor fe = lcni , incl , lcni-incl fe

force-decreasing-is-smaller : (β :   𝟚) (i : )  force-decreasing β i ≤₂ β i
force-decreasing-is-smaller β zero     p = p
force-decreasing-is-smaller β (succ i) p = Lemma[min𝟚ab≡₁→a≡₁] p

force-decreasing-is-not-much-smaller : (β :   𝟚) (n : )
                                      force-decreasing β n  
                                      Σ \(m : )  β m  
force-decreasing-is-not-much-smaller β zero  p    = zero , p
force-decreasing-is-not-much-smaller β (succ n) p = f c
  where
    A = Σ \(m : )  β m  
    c : (β (succ n)  ) + (force-decreasing β n  )
    c = lemma[min𝟚ab≡₀] {β (succ n)} {force-decreasing β n} p
    f : (β (succ n)  ) + (force-decreasing β n  )  A
    f (inl q) = succ n , q
    f (inr r) = force-decreasing-is-not-much-smaller β n r

Cantor-separated : funext₀  separated (  𝟚)
Cantor-separated fe = Π-separated fe  _  𝟚-is-separated)

ℕ∞-separated : funext₀  separated ℕ∞
ℕ∞-separated fe = subtype-of-separated-is-separated pr₁ (incl-lc fe) (Cantor-separated fe)

ℕ∞-is-set : funext₀  is-set ℕ∞
ℕ∞-is-set fe = separated-is-set fe (ℕ∞-separated fe)

open import TotallySeparated

ℕ∞-totally-separated : funext₀  totally-separated ℕ∞
ℕ∞-totally-separated fe {x} {y} α = g
 where
  p :   (ℕ∞  𝟚)
  p i x = incl x i
  l : incl x  incl y
  l = dfunext fe  i  α (p i))
  g : x  y
  g = incl-lc fe l

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

Succ : ℕ∞  ℕ∞
Succ (α , d) = (α' , d')
 where
  α' :   𝟚
  α' 0 = 
  α'(succ n) = α n
  d' : decreasing α'
  d' 0 = λ r  refl
  d' (succ i) = d i

_⊑_ : ℕ∞    U₀ ̇
u  n = incl u n  

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

not-⊏-is-⊒ : {m : } {u : ℕ∞}  ¬(m  u)  u  m
not-⊏-is-⊒ f = Lemma[b≢₁→b≡₀] f

not-⊑-is-⊐ : {m : } {u : ℕ∞}  ¬(u  m)  m  u
not-⊑-is-⊐ f = Lemma[b≢₀→b≡₁] f

is-Zero : ℕ∞  U₀ ̇
is-Zero u = u  0

positive : ℕ∞  U₀ ̇
positive u = 0  u

positivity : ℕ∞  𝟚
positivity u = incl u 0

is-Zero-Zero : is-Zero Zero
is-Zero-Zero = refl

Zero-not-Succ : {u : ℕ∞}  Zero  Succ u
Zero-not-Succ {u} r = zero-is-not-one(ap positivity r)

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

Succ-∞-is-∞ : funext₀  Succ   
Succ-∞-is-∞ fe = incl-lc fe (dfunext fe lemma)
 where
   lemma : (i : )  incl(Succ ) i  incl  i
   lemma 0 = refl
   lemma (succ i) = refl

unique-fixed-point-of-Succ : funext₀  (u : ℕ∞)  u  Succ u  u  
unique-fixed-point-of-Succ fe u r = incl-lc fe claim
 where
  fact : (i : )  incl u i  incl(Succ u) i
  fact i = ap  -  incl - i) r
  lemma : (i : )  incl u i  
  lemma 0 = fact 0
  lemma (succ i) = fact(succ i)  lemma i
  claim : incl u  incl 
  claim = (dfunext fe lemma)

Pred : ℕ∞  ℕ∞
Pred(α , d) = (α  succ , d  succ)

Pred-Zero-is-Zero : Pred Zero  Zero
Pred-Zero-is-Zero = refl

Pred-Succ : {u : ℕ∞}  Pred(Succ u)  u
Pred-Succ {u} = refl

Pred-∞-is-∞ : Pred   
Pred-∞-is-∞ = refl

Succ-lc : left-cancellable Succ
Succ-lc = ap Pred

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

_≣_ : ℕ∞    U₀ ̇
u  n = u  under n

under-lc : left-cancellable under
under-lc {0} {0} r = refl
under-lc {0} {succ n} r = 𝟘-elim(Zero-not-Succ r)
under-lc {succ m} {0} r = 𝟘-elim(Zero-not-Succ (r ⁻¹))
under-lc {succ m} {succ n} r = ap succ (under-lc {m} {n} (Succ-lc r))

under-embedding : funext₀  is-embedding under
under-embedding fe = lc-embedding under under-lc (ℕ∞-is-set fe)

under-lc-refl : (k : )  under-lc refl  refl {_} {} {k}
under-lc-refl 0 = refl
under-lc-refl (succ k) = ap (ap succ) (under-lc-refl k)

under-diagonal₀ : (n : )  under n  n
under-diagonal₀ 0 = refl
under-diagonal₀ (succ n) = under-diagonal₀ n

under-diagonal₁ : (n : )  n  under(succ n)
under-diagonal₁ 0 = refl
under-diagonal₁ (succ n) = under-diagonal₁ n

is-Zero-equal-Zero : funext₀  {u : ℕ∞}  is-Zero u  u  Zero
is-Zero-equal-Zero fe {u} base = incl-lc fe (dfunext fe lemma)
 where
  lemma : (i : )  incl u i  incl Zero i
  lemma 0 = base
  lemma (succ i) = Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] (pr₂ u i) (lemma i)

same-positivity : funext₀  (u v : ℕ∞)
                (u  Zero  v  Zero)
                (v  Zero  u  Zero)
                positivity u  positivity v
same-positivity fe₀ u v f g = ≤₂-anti (≤₂'-coarser-than-≤₂ a)
                                      (≤₂'-coarser-than-≤₂ b)
 where
  a : is-Zero v  is-Zero u
  a p = back-transport is-Zero (g (is-Zero-equal-Zero fe₀ p)) refl
  b : is-Zero u  is-Zero v
  b p = back-transport is-Zero (f (is-Zero-equal-Zero fe₀ p)) refl

successors-same-positivity : {u u' v v' : ℕ∞}
                            u  Succ u'
                            v  Succ v'
                            positivity u  positivity v
successors-same-positivity refl refl = refl

not-Zero-is-Succ : funext₀  {u : ℕ∞}  u  Zero  u  Succ(Pred u)
not-Zero-is-Succ fe {u} f = incl-lc fe (dfunext fe lemma)
 where
  lemma : (i : )  incl u i  incl(Succ(Pred u)) i
  lemma 0 = Lemma[b≢₀→b≡₁] (f  is-Zero-equal-Zero fe)
  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 : funext₀  {u : ℕ∞}  positive u  u  Succ(Pred u)
positive-equal-Succ fe r = not-Zero-is-Succ fe (positive-is-not-Zero r)

Zero-or-Succ : funext₀  (u : ℕ∞)  (u  Zero) + (u  Succ(Pred u))
Zero-or-Succ fe₀ u = 𝟚-equality-cases
                       (z : is-Zero u)  inl (is-Zero-equal-Zero fe₀ z))
                       (p : positive u)  inr (positive-equal-Succ fe₀ p))

is-Succ : ℕ∞  U₀ ̇
is-Succ u = Σ \(w : ℕ∞)  u  Succ w

Zero+Succ : funext₀  (u : ℕ∞)  (u  Zero) + is-Succ u
Zero+Succ fe₀ u = Cases (Zero-or-Succ fe₀ u) inl  p  inr (Pred u , p))

Succ-criterion : funext₀  {u : ℕ∞} {n : }  n  u  u  succ n  u  Succ(under n)
Succ-criterion fe {u} {n} r s = incl-lc fe claim
 where
  lemma : (u : ℕ∞) (n : )  n  u  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 : )  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 : )  n  u  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
  claim : incl u  incl (Succ (under n))
  claim = dfunext fe (lemma u n r s)

∞-is-not-ℕ : (n : )    under n
∞-is-not-ℕ n s = zero-is-not-one ((ap  -  incl - n) s  under-diagonal₀ n)⁻¹)

not-ℕ-is-∞ : funext₀  {u : ℕ∞}  ((n : )  u  under n)  u  
not-ℕ-is-∞ fe {u} f = incl-lc fe (dfunext fe lemma)
 where
  lemma : (n : )  n  u
  lemma 0 = Lemma[b≢₀→b≡₁] r  f 0 (is-Zero-equal-Zero fe r))
  lemma (succ n) = Lemma[b≢₀→b≡₁] r  f(succ n)(Succ-criterion fe (lemma n) r))

ℕ∞-ddensity : funext₀   {U} {Y : ℕ∞  U ̇}
             ({u : ℕ∞}  separated (Y u))
             {f g : Π Y}
             ((n : )  f(under n)  g(under n))
             f   g 
             (u : ℕ∞)  f u  g u
ℕ∞-ddensity fe {U} {Y} s {f} {g} h h∞ u = s (f u) (g u) c
 where
  a : f u  g u  (n : )  u  under n
  a t n = contrapositive  (r : u  under n)  back-transport  -  f -  g -) r (h n)) t
  b : f u  g u  u  
  b = contrapositive  (r : u  )  back-transport  -  f -  g -) r h∞)
  c : ¬¬(f u  g u)
  c = λ t  b t (not-ℕ-is-∞ fe (a t))

ℕ∞-density : funext₀
               {U} {Y : U ̇}
              separated Y
              {f g : ℕ∞  Y}
              ((n : )  f(under n)  g(under n))
              f   g 
              (u : ℕ∞)  f u  g u
ℕ∞-density fe s = ℕ∞-ddensity fe  {_}  s)

ℕ∞-𝟚-density : funext₀
              {p : ℕ∞  𝟚}
              ((n : )  p(under n)  )
              p   
              (u : ℕ∞)  p u  
ℕ∞-𝟚-density fe = ℕ∞-density fe 𝟚-is-separated

under𝟙 :  + 𝟙  ℕ∞
under𝟙 = cases {U₀} {U₀} under  _  )

under𝟙-embedding : funext₀  is-embedding under𝟙
under𝟙-embedding fe = disjoint-cases-embedding under  _  ) (under-embedding fe) g d
 where
  g : is-embedding  _  )
  g x (* , p) (* , q) = ap  -  * , -) (ℕ∞-is-set fe p q)
  d : (n : ) (y : 𝟙)  under n  
  d n _ p = ∞-is-not-ℕ n (p ⁻¹)

under𝟙-dense : funext₀  is-dense under𝟙
under𝟙-dense fe (u , f) = g (not-ℕ-is-∞ fe h)
 where
  g : ¬(u  )
  g p = f ((inr *) , (p ⁻¹))
  h : (n : )  ¬(u  under n)
  h n p = f (inl n , (p ⁻¹))

\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 if n ⊏ u ⊑ n+1.

\begin{code}

finite-isolated : funext₀  (n : )  isolated (under n)
finite-isolated fe n u = decidable-eq-sym u (under n) (f u n)
 where
  f : (u : ℕ∞) (n : )  decidable (u  under n)
  f u 0 = 𝟚-equality-cases g₀ g₁
   where
    g₀ : is-Zero u  decidable (u  Zero)
    g₀ r = inl(is-Zero-equal-Zero fe r)
    g₁ : positive u  decidable (u  Zero)
    g₁ r = inr(contrapositive h (Lemma[b≡₁→b≢₀] r))
     where
      h : u  Zero  is-Zero u
      h r = ap  -  incl - 0) r
  f u (succ n) = 𝟚-equality-cases g₀ g₁
   where
    g₀ :  u  n  decidable (u  under(succ n))
    g₀ r = inr(contrapositive g (Lemma[b≡₀→b≢₁] r))
     where
      g : u  under(succ n)  n  u
      g r = ap  -  incl - n) r  under-diagonal₁ n
    g₁ :  n  u  decidable (u  under(succ n))
    g₁ r = 𝟚-equality-cases g₁₀ g₁₁
     where
      g₁₀ : u  succ n  decidable (u  under(succ n))
      g₁₀ s = inl(Succ-criterion fe r s)
      g₁₁ : succ n  u  decidable (u  under(succ n))
      g₁₁ s = inr (contrapositive g (Lemma[b≡₁→b≢₀] s))
       where
        g : u  under(succ n)  u  succ n
        g r = ap  -  incl - (succ n)) r  under-diagonal₀(succ n)

is-finite : ℕ∞  U₀ ̇
is-finite u = Σ \(n : )  under n  u

size : {u : ℕ∞}  is-finite u  
size (n , r) = n

is-finite-is-prop : funext₀  (u : ℕ∞)  is-prop (is-finite u)
is-finite-is-prop = under-embedding

under-is-finite : (n : )  is-finite(under n)
under-is-finite n = (n , refl)

Zero-is-finite : is-finite Zero
Zero-is-finite = under-is-finite zero

Zero-is-finite' : funext₀  (u : ℕ∞)  is-Zero u  is-finite u
Zero-is-finite' fe u z = back-transport is-finite (is-Zero-equal-Zero fe z) Zero-is-finite

is-finite-down : (u : ℕ∞)  is-finite (Succ u)  is-finite u
is-finite-down u (zero , r) = 𝟘-elim (Zero-not-Succ r)
is-finite-down u (succ n , r) = n , Succ-lc r

is-finite-up : (u : ℕ∞)  is-finite u  is-finite (Succ u)
is-finite-up u (n , r) = (succ n , ap Succ r)

is-finite-up' : funext₀  (u : ℕ∞)  is-finite (Pred u)  is-finite u
is-finite-up' fe u i = 𝟚-equality-cases
                          (z : is-Zero u)
                             Zero-is-finite' fe u z)
                          (p : positive u)
                             back-transport
                               is-finite
                               (positive-equal-Succ fe p)
                               (is-finite-up (Pred u) i))

is-infinite-∞ : ¬(is-finite )
is-infinite-∞ (n , r) = 𝟘-elim (∞-is-not-ℕ n (r ⁻¹))

\end{code}

Order on ℕ∞:

\begin{code}

_≼_ : ℕ∞  ℕ∞  U₀ ̇
u  v = (n : )  n  u  n  v

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

Zero-minimal : (u : ℕ∞)  Zero  u
Zero-minimal u n ()

Succ-not-≼-Zero : (u : ℕ∞)  ¬(Succ u  Zero)
Succ-not-≼-Zero u l = zero-is-not-one (l zero refl)

Succ-monotone : (u v : ℕ∞)  u  v  Succ u  Succ v
Succ-monotone u v l zero p = p
Succ-monotone u v l (succ n) p = l n p

Succ-loc : (u v : ℕ∞)  Succ u  Succ v  u  v
Succ-loc u v l n = l (succ n)

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}

∞-⊏-maximal : (n : )  n  
∞-⊏-maximal n = refl

_≺_ : ℕ∞  ℕ∞  U₀ ̇
u  v = Σ \(n : )  (u  under n) × n  v

∞-top : (u : ℕ∞)  ¬(  u)
∞-top u (n , r , l) = ∞-is-not-ℕ n r

below-isolated : funext₀  (u v : ℕ∞)  u  v  isolated u
below-isolated fe u v (n , r , l) = back-transport isolated r (finite-isolated fe n)

≺-prop-valued : funext₀  (u v : ℕ∞)  is-prop (u  v)
≺-prop-valued fe u v (n , r , a) (m , s , b) =
  to-Σ-≡ (under-lc (r ⁻¹  s) , to-Σ-≡ (ℕ∞-is-set fe _ _ , 𝟚-is-set _ _))

⊏-coarser-than-≺ : (n : ) (u : ℕ∞)  n  u  under n  u
⊏-coarser-than-≺ n u a = n , refl , a

≺-coarser-than-⊏ : (n : ) (u : ℕ∞)  under n  u  n  u
≺-coarser-than-⊏ n u (m , r , a) = back-transport  k  k  u) (under-lc r) a

∞-≺-maximal : (n : )  under n  
∞-≺-maximal n = n , refl , ∞-⊏-maximal n

open import NaturalsOrder

<-coarser-than-⊏ : (m n : )  m < n   m  under n
<-coarser-than-⊏ zero zero ()
<-coarser-than-⊏ zero (succ n) l = refl
<-coarser-than-⊏ (succ m) zero ()
<-coarser-than-⊏ (succ m) (succ n) l = <-coarser-than-⊏ m n l

⊏-coarser-than-< : (m n : )   m  under n  m < n
⊏-coarser-than-< zero zero ()
⊏-coarser-than-< zero (succ n) l = zero-minimal n
⊏-coarser-than-< (succ m) zero ()
⊏-coarser-than-< (succ m) (succ n) l = ⊏-coarser-than-< m n l

⊏-back : (u : ℕ∞) (n : )  succ n  u  n  u
⊏-back = pr₂

⊏-trans'' : (u : ℕ∞) (n : )  (m : )  m  n  n  u  m  u
⊏-trans'' u = regress  n  n  u) (⊏-back u)

⊏-trans' : (m : ) (n : ) (u : ℕ∞)   m < n  n  u  m  u
⊏-trans' m n u l = ⊏-trans'' u n m (≤-trans m (succ m) n (≤-succ m) l)

⊏-trans : (m n : ) (u : ℕ∞)  m  under n  n  u  m  u
⊏-trans m n u a = ⊏-trans' m n u (⊏-coarser-than-< m n a)

open import OrdinalNotions hiding (_≤_) hiding (≤-refl) hiding (_≼_)

≺-trans : is-transitive _≺_
≺-trans u v w (m , r , a) (n , s , b) = m , r , ⊏-trans m n w (transport  t  m  t) s a) b

finite-accessible : (n : )  is-accessible _≺_ (under n)
finite-accessible = course-of-values-induction  n  is-accessible _≺_ (under n)) φ
 where
  φ : (n : )  ((m : )  m < n  is-accessible _≺_ (under m))  is-accessible _≺_ (under n)
  φ n σ = next (under n) τ
   where
    τ : (u : ℕ∞)  u  under n  is-accessible _≺_ u
    τ u (m , r , l) = back-transport (is-accessible _≺_) r (σ m (⊏-coarser-than-< m n l))

≺-well-founded : is-well-founded _≺_
≺-well-founded v = next v σ
 where
  σ : (u : ℕ∞)  u  v  is-accessible _≺_ u
  σ u (n , r , l) = back-transport (is-accessible _≺_) r (finite-accessible n)

≺-extensional : funext₀  is-extensional _≺_
≺-extensional fe u v l m = γ
 where
  f : (i : )  i  u  i  v
  f i a = ≺-coarser-than-⊏ i v (l (under i) (⊏-coarser-than-≺ i u a))
  g : (i : )  i  v  i  u
  g i a = ≺-coarser-than-⊏ i u (m (under i) (⊏-coarser-than-≺ i v a))
  h : (i : )  incl u i  incl v i
  h i = ≤₂-anti (f i) (g i)
  γ : u  v
  γ = incl-lc fe (dfunext fe h)

ℕ∞-ordinal : funext₀  is-well-order _≺_
ℕ∞-ordinal fe = (≺-prop-valued fe) , ≺-well-founded , (≺-extensional fe) , ≺-trans

\end{code}

The following is not needed anymore, as we have the stronger fact,
proved above, that ≺ is well founded:

\begin{code}

≺-well-founded₂ : funext₀  is-well-founded₂ _≺_
≺-well-founded₂ fe p φ = ℕ∞-𝟚-density fe a b
 where
  γ : (n : )  ((m : )  m < n  p (under m)  )  p (under n)  
  γ n g = φ (under n) h
   where
    h : (u : ℕ∞)  u  under n  p u  
    h u (m , r , l) = back-transport  v  p v  ) r (g m (⊏-coarser-than-< m n l))
  a : (n : )  p(under n)  
  a = course-of-values-induction  n  p(under n)  ) γ
  f : (u : ℕ∞)  u    p u  
  f u (n , r , l) = back-transport  v  p v  ) r (a n)
  b : p   
  b = φ  f

ℕ∞-ordinal₂ : funext₀  is-well-order₂ _≺_
ℕ∞-ordinal₂ fe = ≺-prop-valued fe ,
                  ≺-well-founded₂ fe ,
                  ≺-extensional fe ,
                  ≺-trans

under-lemma : funext₀  (u : ℕ∞) (n : )  u  n  Σ \(m : )  (m  n) × (u  under m)
under-lemma fe u zero p     = zero , ≤-refl zero , is-Zero-equal-Zero fe p
under-lemma fe u (succ n) p = g (𝟚-discrete (incl u n) )
 where
  IH : u  n  Σ \(m : )  (m  n) × (u  under m)
  IH = under-lemma fe u n
  g :  decidable(u  n)  Σ \(m : )  (m  succ n) × (u  under m)
  g (inl q) = pr₁(IH q) , ≤-trans (pr₁(IH q)) n (succ n) (pr₁(pr₂(IH q))) (≤-succ n) , pr₂(pr₂(IH q))
  g (inr φ) = succ n , ≤-refl n , s
    where
      q : n  u
      q = Lemma[b≢₀→b≡₁] φ
      s : u  Succ (under n)
      s = Succ-criterion fe {u} {n} q p

≺-cotransitive : funext₀  cotransitive _≺_
≺-cotransitive fe u v w (n , r , a) = g (𝟚-discrete (incl w n) )
 where
  g : decidable(n  w)  (u  w) + (w  v)
  g (inl a) = inl (n , r , a)
  g (inr f) = inr (m , s , ⊏-trans'' v n m l a)
   where
    b : w  n
    b = not-⊏-is-⊒ {n} {w} f
    σ : Σ \(m : )  (m  n) × (w  under m)
    σ = under-lemma fe w n b
    m : 
    m = pr₁ σ
    l : m  n
    l = pr₁(pr₂ σ)
    s : w  under m
    s = pr₂(pr₂ σ)

ℕ∞-𝟚-order-separated : funext₀  𝟚-order-separated _≺_
ℕ∞-𝟚-order-separated fe x y (n , r , l) =  p , t , h
 where
  p : ℕ∞  𝟚
  p z = incl z n
  t : (p x  ) × (p y  )
  t = (back-transport  z  p z  ) r (under-diagonal₀ n) , l)
  f : (u v : ℕ∞)  u  v  p u ≤₂ p v
  f u v (n' , r' , l') s = ⊏-trans' n n' v b l'
   where
    a : p (under n')  
    a = transport  z  p z  ) r' s
    b : n < n'
    b = ⊏-coarser-than-< n n' a
  g : (u v : ℕ∞)  p u <₂ p v  u  v
  g u v (a , b) = pr₁ c , pr₂(pr₂ c) , (⊏-trans'' v n (pr₁ c) (pr₁(pr₂ c)) b)
   where
    c : Σ \(m : )  (m  n) × (u  under m)
    c = under-lemma fe u n a

  h : (u v : ℕ∞)  (u  v  p u ≤₂ p v) × (p u <₂ p v  u  v)
  h u v = f u v , g u v

under-order-preserving : (m n : )  m < n  under m  under n
under-order-preserving m n l = m , refl , <-coarser-than-⊏ m n l

under-order-reflecting : (m n : )  under m  under n  m < n
under-order-reflecting m n (m' , p , l') = ⊏-coarser-than-< m n l
 where
  l : m  under n
  l = back-transport  -  -  under n) (under-lc p) l'

{- TODO

<-coarser-than-≺ : (m n : ℕ) → under m ≺ under n → m < n
<-coarser-than-≺ = ?

⊏-coarser-than-≺ : (m : ℕ) (u : ℕ∞) → m ⊏ u → under m ≺ u
⊏-coarser-than-≺ = ?
-}

\end{code}

Added 25 June 2018. This may be placed somewhere else in the future.
Another version of N∞, to be investigated.

\begin{code}

Ν∞ : U₁ ̇
Ν∞ = Σ \(A :   Ω U₀)  (n : )  A (succ n) holds  A n holds

\end{code}

Needed 28 July 2018:

\begin{code}

≼-is-prop : funext₀  (u v : ℕ∞)  is-prop (u  v)
≼-is-prop fe u v = Π-is-prop fe  n  Π-is-prop fe  l  𝟚-is-set))

≼-not-≺ : (u v : ℕ∞)  u  v  ¬(v  u)
≼-not-≺ u v l (n , (p , m)) = zero-is-not-one (e ⁻¹  d)
 where
  a : v  u
  a = transport  -  -  u) (p ⁻¹) (⊏-coarser-than-≺ n u m)
  k : 
  k = pr₁ a
  b : v  under k
  b = pr₁ (pr₂ a)
  c : k  v
  c = l k (pr₂ (pr₂ a))
  d : incl (under k) k  
  d = transport  -  k  -) b c
  e : incl (under k) k  
  e = under-diagonal₀ k

not-≺-≼ : funext₀  (u v : ℕ∞)  ¬(v  u)  u  v
not-≺-≼ fe u v φ n l = 𝟚-equality-cases f g
 where
  f : v  n  n  v
  f m = 𝟘-elim (φ (k , (p , b)))
   where
    k : 
    k = pr₁(under-lemma fe v n m)
    a : k  n
    a = pr₁(pr₂(under-lemma fe v n m))
    p : v  under k
    p = pr₂(pr₂(under-lemma fe v n m))
    b : k  u
    b = ⊏-trans'' u n k a l
  g : n  v  n  v
  g = id

\end{code}

Characterization of ⊏.

\begin{code}

⊏-positive : (n : ) (u : ℕ∞)  n  u  positive u
⊏-positive n u = ⊏-trans'' u n 0 (zero-minimal n)

⊏-charac→ : funext₀  (n : ) (u : ℕ∞)
            n  u  Σ \(v : ℕ∞)  u  (Succ ^ (n  1)) v
⊏-charac→ fe₀ zero u l = Pred u , (positive-equal-Succ fe₀ l)
⊏-charac→ fe₀ (succ n) u l = γ
 where
  IH : Σ \(v : ℕ∞)  Pred u  (Succ ^ (n  1)) v
  IH = ⊏-charac→ fe₀ n (Pred u) l
  v : ℕ∞
  v = pr₁ IH
  p : u  (Succ ^ (n  2)) v
  p = u                   ≡⟨ positive-equal-Succ fe₀ (⊏-positive (succ n) u l) 
      Succ (Pred u)       ≡⟨ ap Succ (pr₂ IH) 
      (Succ ^ (n  2)) v  
  γ : Σ \(v : ℕ∞)  u  (Succ ^ (n  2)) v
  γ = v , p

⊏-charac← : funext₀  (n : ) (u : ℕ∞)
            (Σ \(v : ℕ∞)  u  (Succ ^ (n  1)) v)  n  u
⊏-charac← fe₀ zero u (v , refl) = refl
⊏-charac← fe₀ (succ n) u (v , refl) = γ
 where
  IH : n  Pred u
  IH = ⊏-charac← fe₀ n (Pred u) (v , refl)
  γ : succ n  u
  γ = IH

\end{code}

precedences:

\begin{code}

infix  30 _⊏_
infix  30 _≺_

\end{code}