Martin Escardo, November 2023.
\begin{code}
{-# OPTIONS --safe --without-K #-}
module CoNaturals.Type2Properties where
open import CoNaturals.Type hiding (is-finite')
open import CoNaturals.GenericConvergentSequence2
open import CoNaturals.Equivalence
open import MLTT.Spartan
open import MLTT.Two-Properties
open import Notation.CanonicalMap
open import TypeTopology.Cantor
open import UF.DiscreteAndSeparated
open import UF.Equiv
open import UF.FunExt
open import UF.Subsingletons
private
T = T-cantor
ϕ = ϕ-cantor
γ = γ-cantor
instance
Canonical-Map-ℕ-ℕ∞' : Canonical-Map ℕ ℕ∞'
ι {{Canonical-Map-ℕ-ℕ∞'}} = ℕ-to-ℕ∞'
canonical-map-ℕ∞'-ℕ→𝟚 : Canonical-Map ℕ∞' (ℕ → 𝟚)
ι {{canonical-map-ℕ∞'-ℕ→𝟚}} = ℕ∞'-to-ℕ→𝟚
module _ (fe : funext₀) where
open ℕ∞-equivalence fe
trivial-fact : (i : ℕ) → ϕ (ℕ∞-to-ℕ→𝟚 ∞) i ＝ ₀
trivial-fact 0 = refl
trivial-fact (succ i) = refl
Zero-preservation : ℕ∞-to-ℕ∞' Zero ＝ Zero'
Zero-preservation = to-subtype-＝ (has-at-most-one-₁-is-prop fe) (dfunext fe I)
where
I : ϕ (ι Zero) ∼ ι Zero'
I 0 = refl
I (succ i) = trivial-fact 0
Succ-preservation : (u : ℕ∞) → ℕ∞-to-ℕ∞' (Succ u) ＝ Succ' (ℕ∞-to-ℕ∞' u)
Succ-preservation u@(α , d) = to-subtype-＝ (has-at-most-one-₁-is-prop fe) II
where
I : ϕ (ℕ∞-to-ℕ→𝟚 (Succ u)) ∼ cons ₀ (ι (ℕ∞-to-ℕ∞' u))
I 0 = refl
I (succ _) = refl
II : ϕ (ℕ∞-to-ℕ→𝟚 (Succ u)) ＝ cons ₀ (ι (ℕ∞-to-ℕ∞' u))
II = dfunext fe I
∞-preservation : ℕ∞-to-ℕ∞' ∞ ＝ ∞'
∞-preservation = to-subtype-＝ (has-at-most-one-₁-is-prop fe)
(dfunext fe trivial-fact)
∞-gives-∞' : (u : ℕ∞') → ℕ∞'-to-ℕ∞ u ＝ ∞ → u ＝ ∞'
∞-gives-∞' u e =
u ＝⟨ II₀ ⟩
ℕ∞-to-ℕ∞' (ℕ∞'-to-ℕ∞ u) ＝⟨ II₁ ⟩
ℕ∞-to-ℕ∞' ∞ ＝⟨ II₂ ⟩
∞' ∎
where
II₀ = (inverses-are-sections' ℕ∞-to-ℕ∞'-≃ u)⁻¹
II₁ = ap ℕ∞-to-ℕ∞' e
II₂ = ∞-preservation
∞'-gives-∞ : (u : ℕ∞) → ℕ∞-to-ℕ∞' u ＝ ∞' → u ＝ ∞
∞'-gives-∞ u e =
u ＝⟨ (inverses-are-retractions' ℕ∞-to-ℕ∞'-≃ u)⁻¹ ⟩
ℕ∞'-to-ℕ∞ (ℕ∞-to-ℕ∞' u) ＝⟨ ap ℕ∞'-to-ℕ∞ e ⟩
ℕ∞'-to-ℕ∞ ∞' ＝⟨ ap ℕ∞'-to-ℕ∞ (∞-preservation ⁻¹) ⟩
ℕ∞'-to-ℕ∞ (ℕ∞-to-ℕ∞' ∞) ＝⟨ inverses-are-retractions' ℕ∞-to-ℕ∞'-≃ ∞ ⟩
∞ ∎
finite-preservation : (n : ℕ) → ℕ∞-to-ℕ∞' (ι n) ＝ ι n
finite-preservation 0 = Zero-preservation
finite-preservation (succ n) =
ℕ∞-to-ℕ∞' (ι (succ n)) ＝⟨ refl ⟩
ℕ∞-to-ℕ∞' (Succ (ι n)) ＝⟨ Succ-preservation (ι n) ⟩
Succ' (ℕ∞-to-ℕ∞' (ι n)) ＝⟨ ap Succ' (finite-preservation n) ⟩
Succ' (ι n) ＝⟨ refl ⟩
ι (succ n) ∎
finite-gives-finite' : (u : ℕ∞') → is-finite (ℕ∞'-to-ℕ∞ u) → is-finite' u
finite-gives-finite' u (n , e) = III
where
I : is-finite' (ι n)
I = ℕ-to-ℕ∞'-is-finite' n
II = ι n ＝⟨ (finite-preservation n)⁻¹ ⟩
ℕ∞-to-ℕ∞' (ι n) ＝⟨ ap ℕ∞-to-ℕ∞' e ⟩
ℕ∞-to-ℕ∞' (ℕ∞'-to-ℕ∞ u) ＝⟨ inverses-are-sections' ℕ∞-to-ℕ∞'-≃ u ⟩
u ∎
III : is-finite' u
III = transport is-finite' II I
finite'-preservation : (n : ℕ) → ℕ∞'-to-ℕ∞ (ι n) ＝ ι n
finite'-preservation n =
ℕ∞'-to-ℕ∞ (ι n) ＝⟨ I ⟩
ℕ∞'-to-ℕ∞ (ℕ∞-to-ℕ∞' (ι n)) ＝⟨ II ⟩
ι n ∎
where
I = (ap ℕ∞'-to-ℕ∞ (finite-preservation n))⁻¹
II = inverses-are-retractions' ℕ∞-to-ℕ∞'-≃ (ι n)
ℕ-to-ℕ∞'-lc : left-cancellable ℕ-to-ℕ∞'
ℕ-to-ℕ∞'-lc {n} {n'} e =
ℕ-to-ℕ∞-lc (
ι n ＝⟨ (finite'-preservation n)⁻¹ ⟩
ℕ∞'-to-ℕ∞ (ι n) ＝⟨ ap ℕ∞'-to-ℕ∞ e ⟩
ℕ∞'-to-ℕ∞ (ι n') ＝⟨ finite'-preservation n' ⟩
ι n' ∎)
ℕ-to-ℕ∞'-diagonal : (n : ℕ) → ℕ∞'-to-ℕ→𝟚 (ι n) n ＝ ₁
ℕ-to-ℕ∞'-diagonal 0 = refl
ℕ-to-ℕ∞'-diagonal (succ n) = ℕ-to-ℕ∞'-diagonal n
diagonal-lemma : (n : ℕ) (u : ℕ∞') → ℕ∞'-to-ℕ→𝟚 u n ＝ ₁ → u ＝ ι n
diagonal-lemma n u p = ℕ∞'-to-ℕ→𝟚-lc fe (dfunext fe f)
where
I : ℕ∞'-to-ℕ→𝟚 u n ＝ ℕ∞'-to-ℕ→𝟚 (ι n) n
I = ℕ∞'-to-ℕ→𝟚 u n ＝⟨ p ⟩
₁ ＝⟨ (ℕ-to-ℕ∞'-diagonal n)⁻¹ ⟩
ℕ∞'-to-ℕ→𝟚 (ι n) n ∎
II : (i : ℕ) → n ≠ i → ℕ∞'-to-ℕ→𝟚 u i ＝ ℕ∞'-to-ℕ→𝟚 (ι n) i
II i ν =
ℕ∞'-to-ℕ→𝟚 u i ＝⟨ II₀ ⟩
₀ ＝⟨ II₁ ⁻¹ ⟩
ℕ∞'-to-ℕ→𝟚 (ι n) i ∎
where
II₀ = different-from-₁-equal-₀
(λ (e : ℕ∞'-to-ℕ→𝟚 u i ＝ ₁)
→ ν (ℕ∞'-index-uniqueness u p e))
II₁ = different-from-₁-equal-₀
(λ (e : ℕ∞'-to-ℕ→𝟚 (ι n) i ＝ ₁)
→ ν (ℕ∞'-index-uniqueness (ι n) (ℕ-to-ℕ∞'-diagonal n) e))
f : (i : ℕ) → ℕ∞'-to-ℕ→𝟚 u i ＝ ℕ∞'-to-ℕ→𝟚 (ι n) i
f i = Cases (ℕ-is-discrete n i)
(λ (q : n ＝ i)
→ transport (λ - → ℕ∞'-to-ℕ→𝟚 u - ＝ ℕ∞'-to-ℕ→𝟚 (ι n) -) q I)
(λ (ν : n ≠ i)
→ II i ν)
size'-property' : {u : ℕ∞'} (φ : is-finite' u) → ι (size' {u} φ) ＝ u
size'-property' {u} φ = II ⁻¹
where
I : ℕ∞'-to-ℕ→𝟚 u (size' {u} φ) ＝ ₁
I = size'-property {u} φ
II : u ＝ ι (size' {u} φ)
II = diagonal-lemma (size' {u} φ) u I
finite'-is-natural : (u : ℕ∞') → is-finite' u → Σ n ꞉ ℕ , u ＝ ι n
finite'-is-natural u (n , p) = (n , diagonal-lemma n u p)
finite'-gives-finite : (u : ℕ∞) → is-finite' (ℕ∞-to-ℕ∞' u) → is-finite u
finite'-gives-finite u (n , e) = III
where
I : is-finite (ι n)
I = ℕ-to-ℕ∞-is-finite n
II = ι n ＝⟨ II₀ ⟩
ℕ∞'-to-ℕ∞ (ι n) ＝⟨ II₁ ⟩
ℕ∞'-to-ℕ∞ (ℕ∞-to-ℕ∞' u) ＝⟨ II₂ ⟩
u ∎
where
II₀ = (finite'-preservation n)⁻¹
II₁ = ap ℕ∞'-to-ℕ∞ ((diagonal-lemma n (ℕ∞-to-ℕ∞' u) e)⁻¹)
II₂ = inverses-are-retractions' ℕ∞-to-ℕ∞'-≃ u
III : is-finite u
III = transport is-finite II I
finite'-isolated : (n : ℕ) → is-isolated (ℕ-to-ℕ∞' n)
finite'-isolated n u = I (finite-isolated fe n (ℕ∞'-to-ℕ∞ u))
where
I : is-decidable (ι n ＝ ℕ∞'-to-ℕ∞ u) → is-decidable (ι n ＝ u)
I (inl e) = inl (ι n ＝⟨ (finite-preservation n)⁻¹ ⟩
ℕ∞-to-ℕ∞' (ι n) ＝⟨ ap ℕ∞-to-ℕ∞' e ⟩
ℕ∞-to-ℕ∞' (ℕ∞'-to-ℕ∞ u) ＝⟨ ℕ∞-ε u ⟩
u ∎)
I (inr ν) = inr (λ (e : ι n ＝ u)
→ ν (ι n ＝⟨ (finite'-preservation n)⁻¹ ⟩
ℕ∞'-to-ℕ∞ (ι n) ＝⟨ ap ℕ∞'-to-ℕ∞ e ⟩
ℕ∞'-to-ℕ∞ u ∎))
ℕ∞'-equality-criterion : (x y : ℕ∞')
→ ((n : ℕ) → ι n ＝ x → ι n ＝ y)
→ ((n : ℕ) → ι n ＝ y → ι n ＝ x)
→ x ＝ y
ℕ∞'-equality-criterion x y f g = ℕ∞'-to-ℕ→𝟚-lc fe V
where
I : (n : ℕ) (x y : ℕ∞')
→ (ι n ＝ x → ι n ＝ y)
→ ℕ∞'-to-ℕ→𝟚 x n ≤₂ ℕ∞'-to-ℕ→𝟚 y n
I n x y h = ≤₂-criterion a
where
a : ℕ∞'-to-ℕ→𝟚 x n ＝ ₁ → ℕ∞'-to-ℕ→𝟚 y n ＝ ₁
a e = ℕ∞'-to-ℕ→𝟚 y n ＝⟨ (ap (λ - → - n) IV)⁻¹ ⟩
ℕ∞'-to-ℕ→𝟚 (ι n) n ＝⟨ ℕ-to-ℕ∞'-diagonal n ⟩
₁ ∎
where
II : ι n ＝ x
II = (diagonal-lemma n x e)⁻¹
III : ι n ＝ y
III = h II
IV : ℕ∞'-to-ℕ→𝟚 (ι n) ＝ ℕ∞'-to-ℕ→𝟚 y
IV = ap ℕ∞'-to-ℕ→𝟚 III
V : ℕ∞'-to-ℕ→𝟚 x ＝ ℕ∞'-to-ℕ→𝟚 y
V = dfunext fe (λ n → ≤₂-anti (I n x y (f n)) (I n y x (g n)))
open import TypeTopology.TotallySeparated
ℕ∞'-is-totally-separated : is-totally-separated ℕ∞'
ℕ∞'-is-totally-separated = equiv-to-totally-separated
ℕ∞-to-ℕ∞'-≃
(ℕ∞-is-totally-separated fe)
\end{code}