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}