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