Martin Escardo, 14th January 2022.

An isomorphic copy of β„•βˆž defined in CoNaturals.GenericConvergentSequence.
The isomorphism is proved in CoNaturals.Equivalence.

\begin{code}

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

module CoNaturals.GenericConvergentSequence2 where

open import MLTT.Spartan
open import MLTT.Two-Properties
open import Notation.CanonicalMap
open import TypeTopology.Cantor
open import UF.DiscreteAndSeparated
open import UF.FunExt
open import UF.NotNotStablePropositions
open import UF.Sets
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

T-cantor : (β„• β†’ 𝟚) β†’ 𝓀₀ Μ‡
T-cantor Ξ± = Ξ£ n κž‰ β„• , Ξ± n ＝ ₁

private
 T = T-cantor

has-at-most-one-₁ : (β„• β†’ 𝟚) β†’ 𝓀₀ Μ‡
has-at-most-one-₁ Ξ± = is-prop (T Ξ±)

has-at-most-one-₁-is-prop : funextβ‚€ β†’ (Ξ± : β„• β†’ 𝟚) β†’ is-prop (has-at-most-one-₁ Ξ±)
has-at-most-one-₁-is-prop fe Ξ± = being-prop-is-prop fe

β„•βˆž' : 𝓀₀ Μ‡
β„•βˆž' = Ξ£ Ξ± κž‰ (β„• β†’ 𝟚) , has-at-most-one-₁ Ξ±

β„•βˆž'-to-β„•β†’πŸš : β„•βˆž' β†’ (β„• β†’ 𝟚)
β„•βˆž'-to-β„•β†’πŸš = pr₁

β„•βˆž'-to-β„•β†’πŸš-lc : funextβ‚€ β†’ left-cancellable β„•βˆž'-to-β„•β†’πŸš
β„•βˆž'-to-β„•β†’πŸš-lc fe = pr₁-lc (being-prop-is-prop fe)

β„•βˆž'-is-¬¬-separated : funextβ‚€ β†’ is-¬¬-separated β„•βˆž'
β„•βˆž'-is-¬¬-separated fe = subtype-is-¬¬-separated
                         pr₁
                         (β„•βˆž'-to-β„•β†’πŸš-lc fe)
                         (Cantor-is-¬¬-separated fe)

β„•βˆž'-is-set : funextβ‚€ β†’ is-set β„•βˆž'
β„•βˆž'-is-set fe = ¬¬-separated-types-are-sets fe (β„•βˆž'-is-¬¬-separated fe)

private
 Β¬T : (β„• β†’ 𝟚) β†’ 𝓀₀ Μ‡
 Β¬T Ξ± = (n : β„•) β†’ Ξ± n ＝ β‚€

not-T-gives-Β¬T : {Ξ± : β„• β†’ 𝟚} β†’ Β¬ (T Ξ±) β†’ Β¬T Ξ±
not-T-gives-Β¬T {Ξ±} Ο• n = different-from-₁-equal-β‚€ (Ξ» (e : Ξ± n ＝ ₁) β†’ Ο• (n , e))

Β¬T-gives-not-T : {Ξ± : β„• β†’ 𝟚} β†’ Β¬T Ξ± β†’ Β¬ (T Ξ±)
Β¬T-gives-not-T {Ξ±} ψ (n , e) = zero-is-not-one ((ψ n)⁻¹ βˆ™ e)

to-T-＝ : {Ξ± : β„• β†’ 𝟚}
          {n n' : β„•}
        β†’ n ＝ n'
        β†’ {e : Ξ± n ＝ ₁} {e' : Ξ± n' ＝ ₁}
        β†’ (n , e) ＝[ T Ξ± ] (n' , e')
to-T-＝ p = to-subtype-＝ (Ξ» - β†’ 𝟚-is-set) p

from-T-＝ : {Ξ± : β„• β†’ 𝟚}
          {n n' : β„•}
        β†’ {e : Ξ± n ＝ ₁} {e' : Ξ± n' ＝ ₁}
        β†’ (n , e) ＝[ T Ξ± ] (n' , e')
        β†’ n ＝ n'
from-T-＝ p = ap pr₁ p

index-uniqueness : (Ξ± : β„• β†’ 𝟚)
                 β†’ is-prop (T Ξ±)
                 β†’ {n n' : β„•} β†’ Ξ± n ＝ ₁ β†’ Ξ± n' ＝ ₁ β†’ n ＝ n'
index-uniqueness α i {n} {n'} e e' = from-T-＝ (i (n , e) (n' , e'))

index-uniqueness-converse : (Ξ± : β„• β†’ 𝟚)
                          β†’ ({n n' : β„•} β†’ Ξ± n ＝ ₁ β†’ Ξ± n' ＝ ₁ β†’ n ＝ n')
                          β†’ is-prop (T Ξ±)
index-uniqueness-converse Ξ± Ο• (n , e) (n' , e') = to-T-＝ (Ο• e e')

private
 instance
  canonical-map-β„•βˆž'-β„•β†’πŸš : Canonical-Map β„•βˆž' (β„• β†’ 𝟚)
  ΞΉ {{canonical-map-β„•βˆž'-β„•β†’πŸš}} = β„•βˆž'-to-β„•β†’πŸš

β„•βˆž'-to-β„•β†’πŸš-at-most-one-₁ : (u : β„•βˆž') β†’ is-prop (T (β„•βˆž'-to-β„•β†’πŸš u))
β„•βˆž'-to-β„•β†’πŸš-at-most-one-₁ = prβ‚‚

β„•βˆž'-index-uniqueness : (u : β„•βˆž')
                     β†’ {n n' : β„•} β†’ ΞΉ u n ＝ ₁ β†’ ΞΉ u n' ＝ ₁ β†’ n ＝ n'
β„•βˆž'-index-uniqueness (Ξ± , i) = index-uniqueness Ξ± i

Zero' : β„•βˆž'
Zero' = Ξ± , h
 where
  Ξ± : β„• β†’ 𝟚
  Ξ± 0        = ₁
  Ξ± (succ n) = β‚€

  i : is-prop (T Ξ±)
  i (0 , e) (0 , e') = to-T-＝ refl

  h : has-at-most-one-₁ Ξ±
  h (n , e) (n' , e') = to-T-＝ (index-uniqueness α i e e')

Succ' : β„•βˆž' β†’ β„•βˆž'
Succ' (Ξ± , h) = cons β‚€ Ξ± , h'
 where
  h' : has-at-most-one-₁ (cons β‚€ Ξ±)
  h' (succ n , e) (succ n' , e') = to-T-＝ (ap succ (index-uniqueness α h e e'))

β„•-to-β„•βˆž' : β„• β†’ β„•βˆž'
β„•-to-β„•βˆž' 0        = Zero'
β„•-to-β„•βˆž' (succ n) = Succ' (β„•-to-β„•βˆž' n)

private
 instance
  Canonical-Map-β„•-β„•βˆž' : Canonical-Map β„• β„•βˆž'
  ΞΉ {{Canonical-Map-β„•-β„•βˆž'}} = β„•-to-β„•βˆž'

is-finite' : β„•βˆž' β†’ 𝓀₀ Μ‡
is-finite' u@(Ξ± , a) = T Ξ±

being-finite'-is-prop : funextβ‚€ β†’ (u : β„•βˆž') β†’ is-prop (is-finite' u)
being-finite'-is-prop feβ‚€ u@(Ξ± , a) = a

size' : {u : β„•βˆž'} β†’ is-finite' u β†’ β„•
size' (n , e) = n

size'-property : {u : β„•βˆž'} (Ο† : is-finite' u) β†’ β„•βˆž'-to-β„•β†’πŸš u (size' {u} Ο†) ＝ ₁
size'-property (n , e) = e

Zero'-is-finite : is-finite' Zero'
Zero'-is-finite = 0 , refl

is-finite'-up : (u : β„•βˆž')
              β†’ is-finite' u
              β†’ is-finite' (Succ' u)
is-finite'-up _ (n , e) = succ n , e

is-finite'-down : (u : β„•βˆž')
                β†’ is-finite' (Succ' u)
                β†’ is-finite' u
is-finite'-down _ (succ n , e) = n , e

β„•-to-β„•βˆž'-is-finite' : (n : β„•) β†’ is-finite' (ΞΉ n)
β„•-to-β„•βˆž'-is-finite' 0        = Zero'-is-finite
β„•-to-β„•βˆž'-is-finite' (succ n) = is-finite'-up (ΞΉ n)
                                (β„•-to-β„•βˆž'-is-finite' n)

∞' : β„•βˆž'
∞' = (Ξ» _ β†’ β‚€) , (Ξ» (n , e) (n' , e') β†’ 𝟘-elim (zero-is-not-one e))

not-finite'-is-∞' : funextβ‚€ β†’ (u : β„•βˆž') β†’ Β¬ is-finite' u β†’ u ＝ ∞'
not-finite'-is-∞' fe u Ξ½ = β„•βˆž'-to-β„•β†’πŸš-lc fe
                            (dfunext fe
                              (Ξ» i β†’ different-from-₁-equal-β‚€
                                      (Ξ» (e : β„•βˆž'-to-β„•β†’πŸš u i ＝ ₁) β†’ Ξ½ (i , e))))

not-T-is-∞' : funextβ‚€ β†’ (u : β„•βˆž') β†’ Β¬ T (ΞΉ u) β†’ u ＝ ∞'
not-T-is-∞' fe u Ξ½ = β„•βˆž'-to-β„•β†’πŸš-lc fe (dfunext fe (not-T-gives-Β¬T Ξ½))

is-infinite-∞' : ¬ is-finite' ∞'
is-infinite-∞' (n , e) = zero-is-not-one e

\end{code}