Martin Escardo, 11th September 2018
Completed by Todd Waugh Ambridge, 15th May 2020
We begin by defining a "closeness function"
c : X → X → ℕ∞
such that
c x y ＝ ∞ ↔ x ＝ y
for some examples of types X, including Baire, Cantor and ℕ∞.
That is, two points are equal iff they are infinitely close. If we
have c x y ＝ under n for n : ℕ, the intuition is that x and y can be
distinguished by a finite amount of information of size n.
(An application is to show that WLPO holds iff ℕ∞ is discrete.)
We then discuss further codistance axioms.
\begin{code}
{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.FunExt
module TWA.Closeness (fe : FunExt) where
open import CoNaturals.Arithmetic fe
open import CoNaturals.Type renaming (min to min')
open import CoNaturals.UniversalProperty fe
open import MLTT.Two-Properties
open import Naturals.Sequence fe
open import Notation.CanonicalMap
open import Notation.Order
open import UF.DiscreteAndSeparated
module sequences
{𝓤 : Universe}
(D : 𝓤 ̇ )
(δ : is-discrete D)
where
\end{code}
We denote the type of sequences over D by $, and define a closeness
function $ → $ → ℕ∞ using the fact that ℕ∞ is the final coalgebra of
the functor 𝟙 + (-), which we refer to as corecursion.
\begin{code}
private
𝓢 : 𝓤 ̇
𝓢 = ℕ → D
X : 𝓤 ̇
X = 𝓢 × 𝓢
f : (α β : 𝓢) → head α ＝ head β → 𝟙 {𝓤₀} + X
f α β q = inr (tail α , tail β)
g : (α β : 𝓢) → head α ≠ head β → 𝟙 {𝓤₀} + X
g α β n = inl ⋆
p : X → 𝟙 {𝓤₀} + X
p (α , β) = cases (f α β) (g α β) (δ (head α) (head β))
c : 𝓢 → 𝓢 → ℕ∞
c = curry (ℕ∞-corec p)
\end{code}
We use the private name "c" in this submodule, which is exported as
"closeness":
\begin{code}
closeness : 𝓢 → 𝓢 → ℕ∞
closeness = c
\end{code}
The two defining properties of the function c are the following:
\begin{code}
closeness-eq₀ : (α β : 𝓢) → head α ≠ head β
→ c α β ＝ Zero
closeness-eq₁ : (α β : 𝓢) → head α ＝ head β
→ c α β ＝ Succ (c (tail α) (tail β))
closeness-eq₀ α β n = γ r
where
t : δ (head α) (head β) ＝ inr n
t = discrete-inr (fe 𝓤 𝓤₀) δ (head α) (head β) n
r : p (α , β) ＝ inl ⋆
r = ap (cases (f α β) (g α β)) t
γ : p (α , β) ＝ inl ⋆ → c α β ＝ Zero
γ = Coalg-morphism-Zero p (α , β) ⋆
closeness-eq₁ α β q = γ r
where
t : δ (head α) (head β) ＝ inl q
t = discrete-inl δ (head α) (head β) q
r : p (α , β) ＝ inr (tail α , tail β)
r = ap (cases (f α β) (g α β)) t
γ : p (α , β) ＝ inr (tail α , tail β)
→ c α β ＝ Succ (c (tail α) (tail β))
γ = Coalg-morphism-Succ p (α , β) (tail α , tail β)
\end{code}
That any sequence is infinitely close to itself is proved by
coinduction on ℕ∞ using closeness-eq₁:
\begin{code}
infinitely-close-to-itself : (α : 𝓢) → c α α ＝ ∞
infinitely-close-to-itself α = ℕ∞-coinduction R b (c α α) ∞ γ
where
l : ∀ α → c α α ＝ Succ (c (tail α) (tail α))
l α = closeness-eq₁ α α refl
R : ℕ∞ → ℕ∞ → 𝓤 ̇
R u v = (Σ α ꞉ 𝓢 , u ＝ c α α) × (v ＝ ∞)
b : ℕ∞-bisimulation R
b .(c α α) .∞ ((α , refl) , refl) = s , t , Pred-∞-is-∞
where
s : positivity (c α α) ＝ positivity ∞
s = ap positivity (l α)
t : Σ α' ꞉ 𝓢 , Pred (c α α) ＝ c α' α'
t = tail α , (ap Pred (l α) ∙ Pred-Succ)
γ : R (c α α) ∞
γ = (α , refl) , refl
\end{code}
That any two infinitely close sequences are equal is proved by
coinduction on sequences, using both closeness-eq₀ (to rule out an
impossible case) and closeness-eq₁ (to establish the result):
\begin{code}
infinitely-close-are-equal : (α β : 𝓢) → c α β ＝ ∞ → α ＝ β
infinitely-close-are-equal = seq-coinduction (λ α β → c α β ＝ ∞) b
where
b : (α β : 𝓢) → c α β ＝ ∞
→ (head α ＝ head β) × (c (tail α) (tail β) ＝ ∞)
b α β q = d , e
where
l : head α ≠ head β → c α β ＝ Zero
l = closeness-eq₀ α β
d : head α ＝ head β
d = Cases (δ (head α) (head β))
(λ (p : head α ＝ head β)
→ p)
(λ (n : head α ≠ head β)
→ 𝟘-elim (Zero-not-Succ (Zero ＝⟨ (l n)⁻¹ ⟩
c α β ＝⟨ q ⟩
∞ ＝⟨ (Succ-∞-is-∞ (fe 𝓤₀ 𝓤₀))⁻¹ ⟩
Succ ∞ ∎)))
e : c (tail α) (tail β) ＝ ∞
e = ap Pred (Succ (c (tail α) (tail β)) ＝⟨ (closeness-eq₁ α β d)⁻¹ ⟩
c α β ＝⟨ q ⟩
∞ ∎)
\end{code}
Symmetric property:
\begin{code}
symmetric-property : (α β : 𝓢) → c α β ＝ c β α
symmetric-property α β = ℕ∞-coinduction R b (c α β) (c β α) γ
where
R : ℕ∞ → ℕ∞ → 𝓤 ̇
R u v = Σ \α → Σ \β → (u ＝ c α β) × (v ＝ c β α)
b : ℕ∞-bisimulation R
b .(c α β) .(c β α) (α , β , refl , refl)
= s , t (δ (head α) (head β))
where
s : positivity (c α β) ＝ positivity (c β α)
s = Cases (δ (head α) (head β)) sₕ sₜ
where
sₕ : head α ＝ head β → positivity (c α β) ＝ positivity (c β α)
sₕ p = successors-same-positivity
(closeness-eq₁ α β p)
(closeness-eq₁ β α (p ⁻¹))
sₜ : head α ≠ head β → positivity (c α β) ＝ positivity (c β α)
sₜ d = ap positivity
(closeness-eq₀ α β d
∙ closeness-eq₀ β α (λ p → d (p ⁻¹)) ⁻¹)
t : (head α ＝ head β) + (head α ≠ head β)
→ R (Pred (c α β)) (Pred (c β α))
t (inl p) = tail α , tail β
, ap Pred (closeness-eq₁ α β p ∙ Pred-Succ)
, ap Pred (closeness-eq₁ β α (p ⁻¹) ∙ Pred-Succ)
t (inr d) = α , β
, Pred-Zero-is-Zero' (c α β) (closeness-eq₀ α β d)
, Pred-Zero-is-Zero' (c β α) (closeness-eq₀ β α (λ p → d (p ⁻¹)))
γ : R (c α β) (c β α)
γ = α , β , refl , refl
\end{code}
Ultra property:
\begin{code}
closeness-eq₁' : (α β : 𝓢) → is-positive (c α β)
→ head α ＝ head β
closeness-eq₁' α β p = Cases (δ (head α) (head β)) id
(λ h≠ → 𝟘-elim (zero-is-not-one
(is-Zero-Zero ⁻¹ ∙ ap (λ - → ι - 0) (closeness-eq₀ α β h≠ ⁻¹) ∙ p)))
open import Naturals.Order
closeness-conceptually₁ : (α β : 𝓢) (n : ℕ)
→ ((k : ℕ) → k ≤ n → α k ＝ β k)
→ n ⊏ c α β
closeness-conceptually₁ α β zero α≈ₙβ
= transport (0 ⊏_) (closeness-eq₁ α β (α≈ₙβ 0 ⋆) ⁻¹)
(is-positive-Succ (c (tail α) (tail β)))
closeness-conceptually₁ α β (succ n) α≈ₙβ
= transport (succ n ⊏_) (closeness-eq₁ α β (α≈ₙβ 0 ⋆) ⁻¹)
(closeness-conceptually₁ (tail α) (tail β) n (λ m → α≈ₙβ (succ m)))
closeness-conceptually₂ : (α β : 𝓢) (n : ℕ)
→ n ⊏ c α β
→ ((k : ℕ) → k ≤ n → α k ＝ β k)
closeness-conceptually₂ α β n ⊏ₙcαβ zero k≤n
= closeness-eq₁' α β (⊏-trans'' (c α β) n 0 k≤n ⊏ₙcαβ)
closeness-conceptually₂ α β n ⊏ₙcαβ (succ k) k≤n
= closeness-conceptually₂ (tail α) (tail β) k (transport (succ k ⊏_)
(closeness-eq₁ α β (closeness-eq₁' α β (⊏-trans'' (c α β) n 0 ⋆ ⊏ₙcαβ)))
(⊏-trans'' (c α β) n (succ k) k≤n ⊏ₙcαβ))
k (≤-refl k)
min-split : (α β : ℕ∞) (n : ℕ) → n ⊏ uncurry min' (α , β) → n ⊏ α × n ⊏ β
pr₁ (min-split α β n min≼) = different-from-₀-equal-₁
(λ x → zero-is-not-one (Lemma[min𝟚ab＝₀] (inl x) ⁻¹ ∙ min≼))
pr₂ (min-split α β n min≼) = different-from-₀-equal-₁
(λ x → zero-is-not-one (Lemma[min𝟚ab＝₀] (inr x) ⁻¹ ∙ min≼))
ultra-property : (α β ε : 𝓢) → min (c α β , c β ε) ≼ c α ε
ultra-property α β ε n min≼ = closeness-conceptually₁ α ε n
(λ k k≤n → closeness-conceptually₂ α β n (pr₁ min-split') k k≤n
∙ closeness-conceptually₂ β ε n (pr₂ min-split') k k≤n)
where
min-split' : n ⊏ c α β × n ⊏ c β ε
min-split' = min-split (c α β) (c β ε) n
(transport (λ - → n ⊏ - (c α β , c β ε)) min＝ min≼)
\end{code}
We now consider the following two special cases for the Baire and
Cantor types:
\begin{code}
open sequences ℕ ℕ-is-discrete
renaming
(closeness to Baire-closeness ;
infinitely-close-to-itself to Baire-infinitely-close-to-itself ;
infinitely-close-are-equal to Baire-infinitely-close-are-equal ;
symmetric-property to Baire-symmetric-property ;
ultra-property to Baire-ultra-property )
open sequences 𝟚 𝟚-is-discrete
renaming
(closeness to Cantor-closeness ;
infinitely-close-to-itself to Cantor-infinitely-close-to-itself ;
infinitely-close-are-equal to Cantor-infinitely-close-are-equal ;
symmetric-property to Cantor-symmetric-property ;
ultra-property to Cantor-ultra-property )
\end{code}
And now we reduce the closeness of the Cantor type to the generic
convergent sequence:
\begin{code}
ℕ∞-closeness : ℕ∞ → ℕ∞ → ℕ∞
ℕ∞-closeness u v = Cantor-closeness (ι u) (ι v)
ℕ∞-infinitely-close-to-itself : (u : ℕ∞) → ℕ∞-closeness u u ＝ ∞
ℕ∞-infinitely-close-to-itself u = Cantor-infinitely-close-to-itself (ι u)
ℕ∞-equal-are-infinitely-close : (u v : ℕ∞) → u ＝ v → ℕ∞-closeness u v ＝ ∞
ℕ∞-equal-are-infinitely-close u .u refl = ℕ∞-infinitely-close-to-itself u
ℕ∞-infinitely-close-are-equal : (u v : ℕ∞) → ℕ∞-closeness u v ＝ ∞ → u ＝ v
ℕ∞-infinitely-close-are-equal u v r = ℕ∞-to-ℕ→𝟚-lc (fe 𝓤₀ 𝓤₀) γ
where
γ : ι u ＝ ι v
γ = Cantor-infinitely-close-are-equal (ι u) (ι v) r
ℕ∞-symmetric-property : (u v : ℕ∞) → ℕ∞-closeness u v ＝ ℕ∞-closeness v u
ℕ∞-symmetric-property u v = Cantor-symmetric-property (ι u) (ι v)
ℕ∞-ultra-property : (u v w : ℕ∞)
→ min (ℕ∞-closeness u v , ℕ∞-closeness v w) ≼ ℕ∞-closeness u w
ℕ∞-ultra-property u v w = Cantor-ultra-property (ι u) (ι v) (ι w)
\end{code}
Axioms for closeness:
\begin{code}
is-closeness
indistinguishable-are-equal
self-indistinguishable
is-symmetric
is-ultra
: {X : 𝓤 ̇ } → (X → X → ℕ∞) → 𝓤 ̇
indistinguishable-are-equal c = ∀ x y → c x y ＝ ∞ → x ＝ y
self-indistinguishable c = ∀ x → c x x ＝ ∞
is-symmetric c = ∀ x y → c x y ＝ c y x
is-ultra c = ∀ x y z → min (c x y , c y z) ≼ c x z
is-closeness c = indistinguishable-are-equal c
× self-indistinguishable c
× is-symmetric c
× is-ultra c
\end{code}
The above closenesss are indeed closenesss according
to this definition
\begin{code}
open sequences
ℕ→D-has-closeness : (X : 𝓤 ̇ ) (δ : is-discrete X)
→ is-closeness (closeness X δ)
ℕ→D-has-closeness X δ
= infinitely-close-are-equal X δ
, infinitely-close-to-itself X δ
, symmetric-property X δ
, ultra-property X δ
ℕ→ℕ-has-closeness : is-closeness (Baire-closeness)
ℕ→ℕ-has-closeness = ℕ→D-has-closeness ℕ ℕ-is-discrete
ℕ→𝟚-has-closeness : is-closeness (Cantor-closeness)
ℕ→𝟚-has-closeness = ℕ→D-has-closeness 𝟚 𝟚-is-discrete
ℕ→ℕ∞-has-closeness : is-closeness (ℕ∞-closeness)
ℕ→ℕ∞-has-closeness = ℕ∞-infinitely-close-are-equal
, ℕ∞-infinitely-close-to-itself
, ℕ∞-symmetric-property
, ℕ∞-ultra-property