Ayberk Tosun.
Formulations of some alternative definitions of the notion of continuity from
`MFPSAndVariations.Continuity` and proofs of their equivalences with the
original definitions.
First equivalence, for continuity, proved on 2023-06-13.
\begin{code}
{-# OPTIONS --safe --without-K --exact-split #-}
open import UF.FunExt
module EffectfulForcing.MFPSAndVariations.ContinuityProperties (fe : Fun-Ext) where
open import EffectfulForcing.MFPSAndVariations.Continuity
open import MGS.hlevels using (ℕ-is-set)
open import MLTT.Athenian
open import MLTT.Spartan
open import MLTT.Two-Properties
open import Naturals.Order
open import Naturals.Properties using (succ-no-fp; zero-not-positive)
open import UF.Embeddings
open import UF.Equiv
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
\end{code}
We first formulate the `α ＝⦅ n ⦆ β` relation expressing that two sequences `α`,
`β` of natural numbers are equal up to (not inclusive) some bound `n`. These
have been adapted from the `CantorSearch` module authored by Martín Escardó
(including the proofs `agreement→` and `agreement←`).
\begin{code}
hd : {X : 𝓤₀ ̇} → (ℕ → X) → X
hd α = α 0
tl : {X : 𝓤₀ ̇} → (ℕ → X) → ℕ → X
tl α = α ∘ succ
_＝⦅_⦆_ : {X : 𝓤₀ ̇} → (ℕ → X) → ℕ → (ℕ → X) → 𝓤₀ ̇
α ＝⦅ 0 ⦆ β = 𝟙
α ＝⦅ succ n ⦆ β = (hd α ＝ hd β) × tl α ＝⦅ n ⦆ tl β
\end{code}
A small lemma characterizing this relation.
\begin{code}
agreement→ : {X : 𝓤₀ ̇} (α α′ : ℕ → X) (n : ℕ)
→ α ＝⦅ n ⦆ α′
→ (i : ℕ) → (i <ℕ n) → α i ＝ α′ i
agreement→ α α′ zero p zero ()
agreement→ α α′ (succ n) (p₁ , p₂) zero q = p₁
agreement→ α α′ (succ n) (p₁ , p₂) (succ i) q = IH i q
where
IH : (j : ℕ) → j <ℕ n → α (succ j) ＝ α′ (succ j)
IH = agreement→ (tl α) (tl α′) n p₂
agreement← : (α α′ : Baire) (n : ℕ)
→ ((i : ℕ) → (i <ℕ n) → α i ＝ α′ i)
→ α ＝⦅ n ⦆ α′
agreement← α α′ zero φ = ⋆
agreement← α α′ (succ n) φ = φ 0 ⋆ , (agreement← (tl α) (tl α′) n ψ)
where
ψ : (j : ℕ) → j <ℕ n → tl α j ＝ tl α′ j
ψ j p = φ (succ j) (succ-monotone (succ j) n p)
\end{code}
\section{Continuity}
Using the `_＝⦅_⦆_` relation, we express the “usual” notion of continuity
mentioned in the TODO. We call this `is-continuous₀` and prove at the end of the
module that it is logically equivalent to `is-continuous`.
\begin{code}
is-continuous₀ : (Baire → ℕ) → 𝓤₀ ̇
is-continuous₀ f =
(α : Baire) → Σ n ꞉ ℕ , ((α′ : Baire) → α ＝⦅ n ⦆ α′ → f α ＝ f α′)
\end{code}
We also define the following operation `modulus-at₀` that projects out the
modulus of continuity computed by a proof of `is-continuous₀`:
\begin{code}
modulus-at₀ : (f : Baire → ℕ) → is-continuous₀ f → Baire → ℕ
modulus-at₀ f c α = pr₁ (c α)
\end{code}
We now formulate an alternative non-inductive version of the `_＝⟪_⟫_` relation
that we call `_＝⟪_⟫₀_` and prove its logical equivalence with `_＝⟪_⟫_`. The
motivation for the non-inductive formulation is to use it as an intermediate
step to simplify our proofs.
\begin{code}
_＝⟪_⟫₀_ : {X : 𝓤₀ ̇} → (ℕ → X) → List ℕ → (ℕ → X) → 𝓤₀ ̇
_＝⟪_⟫₀_ α₁ s α₂ = (i : ℕ) → member i s → α₁ i ＝ α₂ i
\end{code}
It is an obvious fact that equality up to `i ∷ is` (with `_＝⟪_⟫₀_`) entails
equality up to `is`. We record this fact as `＝⟪⟫₀-cons`.
\begin{code}
＝⟪⟫₀-cons : {X : 𝓤₀ ̇} (α α′ : ℕ → X) (i : ℕ) (is : List ℕ)
→ α ＝⟪ i ∷ is ⟫₀ α′ → α ＝⟪ is ⟫₀ α′
＝⟪⟫₀-cons α α′ i is t j p = t j (in-tail p)
\end{code}
We now generalize this fact. Equality up to `ms ++ ns` entails both equality up
to `ms` and up to `ns`. In other words, `α₁ ＝⟪_⟫₀ α₂` is a semigroup
homomorphism from semigroup `(List ℕ, _++_)` into semigroup `(𝓤₀, _×_)`.
\begin{code}
＝⟪⟫-++-lemma₁ : {X : 𝓤₀ ̇} (α₁ α₂ : ℕ → X) (ms ns : List ℕ)
→ α₁ ＝⟪ ms ++ ns ⟫₀ α₂
→ (α₁ ＝⟪ ms ⟫₀ α₂) × (α₁ ＝⟪ ns ⟫₀ α₂)
＝⟪⟫-++-lemma₁ α₁ α₂ ms ns p = † , ‡
where
† : α₁ ＝⟪ ms ⟫₀ α₂
† n q = p n (right-concatenation-preserves-membership n ms ns q)
‡ : α₁ ＝⟪ ns ⟫₀ α₂
‡ n q = p n (left-concatenation-preserves-membership n ns ms q)
＝⟪⟫-++-lemma₂ : {X : 𝓤₀ ̇} (α₁ α₂ : ℕ → X) (ms ns : List ℕ)
→ (α₁ ＝⟪ ms ⟫₀ α₂) × (α₁ ＝⟪ ns ⟫₀ α₂)
→ α₁ ＝⟪ ms ++ ns ⟫₀ α₂
＝⟪⟫-++-lemma₂ α₁ α₂ ms ns (p , q) i r =
cases (p i) (q i) (++-membership₁ i ms ns r)
＝⟪⟫-respects-list-concatenation : {X : 𝓤₀ ̇} (α₁ α₂ : ℕ → X) (ms ns : List ℕ)
→ α₁ ＝⟪ ms ++ ns ⟫₀ α₂
↔ (α₁ ＝⟪ ms ⟫₀ α₂) × (α₁ ＝⟪ ns ⟫₀ α₂)
＝⟪⟫-respects-list-concatenation α₁ α₂ ms ns =
＝⟪⟫-++-lemma₁ α₁ α₂ ms ns , ＝⟪⟫-++-lemma₂ α₁ α₂ ms ns
\end{code}
We now record the fact that the alternative version of `_＝⟪_⟫_` is logically
equivalent to the original version.
\begin{code}
＝⟪⟫₀-implies-＝⟪⟫ : {X : 𝓤₀ ̇} (α α′ : ℕ → X) (s : List ℕ)
→ α ＝⟪ s ⟫₀ α′ → α ＝⟪ s ⟫ α′
＝⟪⟫₀-implies-＝⟪⟫ α α′ [] t = []
＝⟪⟫₀-implies-＝⟪⟫ α α′ (i ∷ is) t = t i in-head ∷ IH
where
IH = ＝⟪⟫₀-implies-＝⟪⟫ α α′ is (＝⟪⟫₀-cons α α′ i is t)
＝⟪⟫-implies-＝⟪⟫₀ : {X : 𝓤₀ ̇} (α β : ℕ → X) (s : List ℕ)
→ α ＝⟪ s ⟫ β → α ＝⟪ s ⟫₀ β
＝⟪⟫-implies-＝⟪⟫₀ α α′ [] [] i ()
＝⟪⟫-implies-＝⟪⟫₀ α α′ (i ∷ is) (p ∷ ps) i in-head = p
＝⟪⟫-implies-＝⟪⟫₀ α α′ (_ ∷ is) (p ∷ ps) j (in-tail q) = IH
where
IH = ＝⟪⟫-implies-＝⟪⟫₀ α α′ is ps j q
\end{code}
We now define the `maximum` function computing the maximum of a given list of
natural numbers.
\begin{code}
maximum : List ℕ → ℕ
maximum = foldr max 0
\end{code}
Recall that the first (logical) equivalence we would like to prove is that
between `is-continuous` and `is-continuous₀`. We tackle this in the next
section, and the converse direction in the section after that.
\section{`is-continuous` implies `is-continuous₀`}
The fact that `is-continuous` implies `is-continuous₀` is the easy direction of
the equivalence in consideration. We need only two minor lemmas to conclude
this.
\begin{code}
member-implies-below-max : (s : List ℕ) (i : ℕ) → member i s → i ≤ℕ maximum s
member-implies-below-max (m ∷ ns) m in-head = max-≤-upper-bound m (maximum ns)
member-implies-below-max (n ∷ ns) m (in-tail p) =
≤-trans m _ _ IH (max-≤-upper-bound' (maximum ns) n)
where
IH =(member-implies-below-max ns m p)
＝⦅⦆-implies-＝⟪⟫ : {X : 𝓤₀ ̇} (α α′ : ℕ → X) (s : List ℕ)
→ α ＝⦅ succ (maximum s) ⦆ α′
→ α ＝⟪ s ⟫ α′
＝⦅⦆-implies-＝⟪⟫ α α′ s t = ＝⟪⟫₀-implies-＝⟪⟫ α α′ s †
where
m : ℕ
m = succ (maximum s)
† : α ＝⟪ s ⟫₀ α′
† i p = agreement→ α α′ m t i (member-implies-below-max s i p)
continuity-implies-continuity₀ : (f : Baire → ℕ)
→ is-continuous f → is-continuous₀ f
continuity-implies-continuity₀ f c = †
where
† : is-continuous₀ f
† α = m , γ
where
s = pr₁ (c α)
m = succ (maximum s)
γ : (α′ : Baire) → α ＝⦅ m ⦆ α′ → f α ＝ f α′
γ α′ p = pr₂ (c α) α′ (＝⦅⦆-implies-＝⟪⟫ α α′ s p)
\end{code}
\section{`is-continuous₀` implies `is-continuous`}
We now address the converse direction which is harder.
We first define a `range` function such that `range n` is the list `[0..n]` and
prove its completeness.
\begin{code}
range : ℕ → List ℕ
range zero = [ 0 ]
range (succ n) = succ n ∷ range n
range-succ : (i n : ℕ) → member i (range n) → member (succ i) (range (succ n))
range-succ zero zero p = in-head
range-succ (succ i) zero (in-tail ())
range-succ zero (succ n) (in-tail p) = in-tail (range-succ zero n p)
range-succ (succ i) (succ i) in-head = in-head
range-succ (succ i) (succ n) (in-tail p) = in-tail (range-succ (succ i) n p)
range-is-complete : (i n : ℕ) → i ≤ℕ n → member i (range n)
range-is-complete zero zero p = in-head
range-is-complete zero (succ n) p = in-tail (range-is-complete zero n p)
range-is-complete (succ i) (succ n) p = range-succ i n (range-is-complete i n p)
\end{code}
We combine all these into a final lemma that we need:
\begin{code}
＝⟪⟫-range-implies-＝⦅⦆ : (α α′ : Baire) (n : ℕ)
→ α ＝⟪ range n ⟫ α′
→ α ＝⦅ n ⦆ α′
＝⟪⟫-range-implies-＝⦅⦆ α α′ n p = agreement← α α′ n †
where
† : (j : ℕ) → j <ℕ n → α j ＝ α′ j
† j q = ＝⟪⟫-implies-＝⟪⟫₀ α α′ (range n) p j ‡
where
‡ : member j (range n)
‡ = range-is-complete j n (<-coarser-than-≤ j n q)
\end{code}
The result we want now follows easily:
\begin{code}
continuity₀-implies-continuity : (f : Baire → ℕ)
→ is-continuous₀ f → is-continuous f
continuity₀-implies-continuity f c α = range m , γ
where
m = modulus-at₀ f c α
γ : (α′ : Baire) → α ＝⟪ range m ⟫ α′ → f α ＝ f α′
γ α′ p = pr₂ (c α) α′ (＝⟪⟫-range-implies-＝⦅⦆ α α′ m p)
\end{code}
Finally, we record the logical equivalence as a fact in itself.
\begin{code}
continuous₀-iff-continuous : (f : Baire → ℕ)
→ is-continuous₀ f ↔ is-continuous f
continuous₀-iff-continuous f = † , ‡
where
† = continuity₀-implies-continuity f
‡ = continuity-implies-continuity₀ f
\end{code}
\section{Uniform continuity}
We start by defining the notion of being “Boolean-valued”: a point `α : Baire`
of the Baire space is called Boolean if its range is a subset of `{0, 1}`.
\begin{code}
is-boolean-valued : ℕ → 𝓤₀ ̇
is-boolean-valued n = (n ＝ 0) + (n ＝ 1)
embedding-𝟚-ℕ-gives-boolean : (b : 𝟚) → is-boolean-valued (embedding-𝟚-ℕ b)
embedding-𝟚-ℕ-gives-boolean ₀ = inl refl
embedding-𝟚-ℕ-gives-boolean ₁ = inr refl
\end{code}
The following is the inverse of `embedding-𝟚-ℕ`: it takes us back to `𝟚` from a
Boolean-valued natural number.
\begin{code}
to-bool : (n : ℕ) → is-boolean-valued n → 𝟚
to-bool _ (inl p) = ₀
to-bool _ (inr q) = ₁
\end{code}
A point `α : Baire` of the Baire space is called a _Boolean point_ if its range
is a subset of {`₀`, `₁`}.
\begin{code}
is-boolean-point : Baire → 𝓤₀ ̇
is-boolean-point α = (n : ℕ) → is-boolean-valued (α n)
\end{code}
Being Boolean-valued is a proposition, from which it follows that being
a Boolean point is also a proposition.
\begin{code}
being-boolean-is-prop : (α : Baire) (i : ℕ) → is-prop (is-boolean-valued (α i))
being-boolean-is-prop α i (inl p) (inl q) = ap inl (ℕ-is-set (α i) 0 p q)
being-boolean-is-prop α i (inr p) (inr q) = ap inr (ℕ-is-set (α i) 1 p q)
being-boolean-is-prop α i (inl p) (inr q) = 𝟘-elim (succ-no-fp 0 ※)
where
※ : 0 ＝ 1
※ = 0 ＝⟨ p ⁻¹ ⟩ α i ＝⟨ q ⟩ 1 ∎
being-boolean-is-prop α i (inr p) (inl q) = 𝟘-elim (succ-no-fp 0 ※)
where
※ : 0 ＝ 1
※ = 0 ＝⟨ q ⁻¹ ⟩ α i ＝⟨ p ⟩ 1 ∎
being-boolean-point-is-prop : (α : Baire) → is-prop (is-boolean-point α)
being-boolean-point-is-prop α = Π-is-prop fe (being-boolean-is-prop α)
\end{code}
Using this, we can give an alternative definition of the Cantor space as the
subtype of Baire space consisting of the Boolean points,
\begin{code}
Cantor₀ : 𝓤₀ ̇
Cantor₀ = Σ α ꞉ Baire , is-boolean-point α
point-of : Cantor₀ → Baire
point-of (α , _) = α
\end{code}
This is clearly equivalent to the usual definition.
\begin{code}
to-baire-gives-boolean-point : (α : Cantor) → is-boolean-point (embedding-C-B α)
to-baire-gives-boolean-point α = embedding-𝟚-ℕ-gives-boolean ∘ α
\end{code}
We now prove the equivalence between `Cantor` and `Cantor₀`.
\begin{code}
to-cantor₀ : Cantor → Cantor₀
to-cantor₀ α = embedding-C-B α , to-baire-gives-boolean-point α
to-cantor : Cantor₀ → Cantor
to-cantor (α , p) = λ n → to-bool (α n) (p n)
\end{code}
\begin{code}
embedding-𝟚-ℕ-0-implies-is-₀ : (b : 𝟚) → embedding-𝟚-ℕ b ＝ 0 → b ＝ ₀
embedding-𝟚-ℕ-0-implies-is-₀ ₀ p = refl
embedding-𝟚-ℕ-1-implies-is-₁ : (b : 𝟚) → embedding-𝟚-ℕ b ＝ 1 → b ＝ ₁
embedding-𝟚-ℕ-1-implies-is-₁ ₁ p = refl
embedding-𝟚-ℕ-is-embedding : is-embedding embedding-𝟚-ℕ
embedding-𝟚-ℕ-is-embedding m (b , p) (c , q) = to-subtype-＝ † ♢
where
† : (b : 𝟚) → is-prop (embedding-𝟚-ℕ b ＝ m)
† b = ℕ-is-set (embedding-𝟚-ℕ b) m
φ : embedding-𝟚-ℕ b ＝ embedding-𝟚-ℕ c
φ = embedding-𝟚-ℕ b ＝⟨ p ⟩ m ＝⟨ q ⁻¹ ⟩ embedding-𝟚-ℕ c ∎
ϑ₁ : b ＝ ₀ → c ＝ ₀ → b ＝ c
ϑ₁ p q = b ＝⟨ p ⟩ ₀ ＝⟨ q ⁻¹ ⟩ c ∎
ϑ₂ : b ＝ ₀ → c ＝ ₁ → b ＝ c
ϑ₂ p q = 𝟘-elim (zero-not-positive (embedding-𝟚-ℕ ₀) ϟ)
where
ϟ : 0 ＝ 1
ϟ = 0 ＝⟨ refl ⟩
embedding-𝟚-ℕ ₀ ＝⟨ ap embedding-𝟚-ℕ p ⁻¹ ⟩
embedding-𝟚-ℕ b ＝⟨ φ ⟩
embedding-𝟚-ℕ c ＝⟨ ap embedding-𝟚-ℕ q ⟩
embedding-𝟚-ℕ ₁ ＝⟨ refl ⟩
1 ∎
ϑ₃ : b ＝ ₁ → c ＝ ₀ → b ＝ c
ϑ₃ p q = 𝟘-elim (zero-not-positive (embedding-𝟚-ℕ ₀) ϟ)
where
ϟ : 0 ＝ 1
ϟ = 0 ＝⟨ refl ⟩
embedding-𝟚-ℕ ₀ ＝⟨ ap embedding-𝟚-ℕ q ⁻¹ ⟩
embedding-𝟚-ℕ c ＝⟨ φ ⁻¹ ⟩
embedding-𝟚-ℕ b ＝⟨ ap embedding-𝟚-ℕ p ⟩
1 ∎
ϑ₄ : b ＝ ₁ → c ＝ ₁ → b ＝ c
ϑ₄ p q = b ＝⟨ p ⟩ ₁ ＝⟨ q ⁻¹ ⟩ c ∎
ξ : b ＝ ₀ → b ＝ c
ξ r = cases (ϑ₁ r) (ϑ₂ r) (𝟚-possibilities c)
ζ : b ＝ ₁ → b ＝ c
ζ r = cases (ϑ₃ r) (ϑ₄ r) (𝟚-possibilities c)
♢ : b ＝ c
♢ = cases ξ ζ (𝟚-possibilities b)
\end{code}
The map `to-cantor₀` is a section whose retraction is the map `to-cantor`
\begin{code}
to-cantor-cancels-to-cantor₀ : (α : Cantor) → to-cantor (to-cantor₀ α) ＝ α
to-cantor-cancels-to-cantor₀ α = dfunext fe †
where
† : (n : ℕ)
→ to-bool (embedding-𝟚-ℕ (α n)) (to-baire-gives-boolean-point α n) ＝ α n
† n = cases †₁ †₂ (to-baire-gives-boolean-point α n)
where
†₁ : embedding-𝟚-ℕ (α n) ＝ 0
→ to-bool (embedding-𝟚-ℕ (α n)) (to-baire-gives-boolean-point α n) ＝ α n
†₁ p =
to-bool (embedding-𝟚-ℕ (α n)) (embedding-𝟚-ℕ-gives-boolean (α n)) ＝⟨ Ⅰ ⟩
to-bool 0 (inl refl) ＝⟨ Ⅱ ⟩
α n ∎
where
Ⅰ = ap
(λ - → to-bool (embedding-𝟚-ℕ -) (embedding-𝟚-ℕ-gives-boolean -))
(embedding-𝟚-ℕ-0-implies-is-₀ (α n) p)
Ⅱ = embedding-𝟚-ℕ-0-implies-is-₀ (α n) p ⁻¹
†₂ : embedding-𝟚-ℕ (α n) ＝ 1
→ to-bool (embedding-𝟚-ℕ (α n)) (to-baire-gives-boolean-point α n) ＝ α n
†₂ p =
to-bool (embedding-𝟚-ℕ (α n)) (embedding-𝟚-ℕ-gives-boolean (α n)) ＝⟨ Ⅰ ⟩
to-bool 1 (inr refl) ＝⟨ Ⅱ ⟩
α n ∎
where
Ⅰ = ap
(λ - → to-bool (embedding-𝟚-ℕ -) (embedding-𝟚-ℕ-gives-boolean -))
(embedding-𝟚-ℕ-1-implies-is-₁ (α n) p)
Ⅱ = embedding-𝟚-ℕ-1-implies-is-₁ (α n) p ⁻¹
point-of-lemma : (α : Cantor)
→ point-of (to-cantor₀ α) ∼ embedding-𝟚-ℕ ∘ α
point-of-lemma α = λ _ → refl
to-bool-lemma₁ : (α : Baire) (bv : is-boolean-point α) (i : ℕ)
→ α i ＝ 0 → to-bool (α i) (bv i) ＝ ₀
to-bool-lemma₁ α bv i p = ap (to-bool (α i)) †
where
† : bv i ＝ inl p
† = being-boolean-is-prop α i (bv i) (inl p)
to-bool-lemma₂ : (α : Baire) (bv : is-boolean-point α) (i : ℕ)
→ α i ＝ 1 → to-bool (α i) (bv i) ＝ ₁
to-bool-lemma₂ α bv i p = ap (to-bool (α i)) †
where
† : bv i ＝ inr p
† = being-boolean-is-prop α i (bv i) (inr p)
to-cantor₀-cancels-to-cantor : to-cantor₀ ∘ to-cantor ∼ id
to-cantor₀-cancels-to-cantor (α , bv) = to-subtype-＝ being-boolean-point-is-prop †
where
‡₁ : (i : ℕ) → α i ＝ 0 → embedding-C-B (to-cantor (α , bv)) i ＝ α i
‡₁ i p = embedding-𝟚-ℕ (to-bool (α i) (bv i)) ＝⟨ Ⅰ ⟩
0 ＝⟨ p ⁻¹ ⟩
α i ∎
where
Ⅰ = ap embedding-𝟚-ℕ (to-bool-lemma₁ α bv i p)
‡₂ : (i : ℕ) → α i ＝ 1 → embedding-C-B (to-cantor (α , bv)) i ＝ α i
‡₂ i p = embedding-C-B (to-cantor (α , bv)) i ＝⟨ refl ⟩
embedding-𝟚-ℕ (to-bool (α i) (bv i)) ＝⟨ Ⅰ ⟩
embedding-𝟚-ℕ ₁ ＝⟨ refl ⟩
1 ＝⟨ p ⁻¹ ⟩
α i ∎
where
Ⅰ = ap embedding-𝟚-ℕ (to-bool-lemma₂ α bv i p)
‡ : embedding-C-B (to-cantor (α , bv)) ∼ α
‡ i = embedding-C-B (to-cantor (α , bv)) i ＝⟨ refl ⟩
embedding-𝟚-ℕ (to-bool (α i) (bv i)) ＝⟨ Ⅰ ⟩
α i ∎
where
Ⅰ : embedding-𝟚-ℕ (to-bool (α i) (bv i)) ＝ α i
Ⅰ = cases (‡₁ i) (‡₂ i) (bv i)
† : embedding-C-B (to-cantor (α , bv)) ＝ α
† = dfunext fe ‡
cantor-equiv-cantor₀ : Cantor ≃ Cantor₀
cantor-equiv-cantor₀ = to-cantor₀ , (to-cantor , φ) , to-cantor , ψ
where
φ : to-cantor₀ ∘ to-cantor ∼ id
φ = to-cantor₀-cancels-to-cantor
ψ : to-cantor ∘ to-cantor₀ ∼ id
ψ = to-cantor-cancels-to-cantor₀
\end{code}
Now, we start working towards showing the equivalence of the alternative notion
of uniform continuity with the original one. We define the following function
`sequentialize` that flattens a binary tree into a list.
\begin{code}
sequentialize : {X : 𝓤₀ ̇} → BT X → List X
sequentialize [] = []
sequentialize (x ∷ φ) = x ∷ sequentialize (φ ₀) ++ sequentialize (φ ₁)
\end{code}
Recall the `maximum` operation that we used in the proof of
`continuous₀-iff-continuous`. We now define an analogue of this operation for
uniform continuity, on binary trees instead of lists.
\begin{code}
maximumᵤ : BT ℕ → ℕ
maximumᵤ [] = 0
maximumᵤ (n ∷ φ) = max n (max (maximumᵤ (φ ₀)) (maximumᵤ (φ ₁)))
\end{code}
Alternatively, this operation could also be defined as:
\begin{code}
maximumᵤ′ : BT ℕ → ℕ
maximumᵤ′ = maximum ∘ sequentialize
\end{code}
We now prove a lemma that we need about `maximum`: it map `ms ++ ns` to the
binary maximum of the maxima of `ms` and `ns`.
\begin{code}
maximum-maps-++-to-max-of-maximum
: (ms ns : List ℕ)
→ maximum (ms ++ ns) ＝ max (maximum ms) (maximum ns)
maximum-maps-++-to-max-of-maximum [] ns = refl
maximum-maps-++-to-max-of-maximum (m ∷ ms) ns = †
where
IH : maximum (ms ++ ns) ＝ max (maximum ms) (maximum ns)
IH = maximum-maps-++-to-max-of-maximum ms ns
Ⅰ = ap (max m) IH
Ⅱ = max-assoc m (maximum ms) (maximum ns) ⁻¹
† : max m (maximum (ms ++ ns)) ＝ max (max m (maximum (ms))) (maximum ns)
† = max m (maximum (ms ++ ns)) ＝⟨ Ⅰ ⟩
max m (max (maximum ms) (maximum ns)) ＝⟨ Ⅱ ⟩
max (max m (maximum ms)) (maximum ns) ∎
\end{code}
It is an easy corollary of this that `maximumᵤ′` and `maximumᵤ` are equal.
\begin{code}
maximumᵤ′-equivalent-to-maximumᵤ : (t : BT ℕ) → maximumᵤ t ＝ maximumᵤ′ t
maximumᵤ′-equivalent-to-maximumᵤ [] = refl
maximumᵤ′-equivalent-to-maximumᵤ (n ∷ φ) = †
where
IH₁ = maximumᵤ′-equivalent-to-maximumᵤ (φ ₀)
IH₂ = maximumᵤ′-equivalent-to-maximumᵤ (φ ₁)
Ⅰ = ap (λ - → max - (maximumᵤ (φ ₁))) IH₁
Ⅱ = ap (max (maximumᵤ′ (φ ₀))) IH₂
Ⅲ = maximum-maps-++-to-max-of-maximum
(sequentialize (φ ₀))
(sequentialize (φ ₁)) ⁻¹
‡ : max (maximumᵤ (φ ₀)) (maximumᵤ (φ ₁))
＝ maximum (sequentialize (φ ₀) ++ sequentialize (φ ₁))
‡ =
max (maximumᵤ (φ ₀)) (maximumᵤ (φ ₁)) ＝⟨ Ⅰ ⟩
max (maximumᵤ′ (φ ₀)) (maximumᵤ (φ ₁)) ＝⟨ Ⅱ ⟩
max (maximumᵤ′ (φ ₀)) (maximumᵤ′ (φ ₁)) ＝⟨ refl ⟩
max (maximum (sequentialize (φ ₀))) (maximum (sequentialize (φ ₁))) ＝⟨ Ⅲ ⟩
maximum (sequentialize (φ ₀) ++ sequentialize (φ ₁)) ∎
† : max n (max (maximumᵤ (φ ₀)) (maximumᵤ (φ ₁)))
＝ max n (maximum (sequentialize (φ ₀) ++ sequentialize (φ ₁)))
† = ap (max n) ‡
\end{code}
We define the following function `to-cantor₀-map`, that extends `to-cantor₀`
from points of the Cantor space to maps `Cantor → ℕ`, and prove some small
lemmas about it.
\begin{code}
to-cantor₀-map : (Cantor → ℕ) → Cantor₀ → ℕ
to-cantor₀-map f = f ∘ to-cantor
to-cantor₀-map-lemma : (f : Cantor → ℕ) (α β : Cantor)
→ let f₀ = to-cantor₀-map f in
f₀ (to-cantor₀ α) ＝ f₀ (to-cantor₀ β)
→ f α ＝ f β
to-cantor₀-map-lemma f α β p = f α ＝⟨ Ⅰ ⟩
f (to-cantor (to-cantor₀ α)) ＝⟨ Ⅱ ⟩
f (to-cantor (to-cantor₀ β)) ＝⟨ Ⅲ ⟩
f β ∎
where
Ⅰ = ap f (to-cantor-cancels-to-cantor₀ α ⁻¹ )
Ⅱ = p
Ⅲ = ap f (to-cantor-cancels-to-cantor₀ β)
\end{code}
We now define the alternative notion of uniform continuity, analogous to
`is-continuous₀`.
\begin{code}
is-uniformly-continuous₀ : (Cantor → ℕ) → 𝓤₀ ̇
is-uniformly-continuous₀ f =
Σ n ꞉ ℕ , ((ξ₁@(α₁ , _) ξ₂@(α₂ , _) : Cantor₀) → α₁ ＝⦅ n ⦆ α₂ → f₀ ξ₁ ＝ f₀ ξ₂)
where
f₀ : Cantor₀ → ℕ
f₀ = to-cantor₀-map f
modulus-atᵘ₀ : (f : Cantor → ℕ) → is-uniformly-continuous₀ f → ℕ
modulus-atᵘ₀ f (m , _) = m
\end{code}
The equality-up-to relation `_＝⟪_⟫₀_` that we have defined above, implies the
`_＝⟦_⟧_` relation that uses binary trees.
\begin{code}
＝⟪⟫₀-implies-＝⟦⟧ : {X : 𝓤₀ ̇} (α₁ α₂ : ℕ → X) (t : BT ℕ)
→ α₁ ＝⟪ sequentialize t ⟫₀ α₂ → α₁ ＝⟦ t ⟧ α₂
＝⟪⟫₀-implies-＝⟦⟧ α₁ α₂ [] p = []
＝⟪⟫₀-implies-＝⟦⟧ α₁ α₂ (x ∷ φ) p = p x in-head ∷ †
where
ϑ : α₁ ＝⟪ sequentialize (φ ₀) ++ sequentialize (φ ₁) ⟫₀ α₂
ϑ = ＝⟪⟫₀-cons α₁ α₂ x (sequentialize (φ ₀) ++ sequentialize (φ ₁)) p
ς₀ : α₁ ＝⟪ sequentialize (φ ₀) ⟫₀ α₂
ς₀ = pr₁ (＝⟪⟫-++-lemma₁ α₁ α₂ (sequentialize (φ ₀)) (sequentialize (φ ₁)) ϑ)
ς₁ : α₁ ＝⟪ sequentialize (φ ₁) ⟫₀ α₂
ς₁ = pr₂ (＝⟪⟫-++-lemma₁ α₁ α₂ (sequentialize (φ ₀)) (sequentialize (φ ₁)) ϑ)
† : (j : 𝟚) → α₁ ＝⟦ φ j ⟧ α₂
† ₀ = ＝⟪⟫₀-implies-＝⟦⟧ α₁ α₂ (φ ₀) ς₀
† ₁ = ＝⟪⟫₀-implies-＝⟦⟧ α₁ α₂ (φ ₁) ς₁
\end{code}
Conversely, the `_＝⟦_⟧_` relation implies the `_＝⟪_⟫₀` relation.
\begin{code}
＝⟦⟧-implies-＝⟪⟫₀ : (α β : Baire) (t : BT ℕ)
→ α ＝⟦ t ⟧ β → α ＝⟪ sequentialize t ⟫₀ β
＝⟦⟧-implies-＝⟪⟫₀ _ _ [] _ _ ()
＝⟦⟧-implies-＝⟪⟫₀ α β (n ∷ φ) (p ∷ _) _ in-head = p
＝⟦⟧-implies-＝⟪⟫₀ α β (n ∷ φ) (p ∷ ψ) i (in-tail q) = † i q
where
ms = sequentialize (φ ₀)
ns = sequentialize (φ ₁)
IH₁ : α ＝⟪ ms ⟫₀ β
IH₁ = ＝⟦⟧-implies-＝⟪⟫₀ α β (φ ₀) (ψ ₀)
IH₂ : α ＝⟪ ns ⟫₀ β
IH₂ = ＝⟦⟧-implies-＝⟪⟫₀ α β (φ ₁) (ψ ₁)
† : α ＝⟪ ms ++ ns ⟫₀ β
† = ＝⟪⟫-++-lemma₂ α β ms ns (IH₁ , IH₂)
\end{code}
\begin{code}
to-bool-congruence : (m n : ℕ)
→ (𝒷₁ : is-boolean-valued m)
→ (𝒷₂ : is-boolean-valued n)
→ m ＝ n
→ to-bool m 𝒷₁ ＝ to-bool n 𝒷₂
to-bool-congruence zero zero (inl refl) (inl refl) _ = refl
to-bool-congruence (succ zero) (succ zero) (inr refl) (inr refl) _ = refl
to-bool-congruence (succ (succ _)) (succ (succ _)) (inl ()) (inl _) _
to-bool-congruence (succ (succ _)) (succ (succ _)) (inl ()) (inr _) _
to-bool-congruence (succ (succ _)) (succ (succ _)) (inr ()) (inl _) _
to-bool-congruence (succ (succ _)) (succ (succ _)) (inr ()) (inr _) _
\end{code}
\begin{code}
to-cantor-＝⟦⟧ : {α₁ α₂ : Baire}
(ϑ₁ : is-boolean-point α₁) (ϑ₂ : is-boolean-point α₂)
(t : BT ℕ)
→ α₁ ＝⟦ t ⟧ α₂
→ to-cantor (α₁ , ϑ₁) ＝⟦ t ⟧ to-cantor (α₂ , ϑ₂)
to-cantor-＝⟦⟧ {α₁} {α₂} ϑ₁ ϑ₂ [] _ = []
to-cantor-＝⟦⟧ {α₁} {α₂} ϑ₁ ϑ₂ (n ∷ φ) (p ∷ ψ) = β ∷ γ
where
β : to-bool (α₁ n) (ϑ₁ n) ＝ to-bool (α₂ n) (ϑ₂ n)
β = to-bool-congruence (α₁ n) (α₂ n) (ϑ₁ n) (ϑ₂ n) p
γ : (b : 𝟚) → to-cantor (α₁ , ϑ₁) ＝⟦ φ b ⟧ to-cantor (α₂ , ϑ₂)
γ ₀ = to-cantor-＝⟦⟧ ϑ₁ ϑ₂ (φ ₀) (ψ ₀)
γ ₁ = to-cantor-＝⟦⟧ ϑ₁ ϑ₂ (φ ₁) (ψ ₁)
\end{code}
At this point, we are ready to prove one direction of the equivalence we are
interested in: `is-uniformly-continuous` implies `is-uniformly-continuous₀`.
\begin{code}
uni-continuity-implies-uni-continuity₀ : (f : Cantor → ℕ)
→ is-uniformly-continuous f
→ is-uniformly-continuous₀ f
uni-continuity-implies-uni-continuity₀ f 𝔠 =
n , λ (α₁ , ϑ₁) (α₂ , ϑ₂) → † α₁ α₂ ϑ₁ ϑ₂
where
t : BT ℕ
t = pr₁ 𝔠
n : ℕ
n = succ (maximumᵤ (pr₁ 𝔠))
f₀ : Cantor₀ → ℕ
f₀ = to-cantor₀-map f
† : (α₁ α₂ : Baire) (ϑ₁ : is-boolean-point α₁) (ϑ₂ : is-boolean-point α₂)
→ α₁ ＝⦅ n ⦆ α₂ → f₀ (α₁ , ϑ₁) ＝ f₀ (α₂ , ϑ₂)
† α₁ α₂ ϑ₁ ϑ₂ (p , q) = pr₂ 𝔠 (to-cantor (α₁ , ϑ₁)) (to-cantor (α₂ , ϑ₂)) η
where
ϝ : tl α₁ ＝⦅ maximumᵤ′ t ⦆ (tl α₂)
ϝ = transport
(λ - → tl α₁ ＝⦅ - ⦆ tl α₂)
(maximumᵤ′-equivalent-to-maximumᵤ t)
q
χ : α₁ ＝⦅ succ (maximum (sequentialize t)) ⦆ α₂
χ = p , ϝ
υ : α₁ ＝⟪ sequentialize t ⟫ α₂
υ = ＝⦅⦆-implies-＝⟪⟫ α₁ α₂ (sequentialize t) χ
ξ : α₁ ＝⟪ sequentialize t ⟫₀ α₂
ξ = ＝⟪⟫-implies-＝⟪⟫₀ α₁ α₂ (sequentialize t) υ
ζ : α₁ ＝⟦ t ⟧ α₂
ζ = ＝⟪⟫₀-implies-＝⟦⟧ α₁ α₂ t ξ
η : to-cantor (α₁ , ϑ₁) ＝⟦ t ⟧ to-cantor (α₂ , ϑ₂)
η = to-cantor-＝⟦⟧ ϑ₁ ϑ₂ t ζ
\end{code}
To prove the converse, we define an analogue of the range function for binary
trees that we call `rangeᵤ`. We also prove some small lemmas about this
function.
\begin{code}
singleton : ℕ → BT ℕ
singleton n = n ∷ λ { ₀ → [] ; ₁ → [] }
pred : ℕ → ℕ
pred zero = zero
pred (succ n) = n
rangeᵤ : (n : ℕ) → BT ℕ
rangeᵤ zero = singleton 0
rangeᵤ (succ n) = succ n ∷ λ { ₀ → [] ; ₁ → rangeᵤ n }
＝⟦⟧-up-to-rangeᵤ-m-implies-＝⟪⟫-up-to-range-m : {X : 𝓤₀ ̇} (α α′ : ℕ → X) (m : ℕ)
→ α ＝⟦ rangeᵤ m ⟧ α′
→ α ＝⟪ range m ⟫ α′
＝⟦⟧-up-to-rangeᵤ-m-implies-＝⟪⟫-up-to-range-m α α′ zero (p ∷ _) = p ∷ []
＝⟦⟧-up-to-rangeᵤ-m-implies-＝⟪⟫-up-to-range-m α α′ (succ m) (p ∷ q) = p ∷ IH
where
IH : α ＝⟪ range m ⟫ α′
IH = ＝⟦⟧-up-to-rangeᵤ-m-implies-＝⟪⟫-up-to-range-m α α′ m (q ₁)
＝⟦⟧-up-to-range-m-implies-＝⦅⦆-up-to-m : (α β : Baire) (m : ℕ)
→ α ＝⟦ rangeᵤ m ⟧ β
→ α ＝⦅ m ⦆ β
＝⟦⟧-up-to-range-m-implies-＝⦅⦆-up-to-m α β m = φ ∘ ψ
where
φ = ＝⟪⟫-range-implies-＝⦅⦆ α β m
ψ = ＝⟦⟧-up-to-rangeᵤ-m-implies-＝⟪⟫-up-to-range-m α β m
\end{code}
We prove one final lemma about the `embedding-C-B` function.
\begin{code}
＝⟦⟧-boolean-lemma : (α β : Cantor) (m : ℕ)
→ α ＝⟦ rangeᵤ m ⟧ β
→ embedding-C-B α ＝⟦ rangeᵤ m ⟧ embedding-C-B β
＝⟦⟧-boolean-lemma α β zero (p ∷ _) = ap embedding-𝟚-ℕ p ∷ (λ { ₀ → [] ; ₁ → [] })
＝⟦⟧-boolean-lemma α β (succ m) (p ∷ φ) =
ap embedding-𝟚-ℕ p ∷ λ { ₀ → [] ; ₁ → ＝⟦⟧-boolean-lemma α β m (φ ₁) }
\end{code}
We can now easily write down the proof that `is-uniformly-continuous` implies
`is-uniformly-continuous₀`.
\begin{code}
uni-continuity₀-implies-uni-continuity : (f : Cantor → ℕ)
→ is-uniformly-continuous₀ f
→ is-uniformly-continuous f
uni-continuity₀-implies-uni-continuity f ζ = rangeᵤ m , †
where
m : ℕ
m = modulus-atᵘ₀ f ζ
f₀ : Cantor₀ → ℕ
f₀ = to-cantor₀-map f
‡ : (α β : Baire) (𝒷₁ : is-boolean-point α) (𝒷₂ : is-boolean-point β)
→ α ＝⟦ rangeᵤ m ⟧ β → f₀ (α , 𝒷₁) ＝ f₀ (β , 𝒷₂)
‡ α β 𝒷₁ 𝒷₂ =
pr₂ ζ (α , 𝒷₁) (β , 𝒷₂) ∘ ＝⟦⟧-up-to-range-m-implies-＝⦅⦆-up-to-m α β m
† : (α β : Cantor) → α ＝⟦ rangeᵤ m ⟧ β → f α ＝ f β
† α β p = to-cantor₀-map-lemma f α β (‡ α′ β′ 𝒷₁ 𝒷₂ p′)
where
α′ : Baire
α′ = embedding-C-B α
𝒷₁ : (n : ℕ) → is-boolean-valued (α′ n)
𝒷₁ = to-baire-gives-boolean-point α
β′ : Baire
β′ = embedding-C-B β
𝒷₂ : (n : ℕ) → is-boolean-valued (β′ n)
𝒷₂ = to-baire-gives-boolean-point β
p′ : α′ ＝⟦ rangeᵤ m ⟧ β′
p′ = ＝⟦⟧-boolean-lemma α β m p
\end{code}
We finish by recording the equivalence of interest as a fact in itself.
\begin{code}
uni-continuity-equivalent-to-uni-continuity : (f : Cantor → ℕ)
→ is-uniformly-continuous₀ f
↔ is-uniformly-continuous f
uni-continuity-equivalent-to-uni-continuity f = ⦅⇒⦆ , ⦅⇐⦆
where
⦅⇒⦆ = uni-continuity₀-implies-uni-continuity f
⦅⇐⦆ = uni-continuity-implies-uni-continuity₀ f
\end{code}