Martin Escardo, 20th June 2019 onwards.
The Cantor type of infinite binary sequences.
\begin{code}
{-# OPTIONS --safe --without-K #-}
open import Apartness.Definition
open import MLTT.Spartan
open import MLTT.Two-Properties
open import Naturals.Order
open import Naturals.ExitTruncation
open import Notation.Order
open import NotionsOfDecidability.Decidable
open import UF.DiscreteAndSeparated hiding (_♯_)
open import UF.Equiv
open import UF.FunExt
open import UF.PropTrunc
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
module TypeTopology.Cantor where
\end{code}
The Cantor type 𝟚ᴺ.
\begin{code}
𝟚ᴺ : 𝓤₀ ̇
𝟚ᴺ = ℕ → 𝟚
Cantor-is-set : funext₀ → is-set 𝟚ᴺ
Cantor-is-set fe = Π-is-set fe (λ _ → 𝟚-is-set)
\end{code}
We let α,β,γ range over the Cantor type.
The constant sequences:
\begin{code}
𝟎 : 𝟚ᴺ
𝟎 = (i ↦ ₀)
𝟏 : 𝟚ᴺ
𝟏 = (i ↦ ₁)
\end{code}
Cons, head and tail.
\begin{code}
head : 𝟚ᴺ → 𝟚
head α = α 0
tail : 𝟚ᴺ → 𝟚ᴺ
tail α = α ∘ succ
cons : 𝟚 → 𝟚ᴺ → 𝟚ᴺ
cons n α 0 = n
cons n α (succ i) = α i
_∷_ : 𝟚 → 𝟚ᴺ → 𝟚ᴺ
_∷_ = cons
cons-∼ : {x : 𝟚} {α β : 𝟚ᴺ} → α ∼ β → x ∷ α ∼ x ∷ β
cons-∼ h 0 = refl
cons-∼ h (succ i) = h i
∼-cons : {x y : 𝟚} {α : 𝟚ᴺ} → x ＝ y → x ∷ α ∼ y ∷ α
∼-cons refl = ∼-refl
head-cons : (n : 𝟚) (α : 𝟚ᴺ) → head (cons n α) ＝ n
head-cons n α = refl
tail-cons : (n : 𝟚) (α : 𝟚ᴺ) → tail (cons n α) ＝ α
tail-cons n α = refl
tail-cons' : (n : 𝟚) (α : 𝟚ᴺ) → tail (cons n α) ∼ α
tail-cons' n α i = refl
cons-head-tail : (α : 𝟚ᴺ) → α ∼ cons (head α) (tail α)
cons-head-tail α 0 = refl
cons-head-tail α (succ i) = refl
\end{code}
Agreement of two binary sequences α and β at the first n positions,
written α ＝⟦ n ⟧ β.
\begin{code}
_＝⟦_⟧_ : 𝟚ᴺ → ℕ → 𝟚ᴺ → 𝓤₀ ̇
α ＝⟦ 0 ⟧ β = 𝟙
α ＝⟦ succ n ⟧ β = (head α ＝ head β) × (tail α ＝⟦ n ⟧ tail β)
＝⟦⟧-refl : (α : 𝟚ᴺ) (k : ℕ) → α ＝⟦ k ⟧ α
＝⟦⟧-refl α 0 = ⋆
＝⟦⟧-refl α (succ k) = refl , ＝⟦⟧-refl (tail α) k
＝⟦⟧-trans : (α β γ : 𝟚ᴺ) (k : ℕ) → α ＝⟦ k ⟧ β → β ＝⟦ k ⟧ γ → α ＝⟦ k ⟧ γ
＝⟦⟧-trans α β γ 0 d e = ⋆
＝⟦⟧-trans α β γ (succ k) (h , t) (h' , t') =
(h ∙ h') ,
＝⟦⟧-trans (tail α) (tail β) (tail γ) k t t'
＝⟦⟧-sym : (α β : 𝟚ᴺ) (k : ℕ) → α ＝⟦ k ⟧ β → β ＝⟦ k ⟧ α
＝⟦⟧-sym α β 0 ⋆ = ⋆
＝⟦⟧-sym α β (succ k) (h , t) = (h ⁻¹) , ＝⟦⟧-sym (tail α) (tail β) k t
＝⟦⟧-is-decidable : (α β : 𝟚ᴺ) (k : ℕ) → is-decidable (α ＝⟦ k ⟧ β)
＝⟦⟧-is-decidable α β 0 = inl ⋆
＝⟦⟧-is-decidable α β (succ k) =
Cases (𝟚-is-discrete (head α) (head β))
(λ (h : head α ＝ head β)
→ map-decidable
(λ (t : tail α ＝⟦ k ⟧ tail β) → h , t)
(λ (_ , t) → t)
(＝⟦⟧-is-decidable (tail α) (tail β) k))
(λ (ν : head α ≠ head β) → inr (λ (h , _) → ν h))
\end{code}
We have that (α ＝⟦ n ⟧ β) iff α k ＝ β k for all k < n:
\begin{code}
agreement→ : (α β : 𝟚ᴺ)
(n : ℕ)
→ (α ＝⟦ n ⟧ β)
→ ((k : ℕ) → k < n → α k ＝ β k)
agreement→ α β 0 * k l = 𝟘-elim l
agreement→ α β (succ n) (p , e) 0 l = p
agreement→ α β (succ n) (p , e) (succ k) l = IH k l
where
IH : (k : ℕ) → k < n → α (succ k) ＝ β (succ k)
IH = agreement→ (tail α) (tail β) n e
agreement← : (α β : 𝟚ᴺ)
(n : ℕ)
→ ((k : ℕ) → k < n → α k ＝ β k)
→ (α ＝⟦ n ⟧ β)
agreement← α β 0 ϕ = ⋆
agreement← α β (succ n) ϕ = ϕ 0 ⋆ , agreement← (tail α) (tail β) n (ϕ ∘ succ)
\end{code}
A function 𝟚ᴺ → 𝟚 is uniformly continuous if it has a modulus
of continuity:
\begin{code}
_is-a-modulus-of-uniform-continuity-of_ : ℕ → (𝟚ᴺ → 𝟚) → 𝓤₀ ̇
m is-a-modulus-of-uniform-continuity-of p = ∀ α β → α ＝⟦ m ⟧ β → p α ＝ p β
uniformly-continuous : (𝟚ᴺ → 𝟚) → 𝓤₀ ̇
uniformly-continuous p = Σ m ꞉ ℕ , m is-a-modulus-of-uniform-continuity-of p
uniform-continuity-data = uniformly-continuous
\end{code}
Uniform continuity as defined above is data rather than property. This
is because any number bigger than a modulus of uniform continuity is
also a modulus.
TODO. Show that
(Σ p ꞉ (𝟚ᴺ → 𝟚) , uniformly-continuous p) ≃ (Σ n ꞉ ℕ , Fin (2 ^ n) → 𝟚)
If we define uniform continuity with ∃ rather than Σ, this is no
longer the case.
\begin{code}
continuous : (𝟚ᴺ → 𝟚) → 𝓤₀ ̇
continuous p = ∀ α → Σ m ꞉ ℕ , (∀ β → α ＝⟦ m ⟧ β → p α ＝ p β)
continuity-data = continuous
\end{code}
\begin{code}
module notions-of-continuity (pt : propositional-truncations-exist) where
open PropositionalTruncation pt
is-uniformly-continuous : (𝟚ᴺ → 𝟚) → 𝓤₀ ̇
is-uniformly-continuous p = ∃ m ꞉ ℕ , m is-a-modulus-of-uniform-continuity-of p
is-continuous : (𝟚ᴺ → 𝟚) → 𝓤₀ ̇
is-continuous p = ∀ α → ∃ m ꞉ ℕ , (∀ β → α ＝⟦ m ⟧ β → p α ＝ p β)
\end{code}
We now define the canonical apartness relation _♯_ for points of the
𝟚ᴺ type. Two sequences are apart if they differ at some index.
To make apartness into a proposition, which is crucial for our
purposes, we consider the minimal index at which they differ. This
allows us to avoid the assumption that propositional truncations
exist. But we still need function extensionality, so that the proof is
not in the realm of pure Martin-Löf type theory.
\begin{code}
open Apartness
_♯_ : 𝟚ᴺ → 𝟚ᴺ → 𝓤₀ ̇
α ♯ β = Σ n ꞉ ℕ , (α n ≠ β n)
× ((i : ℕ) → α i ≠ β i → n ≤ i)
\end{code}
We use δ to range over the type α n ≠ β n, and μ to range over the
minimality condition (i : ℕ) → α i ≠ β i → n ≤ i, for α, β and n
suitably specialized according to the situation we are considering.
We also use the letter "a" to range over the apartness type α ♯ β.
\begin{code}
apartness-criterion : (α β : 𝟚ᴺ) → (Σ n ꞉ ℕ , α n ≠ β n) → α ♯ β
apartness-criterion α β = minimal-witness
(λ n → α n ≠ β n)
(λ n → ¬-preserves-decidability
(𝟚-is-discrete (α n) (β n)))
apartness-criterion-converse : (α β : 𝟚ᴺ) → α ♯ β → (Σ n ꞉ ℕ , α n ≠ β n)
apartness-criterion-converse α β (n , δ , _) = (n , δ)
\end{code}
Hence, in view of the following, the type α ♯ β has the universal
property of the propositional truncation of the type Σ n ꞉ ℕ , α n ≠ β n.
\begin{code}
♯-is-prop-valued : Fun-Ext → is-prop-valued _♯_
♯-is-prop-valued fe α β (n , δ , μ) (n' , δ' , μ') = III
where
I : (n : ℕ) → is-prop ((α n ≠ β n) × ((i : ℕ) → α i ≠ β i → n ≤ i))
I n = ×-is-prop
(negations-are-props fe)
(Π₂-is-prop fe λ i _ → ≤-is-prop-valued n i)
II : n ＝ n'
II = ≤-anti n n' (μ n' δ') (μ' n δ)
III : (n , δ , μ) ＝[ α ♯ β ] (n' , δ' , μ')
III = to-subtype-＝ I II
\end{code}
The apartness axioms are satisfied, and, moreover, the apartness is tight.
\begin{code}
♯-is-irreflexive : is-irreflexive _♯_
♯-is-irreflexive α (n , δ , μ) = ≠-is-irrefl (α n) δ
♯-is-symmetric : is-symmetric _♯_
♯-is-symmetric α β (n , δ , μ) = n , (λ e → δ (e ⁻¹)) , λ i d → μ i (≠-sym d)
♯-strongly-cotransitive : is-strongly-cotransitive _♯_
♯-strongly-cotransitive α β γ (n , δ , μ) = III
where
I : (α n ≠ γ n) + (β n ≠ γ n)
I = discrete-types-are-cotransitive' 𝟚-is-discrete {α n} {β n} {γ n} δ
II : type-of I → (α ♯ γ) + (β ♯ γ)
II (inl d) = inl (apartness-criterion α γ (n , d))
II (inr d) = inr (apartness-criterion β γ (n , d))
III : (α ♯ γ) + (β ♯ γ)
III = II I
♯-is-strong-apartness : Fun-Ext → is-strong-apartness _♯_
♯-is-strong-apartness fe = ♯-is-prop-valued fe ,
♯-is-irreflexive ,
♯-is-symmetric ,
♯-strongly-cotransitive
♯-is-apartness : (fe : Fun-Ext)
→ (pt : propositional-truncations-exist)
→ is-apartness pt _♯_
♯-is-apartness fe pt =
strong-apartness-is-apartness pt _♯_ (♯-is-strong-apartness fe)
♯-is-tight : Fun-Ext → is-tight _♯_
♯-is-tight fe α β ν = dfunext fe I
where
I : (n : ℕ) → α n ＝ β n
I n = 𝟚-is-¬¬-separated (α n) (β n)
(λ (d : α n ≠ β n) → ν (apartness-criterion α β (n , d)))
\end{code}
If two sequences α and β are apart, they agree before the apartness index n.
\begin{code}
♯-agreement : (α β : 𝟚ᴺ)
((n , _) : α ♯ β)
(i : ℕ)
→ i < n → α i ＝ β i
♯-agreement α β (n , _ , μ) i ℓ = IV
where
I : α i ≠ β i → n ≤ i
I = μ i
II : ¬ (n ≤ i) → ¬ (α i ≠ β i)
II = contrapositive I
III : ¬ (n ≤ i)
III = less-not-bigger-or-equal i n ℓ
IV : α i ＝ β i
IV = 𝟚-is-¬¬-separated (α i) (β i) (II III)
\end{code}
The Cantor type is homogeneous.
\begin{code}
module _ (fe : funext₀) (α β : 𝟚ᴺ) where
Cantor-swap : 𝟚ᴺ → 𝟚ᴺ
Cantor-swap γ i = (β i ⊕ α i) ⊕ γ i
Cantor-swap-involutive : Cantor-swap ∘ Cantor-swap ∼ id
Cantor-swap-involutive γ = dfunext fe (λ i → ⊕-involutive {β i ⊕ α i} {γ i})
Cantor-swap-swaps∼ : Cantor-swap α ∼ β
Cantor-swap-swaps∼ i =
Cantor-swap α i ＝⟨ refl ⟩
(β i ⊕ α i) ⊕ α i ＝⟨ ⊕-assoc {β i} {α i} {α i} ⟩
β i ⊕ (α i ⊕ α i) ＝⟨ ap (β i ⊕_) (Lemma[b⊕b＝₀] {α i}) ⟩
β i ⊕ ₀ ＝⟨ ⊕-₀-right-neutral ⟩
β i ∎
Cantor-swap-swaps : Cantor-swap α ＝ β
Cantor-swap-swaps = dfunext fe Cantor-swap-swaps∼
Cantor-swap-swaps' : Cantor-swap β ＝ α
Cantor-swap-swaps' = involution-swap
Cantor-swap
Cantor-swap-involutive
Cantor-swap-swaps
Cantor-swap-≃ : 𝟚ᴺ ≃ 𝟚ᴺ
Cantor-swap-≃ = Cantor-swap ,
involutions-are-equivs Cantor-swap Cantor-swap-involutive
Cantor-homogeneous : funext₀
→ (α β : 𝟚ᴺ)
→ Σ f ꞉ 𝟚ᴺ ≃ 𝟚ᴺ , (⌜ f ⌝ α ＝ β)
Cantor-homogeneous fe α β = Cantor-swap-≃ fe α β , Cantor-swap-swaps fe α β
\end{code}