Martin Escardo, November 2023.

We show that the two types ℕ∞ and ℕ∞' of conatural numbers are
equivalent.

For that purpose, we develop an automorphism of the Cantor type ℕ → 𝟚
that restricts restricts to an equivalence between ℕ∞ and the subtype

ℕ∞ := Σ α ꞉ (ℕ → 𝟚) , is-prop (Σ n ꞉ ℕ , α n ＝ ₁)

of the Cantor type (of binary sequences with at most one ₁).

Notice that the condition on α can be expressed as "is-prop (fiber α ₁)".

\begin{code}

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

module CoNaturals.Equivalence where

open import CoNaturals.GenericConvergentSequence
open import CoNaturals.GenericConvergentSequence2
open import MLTT.Spartan
open import MLTT.Two-Properties
open import Naturals.Order
open import Naturals.Properties
open import Notation.CanonicalMap
open import Notation.Order
open import TypeTopology.Cantor
open import UF.Equiv
open import UF.FunExt
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

private
T = T-cantor

private
instance
Canonical-Map-ℕ-ℕ∞' : Canonical-Map ℕ ℕ∞'
ι {{Canonical-Map-ℕ-ℕ∞'}} = ℕ-to-ℕ∞'

\end{code}

To show that ℕ∞' gives an equivalent copy of ℕ∞, we consider a
particular equivalence (ℕ → 𝟚) ≃ (ℕ → 𝟚).

\begin{code}

ϕ-cantor γ-cantor : (ℕ → 𝟚) → (ℕ → 𝟚)

ϕ-cantor α n = cons ₁ α n ⊕ α n

γ-cantor β 0        = complement (β 0)
γ-cantor β (succ n) = γ-cantor β n ⊕ β (succ n)

private
ϕ γ : (ℕ → 𝟚) → (ℕ → 𝟚)
ϕ = ϕ-cantor
γ = γ-cantor

η-cantor : (β : ℕ → 𝟚) → ϕ (γ β) ∼ β
η-cantor β 0        = complement-involutive (β 0)
η-cantor β (succ n) = ⊕-involutive {γ β n} {β (succ n)}

ε-cantor : (α : ℕ → 𝟚) → γ (ϕ α) ∼ α
ε-cantor α 0        = complement-involutive (α 0)
ε-cantor α (succ n) = γ (ϕ α) (succ n)             ＝⟨ refl ⟩
γ (ϕ α) n ⊕ α n ⊕ α (succ n) ＝⟨ I ⟩
α n ⊕ α n ⊕ α (succ n)       ＝⟨ II ⟩
α (succ n)                   ∎
where
I  = ap (_⊕ α n ⊕ α (succ n)) (ε-cantor α n)
II = ⊕-involutive {α n} {α (succ n)}

private
η : (β : ℕ → 𝟚) → ϕ (γ β) ∼ β
ε : (α : ℕ → 𝟚) → γ (ϕ α) ∼ α

η = η-cantor
ε = ε-cantor

\end{code}

We now discuss the restrictions of ϕ and γ mentioned above. Notice
that the following is by four cases without induction.

\begin{code}

ϕ-property : funext₀
→ (α : ℕ → 𝟚)
→ is-decreasing α
→ has-at-most-one-₁ (ϕ α)
ϕ-property fe α δ (0 , p) (0 ,      q) = to-T-＝ refl
ϕ-property fe α δ (0 , p) (succ m , q) = 𝟘-elim (Zero-not-Succ (II ⁻¹ ∙ IV))
where
u : ℕ∞
u = (α , δ)

I = α 0                           ＝⟨ (complement-involutive (α 0))⁻¹ ⟩
complement (complement (α 0)) ＝⟨ ap complement p ⟩
complement ₁                  ＝⟨ refl ⟩
₀                             ∎

II : u ＝ Zero
II = is-Zero-equal-Zero fe I

III : (α m ＝ ₁) × (α (succ m) ＝ ₀)
III = ⊕-property₁ {α m} {α (succ m)} (δ m) q

IV : u ＝ Succ (ι m)
IV = uncurry (Succ-criterion fe) III

ϕ-property fe α δ (succ n , p) (0 , q)= 𝟘-elim (Zero-not-Succ (II ⁻¹ ∙ IV))
where
u : ℕ∞
u = (α , δ)

I = α 0                           ＝⟨ (complement-involutive (α 0))⁻¹ ⟩
complement (complement (α 0)) ＝⟨ ap complement q ⟩
complement ₁                  ＝⟨ refl ⟩
₀                             ∎

II : u ＝ Zero
II = is-Zero-equal-Zero fe I

III : (α n ＝ ₁) × (α (succ n) ＝ ₀)
III = ⊕-property₁ {α n} {α (succ n)} (δ n) p

IV : u ＝ Succ (ι n)
IV = uncurry (Succ-criterion fe) III

ϕ-property fe α δ (succ n , p) (succ m , q) = VI
where
u : ℕ∞
u = (α , δ)

I : (α n ＝ ₁) × (α (succ n) ＝ ₀)
I = ⊕-property₁ (δ n) p

II : (α m ＝ ₁) × (α (succ m) ＝ ₀)
II = ⊕-property₁ (δ m) q

III : u ＝ Succ (ι n)
III = uncurry (Succ-criterion fe) I

IV : u ＝ Succ (ι m)
IV = uncurry (Succ-criterion fe) II

V : succ n ＝ succ m
V = ℕ-to-ℕ∞-lc (III ⁻¹ ∙ IV)

VI : (succ n , p) ＝ (succ m , q)
VI = to-T-＝ V

\end{code}

The following two observations give an alternative understanding of
the definition of γ:

\begin{code}

γ-case₀ : {β : ℕ → 𝟚} {n : ℕ}
→ β (succ n) ＝ ₀ → γ β (succ n) ＝ γ β n
γ-case₀ = ⊕-₀-right-neutral'

γ-case₁ : {β : ℕ → 𝟚} {n : ℕ}
→ β (succ n) ＝ ₁ → γ β (succ n) ＝ complement (γ β n)
γ-case₁ = ⊕-left-complement

\end{code}

We need the following consequences of the sequence β having at most
one ₁.

\begin{code}

at-most-one-₁-Lemma₀ : (β : ℕ → 𝟚)
→ has-at-most-one-₁ β
→ {m n : ℕ} → (β m ＝ ₁) × (β n ＝ ₁) → m ＝ n
at-most-one-₁-Lemma₀ β π {m} {n} (p , q) = ap pr₁ (π (m , p) (n , q))

at-most-one-₁-Lemma₁ : (β : ℕ → 𝟚)
→ has-at-most-one-₁ β
→ {m n : ℕ} → m ≠ n → β m ＝ ₁ → β n ＝ ₀
at-most-one-₁-Lemma₁ β π {m} {n} ν p = II
where
I : β n ≠ ₁
I q = ν (at-most-one-₁-Lemma₀ β π (p , q))

II : β n ＝ ₀
II = different-from-₁-equal-₀ I

\end{code}

The main lemma about γ is the following, where we are interested in
the choice k = n, but we need to prove the lemma for general k to get
a suitable induction hypothesis.

\begin{code}

γ-lemma : (β : ℕ → 𝟚)
→ has-at-most-one-₁ β
→ (n : ℕ) → β (succ n) ＝ ₁ → (k : ℕ) → k ≤ n → γ β k ＝ ₁
γ-lemma β π n p 0 l = w
where
w : complement (β 0) ＝ ₁
w = complement₁-back (at-most-one-₁-Lemma₁ β π (positive-not-zero n) p)

γ-lemma β π 0 p (succ k) ()
γ-lemma β π (succ n) p (succ k) l = w
where
IH : γ β k ＝ ₁
IH = γ-lemma β π (succ n) p k (≤-trans k n (succ n) l (≤-succ n))

I : succ (succ n) ≠ succ k
I m = not-less-than-itself n r
where
q : succ n ＝ k
q = succ-lc m

r : succ n ≤ n
r = transport⁻¹ (_≤ n) q l

II : β (succ k) ＝ ₀
II = at-most-one-₁-Lemma₁ β π I p

w : γ β k ⊕ β (succ k) ＝ ₁
w =  ⊕-intro₁₀ IH II

\end{code}

With this it is almost immediate that γ produces a decreasing
sequence if it is given a sequence with at most one ₁:

\begin{code}

γ-property : (β : ℕ → 𝟚)
→ has-at-most-one-₁ β
→ is-decreasing (γ β)
γ-property β π n = IV
where
I : β (succ n) ＝ ₁ → γ β n ＝ ₁
I p = γ-lemma β π n p n (≤-refl n)

II : β (succ n) ≤ γ β n
II = ≤₂-criterion I

III : γ β n ⊕ β (succ n) ≤ γ β n
III = ≤₂-add-left (γ β n) (β (succ n)) II

IV : γ β (succ n) ≤ γ β n
IV = III

module ℕ∞-equivalence (fe : funext₀) where

ℕ∞-to-ℕ∞' : ℕ∞ → ℕ∞'
ℕ∞-to-ℕ∞' (α , δ) = ϕ α , ϕ-property fe α δ

ℕ∞'-to-ℕ∞ : ℕ∞' → ℕ∞
ℕ∞'-to-ℕ∞ (β , π) = γ β , γ-property β π

ℕ∞-η : ℕ∞'-to-ℕ∞ ∘ ℕ∞-to-ℕ∞' ∼ id
ℕ∞-η (α , δ) = to-subtype-＝
(being-decreasing-is-prop fe)
(dfunext fe (ε α))

ℕ∞-ε : ℕ∞-to-ℕ∞' ∘ ℕ∞'-to-ℕ∞ ∼ id
ℕ∞-ε (β , π) = to-subtype-＝
(λ β → being-prop-is-prop fe)
(dfunext fe (η β))

\end{code}

And with this we get the promised equivalence.

\begin{code}

ℕ∞-to-ℕ∞'-≃ : ℕ∞ ≃ ℕ∞'
ℕ∞-to-ℕ∞'-≃ = qinveq ℕ∞-to-ℕ∞' (ℕ∞'-to-ℕ∞ , ℕ∞-η , ℕ∞-ε)

\end{code}