ClosenessSpaces-Examples
Todd Waugh Ambridge, January 2024 # Examples of closeness spaces{-# OPTIONS --without-K --safe #-} open import MLTT.Spartan open import CoNaturals.Type renaming (ℕ-to-ℕ∞ to _↑) hiding (max) open import Notation.Order open import Naturals.Order open import NotionsOfDecidability.Complemented open import UF.DiscreteAndSeparated open import UF.FunExt open import UF.Subsingletons open import UF.Embeddings open import MLTT.Two-Properties open import Fin.Type open import Fin.Bishop open import Fin.Embeddings open import UF.Equiv open import MLTT.SpartanList hiding (⟨_⟩; _∷_) module TWA.Thesis.Chapter3.ClosenessSpaces-Examples (fe : FunExt) where open import TWA.Thesis.Chapter2.Sequences open import TWA.Thesis.Chapter2.Vectors open import TWA.Thesis.Chapter2.Finite open import TWA.Thesis.Chapter3.ClosenessSpaces fe open import TWA.Closeness fe hiding (is-ultra; is-closeness)## Trivial closeness spaces𝟘-clospace : is-closeness-space (𝟘 {𝓤}) 𝟘-clospace = (λ ()) , ((λ ()) , (λ ()) , ((λ ()) , (λ ()))) 𝟙-clospace : is-closeness-space (𝟙 {𝓤}) 𝟙-clospace = (λ _ _ → ∞) , (λ _ _ _ → refl) , (λ _ → refl) , (λ _ _ → refl) , (λ _ _ _ _ _ → refl)## Discrete closeness spacesdiscrete-clofun'' : {X : 𝓤 ̇ } (x y : X) → is-decidable (x ＝ y) → ℕ∞ discrete-clofun'' x y (inl _) = ∞ discrete-clofun'' x y (inr _) = 0 ↑ discrete-clofun' : {X : 𝓤 ̇ } → is-discrete X → X → X → ℕ∞ discrete-clofun' d x y = discrete-clofun'' x y (d x y) discrete-clofun''-e : {X : 𝓤 ̇ } (x y : X) → (d : is-decidable (x ＝ y)) → discrete-clofun'' x y d ＝ ∞ → x ＝ y discrete-clofun''-e x y (inl e) cxy＝∞ = e discrete-clofun''-e x y (inr f) cxy＝∞ = 𝟘-elim (zero-is-not-one (ap (λ - → ℕ∞-to-ℕ→𝟚 - 0) cxy＝∞)) discrete-clofun''-i : {X : 𝓤 ̇ } (x : X) → (d : is-decidable (x ＝ x)) → discrete-clofun'' x x d ＝ ∞ discrete-clofun''-i x (inl _) = refl discrete-clofun''-i x (inr f) = 𝟘-elim (f refl) discrete-clofun''-s : {X : 𝓤 ̇ } (x y : X) → (d : is-decidable (x ＝ y)) → (d' : is-decidable (y ＝ x)) → discrete-clofun'' x y d ＝ discrete-clofun'' y x d' discrete-clofun''-s x y (inl _) (inl _) = refl discrete-clofun''-s x y (inr _) (inr _) = refl discrete-clofun''-s x y (inl e) (inr f) = 𝟘-elim (f (e ⁻¹)) discrete-clofun''-s x y (inr f) (inl e) = 𝟘-elim (f (e ⁻¹)) discrete-clofun''-u : {X : 𝓤 ̇ } (x y z : X) → (d : is-decidable (x ＝ y)) → (d' : is-decidable (y ＝ z)) → (d'' : is-decidable (x ＝ z)) → min (discrete-clofun'' x y d ) (discrete-clofun'' y z d' ) ≼ discrete-clofun'' x z d'' discrete-clofun''-u x y z _ _ (inl _) _ _ = refl discrete-clofun''-u x y z (inl _) (inr _) (inr _) _ = id discrete-clofun''-u x y z (inr _) _ (inr _) _ = id discrete-clofun''-u x x x (inl refl) (inl refl) (inr f) = 𝟘-elim (f refl) discrete-clofun'-is-clofun : {X : 𝓤 ̇ } (d : is-discrete X) → is-closeness (discrete-clofun' d) discrete-clofun'-is-clofun d = (λ x y → discrete-clofun''-e x y (d x y)) , (λ x → discrete-clofun''-i x (d x x)) , (λ x y → discrete-clofun''-s x y (d x y) (d y x)) , (λ x y z → discrete-clofun''-u x y z (d x y) (d y z) (d x z)) discrete-clospace : {X : 𝓤 ̇ } (d : is-discrete X) → is-closeness-space X discrete-clospace d = discrete-clofun' d , discrete-clofun'-is-clofun d D-ClosenessSpace : {X : 𝓤 ̇ } → is-discrete X → ClosenessSpace 𝓤 D-ClosenessSpace {𝓤} {X} d = X , discrete-clospace d finite-totally-bounded : {X : 𝓤 ̇ } (f : finite-linear-order X) (d : is-discrete X) → pointed X → totally-bounded (D-ClosenessSpace d) 𝓤 finite-totally-bounded f d x 0 = pointed-has-a-0-net (D-ClosenessSpace d) x finite-totally-bounded {𝓤} {X} f d x (succ ε) = X , (id , id , η) , f where η : (x : X) → C (D-ClosenessSpace d) (succ ε) x x η x n _ = ap (λ - → ℕ∞-to-ℕ→𝟚 - n) (i⟨ D-ClosenessSpace d ⟩ x) discrete-apart-implies-closeness-0 : {X : 𝓤 ̇ } → (d : is-discrete X) → (x y : X) → x ≠ y → c⟨ D-ClosenessSpace d ⟩ x y ＝ 0 ↑ discrete-apart-implies-closeness-0 d x y f = γ (d x y) where γ : (dxy : is-decidable (x ＝ y)) → discrete-clofun'' x y dxy ＝ Zero γ (inl e) = 𝟘-elim (f e) γ (inr _) = refl discrete-closeness-succ-implies-equal : {X : 𝓤 ̇ } → (d : is-discrete X) → (x y : X) → (n : ℕ) → C (D-ClosenessSpace d) (succ n) x y → x ＝ y discrete-closeness-succ-implies-equal d x y n Csnxy = γ (d x y) (Csnxy n (<-gives-⊏ n (succ n) (<-succ n))) where γ : (dxy : is-decidable (x ＝ y)) → ℕ∞-to-ℕ→𝟚 (discrete-clofun'' x y dxy) n ＝ ₁ → x ＝ y γ (inl e) _ = e γ (inr f) cxyₙ=₁ = 𝟘-elim (zero-is-not-one cxyₙ=₁)## Disjoint union of closeness spaces+-clofun' : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → (⟨ X ⟩ + ⟨ Y ⟩ → ⟨ X ⟩ + ⟨ Y ⟩ → ℕ∞) +-clofun' X Y (inl x₁) (inl x₂) = c⟨ X ⟩ x₁ x₂ +-clofun' X Y (inr y₁) (inr y₂) = c⟨ Y ⟩ y₁ y₂ +-clofun' X Y (inl x₁) (inr y₂) = 0 ↑ +-clofun' X Y (inr y₁) (inl x₂) = 0 ↑ +-clofun'-e : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → indistinguishable-are-equal (+-clofun' X Y) +-clofun'-e X Y (inl x₁) (inl x₂) q = ap inl (e⟨ X ⟩ x₁ x₂ q) +-clofun'-e X Y (inr y₁) (inr y₂) q = ap inr (e⟨ Y ⟩ y₁ y₂ q) +-clofun'-e X Y (inl x₁) (inr y₂) f = 𝟘-elim (zero-is-not-one (ap (λ - → ℕ∞-to-ℕ→𝟚 - 0) f)) +-clofun'-e X Y (inr y₁) (inl x₂) f = 𝟘-elim (zero-is-not-one (ap (λ - → ℕ∞-to-ℕ→𝟚 - 0) f)) +-clofun'-i : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → self-indistinguishable (+-clofun' X Y) +-clofun'-i X Y (inl x) = i⟨ X ⟩ x +-clofun'-i X Y (inr y) = i⟨ Y ⟩ y +-clofun'-s : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → is-symmetric (+-clofun' X Y) +-clofun'-s X Y (inl x₁) (inl x₂) = s⟨ X ⟩ x₁ x₂ +-clofun'-s X Y (inr y₁) (inr y₂) = s⟨ Y ⟩ y₁ y₂ +-clofun'-s X Y (inl x₁) (inr y₂) = refl +-clofun'-s X Y (inr y₁) (inl x₂) = refl +-clofun'-u : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → is-ultra (+-clofun' X Y) +-clofun'-u X Y (inl x₁) (inl x₂) (inl x₃) = u⟨ X ⟩ x₁ x₂ x₃ +-clofun'-u X Y (inr y₁) (inr y₂) (inr y₃) = u⟨ Y ⟩ y₁ y₂ y₃ +-clofun'-u X Y (inl x₁) (inl x₂) (inr y₃) n mina₀＝₁ = Lemma[min𝟚ab＝₀] (inr refl) ⁻¹ ∙ mina₀＝₁ +-clofun'-u X Y (inr y₁) (inr y₂) (inl x₃) n mina₀＝₁ = Lemma[min𝟚ab＝₀] (inr refl) ⁻¹ ∙ mina₀＝₁ +-clofun'-u X Y (inl x₁) (inr y₂) _ _ () +-clofun'-u X Y (inr y₁) (inl x₂) _ _ () +-clofun'-is-clofun : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → is-closeness (+-clofun' X Y) +-clofun'-is-clofun X Y = +-clofun'-e X Y , +-clofun'-i X Y , +-clofun'-s X Y , +-clofun'-u X Y +-clospace : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → is-closeness-space (⟨ X ⟩ + ⟨ Y ⟩) +-clospace X Y = +-clofun' X Y , +-clofun'-is-clofun X Y +-ClosenessSpace : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → ClosenessSpace (𝓤 ⊔ 𝓥) +-ClosenessSpace X Y = (⟨ X ⟩ + ⟨ Y ⟩) , +-clospace X Y +-preserves-nets : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → (ε : ℕ) → (X' : 𝓤' ̇ ) (Y' : 𝓥' ̇ ) → X' is ε net-of X → Y' is ε net-of Y → (X' + Y') is ε net-of (+-ClosenessSpace X Y) +-preserves-nets X Y ε X' Y' ((gx , hx , ηx) , fx) ((gy , hy , ηy) , fy) = (g , h , η) , f where g : X' + Y' → ⟨ X ⟩ + ⟨ Y ⟩ g (inl x') = inl (gx x') g (inr y') = inr (gy y') h : ⟨ X ⟩ + ⟨ Y ⟩ → X' + Y' h (inl x ) = inl (hx x) h (inr y ) = inr (hy y) η : (x : ⟨ X ⟩ + ⟨ Y ⟩) → C (+-ClosenessSpace X Y) ε x (g (h x)) η (inl x ) = ηx x η (inr y ) = ηy y f : finite-linear-order (X' + Y') f = +-is-finite fx fy +-totally-bounded : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → totally-bounded X 𝓤' → totally-bounded Y 𝓥' → totally-bounded (+-ClosenessSpace X Y) (𝓤' ⊔ 𝓥') +-totally-bounded X Y tx ty ε = (X' + Y') , (+-preserves-nets X Y ε X' Y' X'-is-ε-net Y'-is-ε-net) where X' = pr₁ (tx ε) Y' = pr₁ (ty ε) X'-is-ε-net = pr₂ (tx ε) Y'-is-ε-net = pr₂ (ty ε) +-C-left : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → (x₁ x₂ : ⟨ X ⟩) → (ε : ℕ) → C (+-ClosenessSpace X Y) ε (inl x₁) (inl x₂) → C X ε x₁ x₂ +-C-left X Y x₁ x₂ ε Cxy n = Cxy n## Binary product of closeness spaces×-clofun' : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → (⟨ X ⟩ × ⟨ Y ⟩ → ⟨ X ⟩ × ⟨ Y ⟩ → ℕ∞) ×-clofun' X Y (x₁ , y₁) (x₂ , y₂) = min (c⟨ X ⟩ x₁ x₂) (c⟨ Y ⟩ y₁ y₂) min-∞-l : (u v : ℕ∞) → min u v ＝ ∞ → u ＝ ∞ min-∞-l u v min＝∞ = to-subtype-＝ (being-decreasing-is-prop (fe _ _)) (dfunext (fe _ _) (λ i → Lemma[min𝟚ab＝₁→a＝₁] (ap (λ - → ℕ∞-to-ℕ→𝟚 - i) min＝∞))) min-∞-r : (u v : ℕ∞) → min u v ＝ ∞ → v ＝ ∞ min-∞-r u v min＝∞ = to-subtype-＝ (being-decreasing-is-prop (fe _ _)) (dfunext (fe _ _) (λ i → Lemma[min𝟚ab＝₁→b＝₁] (ap (λ - → ℕ∞-to-ℕ→𝟚 - i) min＝∞))) ×-clofun'-e : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → indistinguishable-are-equal (×-clofun' X Y) ×-clofun'-e X Y (x₁ , y₁) (x₂ , y₂) cxy＝∞ = ap (_, y₁) (e⟨ X ⟩ x₁ x₂ cx＝∞) ∙ ap (x₂ ,_) (e⟨ Y ⟩ y₁ y₂ cy＝∞) where cx＝∞ : c⟨ X ⟩ x₁ x₂ ＝ ∞ cx＝∞ = min-∞-l (c⟨ X ⟩ x₁ x₂) (c⟨ Y ⟩ y₁ y₂) cxy＝∞ cy＝∞ : c⟨ Y ⟩ y₁ y₂ ＝ ∞ cy＝∞ = min-∞-r (c⟨ X ⟩ x₁ x₂) (c⟨ Y ⟩ y₁ y₂) cxy＝∞ ×-clofun'-i : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → self-indistinguishable (×-clofun' X Y) ×-clofun'-i X Y (x , y) = ap (λ - → min - (c⟨ Y ⟩ y y)) (i⟨ X ⟩ x) ∙ ap ( min ∞ ) (i⟨ Y ⟩ y) ×-clofun'-s : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → is-symmetric (×-clofun' X Y) ×-clofun'-s X Y (x₁ , y₁) (x₂ , y₂) = ap (λ - → min - (c⟨ Y ⟩ y₁ y₂)) (s⟨ X ⟩ x₁ x₂) ∙ ap ( min (c⟨ X ⟩ x₂ x₁) ) (s⟨ Y ⟩ y₁ y₂) min𝟚-abcd : {a b c d : 𝟚} → a ＝ c → b ＝ d → min𝟚 a b ＝ min𝟚 c d min𝟚-abcd {a} {b} {.a} {.b} refl refl = refl min𝟚-abcd-ac : (a b c d : 𝟚) → min𝟚 (min𝟚 a b) (min𝟚 c d) ＝ ₁ → min𝟚 a c ＝ ₁ min𝟚-abcd-ac ₁ ₁ ₁ ₁ e = refl min𝟚-abcd-bd : (a b c d : 𝟚) → min𝟚 (min𝟚 a b) (min𝟚 c d) ＝ ₁ → min𝟚 b d ＝ ₁ min𝟚-abcd-bd ₁ ₁ ₁ ₁ e = refl minℕ∞-abcdef : (a b c d e f : ℕ∞) → min a b ≼ e → min c d ≼ f → min (min a c) (min b d) ≼ min e f minℕ∞-abcdef a b c d e f mab≼e mcd≼f n minabcd＝₁ = Lemma[a＝₁→b＝₁→min𝟚ab＝₁] (mab≼e n (min𝟚-abcd-ac (ℕ∞-to-ℕ→𝟚 a n) (ℕ∞-to-ℕ→𝟚 c n) (ℕ∞-to-ℕ→𝟚 b n) (ℕ∞-to-ℕ→𝟚 d n) minabcd＝₁)) (mcd≼f n (min𝟚-abcd-bd (ℕ∞-to-ℕ→𝟚 a n) (ℕ∞-to-ℕ→𝟚 c n) (ℕ∞-to-ℕ→𝟚 b n) (ℕ∞-to-ℕ→𝟚 d n) minabcd＝₁)) ×-clofun'-u : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → is-ultra (×-clofun' X Y) ×-clofun'-u X Y (x₁ , y₁) (x₂ , y₂) (x₃ , y₃) = minℕ∞-abcdef (c⟨ X ⟩ x₁ x₂) (c⟨ X ⟩ x₂ x₃) (c⟨ Y ⟩ y₁ y₂) (c⟨ Y ⟩ y₂ y₃) (c⟨ X ⟩ x₁ x₃) (c⟨ Y ⟩ y₁ y₃) (u⟨ X ⟩ x₁ x₂ x₃) (u⟨ Y ⟩ y₁ y₂ y₃) ×-clofun'-is-clofun : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → is-closeness (×-clofun' X Y) ×-clofun'-is-clofun X Y = ×-clofun'-e X Y , ×-clofun'-i X Y , ×-clofun'-s X Y , ×-clofun'-u X Y ×-clospace : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → is-closeness-space (⟨ X ⟩ × ⟨ Y ⟩) ×-clospace X Y = ×-clofun' X Y , ×-clofun'-is-clofun X Y ×-ClosenessSpace : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → ClosenessSpace (𝓤 ⊔ 𝓥) ×-ClosenessSpace X Y = (⟨ X ⟩ × ⟨ Y ⟩) , (×-clospace X Y) ×-C-left : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → (x₁ x₂ : ⟨ X ⟩) (y₁ y₂ : ⟨ Y ⟩) → (ε : ℕ) → C (×-ClosenessSpace X Y) ε (x₁ , y₁) (x₂ , y₂) → C X ε x₁ x₂ ×-C-left X Y x₁ x₂ y₁ y₂ ε Cxy n = Lemma[min𝟚ab＝₁→a＝₁] ∘ (Cxy n) ×-C-right : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → (x₁ x₂ : ⟨ X ⟩) (y₁ y₂ : ⟨ Y ⟩) → (ε : ℕ) → C (×-ClosenessSpace X Y) ε (x₁ , y₁) (x₂ , y₂) → C Y ε y₁ y₂ ×-C-right X Y x₁ x₂ y₁ y₂ ε Cxy n = Lemma[min𝟚ab＝₁→b＝₁] ∘ (Cxy n) ×-C-combine : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → (x₁ x₂ : ⟨ X ⟩) (y₁ y₂ : ⟨ Y ⟩) → (ε : ℕ) → C X ε x₁ x₂ → C Y ε y₁ y₂ → C (×-ClosenessSpace X Y) ε (x₁ , y₁) (x₂ , y₂) ×-C-combine X Y x₁ x₂ y₁ y₂ ε Cεx₁x₂ Cεy₁y₂ n n⊏ε = Lemma[a＝₁→b＝₁→min𝟚ab＝₁] (Cεx₁x₂ n n⊏ε) (Cεy₁y₂ n n⊏ε) ×-preserves-nets : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → (ε : ℕ) → (X' : 𝓤' ̇ ) (Y' : 𝓥' ̇ ) → X' is ε net-of X → Y' is ε net-of Y → (X' × Y') is ε net-of (×-ClosenessSpace X Y) ×-preserves-nets X Y ε X' Y' ((gx , hx , ηx) , fx) ((gy , hy , ηy) , fy) = (g , h , η) , f where g : X' × Y' → ⟨ X ⟩ × ⟨ Y ⟩ g (x' , y') = gx x' , gy y' h : ⟨ X ⟩ × ⟨ Y ⟩ → X' × Y' h (x , y ) = hx x , hy y η : (x : ⟨ X ⟩ × ⟨ Y ⟩) → C (×-ClosenessSpace X Y) ε x (g (h x)) η (x , y ) = ×-C-combine X Y x (gx (hx x)) y (gy (hy y)) ε (ηx x) (ηy y) f : finite-linear-order (X' × Y') f = ×-is-finite fx fy ×-totally-bounded : (X : ClosenessSpace 𝓤) (Y : ClosenessSpace 𝓥) → totally-bounded X 𝓤' → totally-bounded Y 𝓥' → totally-bounded (×-ClosenessSpace X Y) (𝓤' ⊔ 𝓥') ×-totally-bounded X Y tx ty ε = (X' × Y') , (×-preserves-nets X Y ε X' Y' X'-is-ε-net Y'-is-ε-net) where X' = pr₁ (tx ε) Y' = pr₁ (ty ε) X'-is-ε-net = pr₂ (tx ε) Y'-is-ε-net = pr₂ (ty ε)## Vector closeness spacesvec-ClosenessSpace : (n : ℕ) (X : Fin n → ClosenessSpace 𝓤) → ClosenessSpace 𝓤 vec-clospace : (n : ℕ) (X : Fin n → ClosenessSpace 𝓤) → is-closeness-space (vec n (⟨_⟩ ∘ X)) vec-ClosenessSpace n X = (vec n (⟨_⟩ ∘ X)) , vec-clospace n X vec-clospace 0 X = (λ _ _ → ∞) , e , i , s , u where e : indistinguishable-are-equal (λ _ _ → ∞) e ⟨⟩ ⟨⟩ _ = refl i : self-indistinguishable (λ _ _ → ∞) i ⟨⟩ = refl s : is-symmetric (λ _ _ → ∞) s ⟨⟩ ⟨⟩ = refl u : is-ultra (λ _ _ → ∞) u ⟨⟩ ⟨⟩ ⟨⟩ _ _ = refl vec-clospace (succ n) X = ×-clospace (X 𝟎) (vec-ClosenessSpace n (X ∘ suc)) vec-totally-bounded : (n : ℕ) (X : Fin n → ClosenessSpace 𝓤) → ((i : Fin n) → totally-bounded (X i) 𝓥) → totally-bounded (vec-ClosenessSpace n X) 𝓥 vec-totally-bounded 0 X t ϵ = 𝟙 , ((g , h , η) , 𝟙-is-finite) where g : 𝟙 → vec 0 (⟨_⟩ ∘ X) g _ = ⟨⟩ h : vec 0 (⟨_⟩ ∘ X) → 𝟙 h _ = ⋆ η : (x : vec 0 (⟨_⟩ ∘ X)) → C (vec-ClosenessSpace 0 X) ϵ x ⟨⟩ η ⟨⟩ = C-refl (vec-ClosenessSpace 0 X) ϵ ⟨⟩ vec-totally-bounded (succ n) X t = ×-totally-bounded (X 𝟎) (vec-ClosenessSpace n (X ∘ suc)) (t 𝟎) (vec-totally-bounded n (X ∘ suc) (t ∘ suc)) Vec-clospace : (X : ClosenessSpace 𝓤) (n : ℕ) → is-closeness-space (Vec ⟨ X ⟩ n) Vec-clospace X n = vec-clospace n (λ _ → X) Vec-ClosenessSpace : (X : ClosenessSpace 𝓤) (n : ℕ) → ClosenessSpace 𝓤 Vec-ClosenessSpace X n = Vec ⟨ X ⟩ n , Vec-clospace X n Vec-totally-bounded : (X : ClosenessSpace 𝓤) (n : ℕ) → totally-bounded X 𝓥 → totally-bounded (Vec-ClosenessSpace X n) 𝓥 Vec-totally-bounded X n t = vec-totally-bounded n (λ _ → X) (λ _ → t)## Least closeness pseudocloseness spaceLeast-clofun : (X : 𝓤 ̇ ) (Y : ClosenessSpace 𝓥) → {n : ℕ} → Vec X n → ((X → ⟨ Y ⟩) → (X → ⟨ Y ⟩) → ℕ∞) Least-clofun X Y {n} v f g = pr₁ (Vec-clospace Y n) (vec-map f v) (vec-map g v) Least-clofun-is-psclofun : (X : 𝓤 ̇ ) (Y : ClosenessSpace 𝓥) → {n : ℕ} → (v : Vec X n) → is-pseudocloseness (Least-clofun X Y v) Least-clofun-is-psclofun X Y {n} v = (λ f → pr₁ (pr₂ γ) (vec-map f v)) , (λ f g → pr₁ (pr₂ (pr₂ γ)) (vec-map f v) (vec-map g v)) , (λ f g h → pr₂ (pr₂ (pr₂ γ)) (vec-map f v) (vec-map g v) (vec-map h v)) where γ : is-closeness (pr₁ (Vec-clospace Y n)) γ = pr₂ (Vec-clospace Y n) Least-PseudoClosenessSpace : (X : 𝓤 ̇ ) (Y : ClosenessSpace 𝓥) → (f : X → ⟨ Y ⟩) → {n : ℕ} → Vec X n → PseudoClosenessSpace (𝓤 ⊔ 𝓥) Least-PseudoClosenessSpace X Y f v = (X → ⟨ Y ⟩) , Least-clofun X Y v , Least-clofun-is-psclofun X Y v close-to-close : (X : ClosenessSpace 𝓤) → (Y : ClosenessSpace 𝓥) → (Z : ClosenessSpace 𝓦) → (f : ⟨ X ⟩ → ⟨ Y ⟩ → ⟨ Z ⟩) → {n : ℕ} (v : Vec ⟨ Y ⟩ n) → ((y : ⟨ Y ⟩) → f-ucontinuous X Z (λ x → f x y)) → ((g : ⟨ Y ⟩ → ⟨ Z ⟩) → f-ucontinuous' (ι X) (Least-PseudoClosenessSpace ⟨ Y ⟩ Z g v) f) close-to-close X Y Z f {0} ⟨⟩ _ k ε = 0 , λ _ _ _ _ _ → refl close-to-close X Y Z f {succ n} v@(y :: ys) ϕʸ g ε = δ , γ where IH = close-to-close X Y Z f ys ϕʸ g ε δ δ₁ δ₂ : ℕ δ₁ = pr₁ (ϕʸ y ε) δ₂ = pr₁ IH δ = max δ₁ δ₂ γ : (x₁ x₂ : ⟨ X ⟩) → C X δ x₁ x₂ → C' (Least-PseudoClosenessSpace ⟨ Y ⟩ Z g v) ε (f x₁) (f x₂) γ x₁ x₂ Cx₁x₂ n z = Lemma[a＝₁→b＝₁→min𝟚ab＝₁] (pr₂ (ϕʸ y ε) x₁ x₂ (C-mono X δ δ₁ (max-≤-upper-bound δ₁ δ₂) x₁ x₂ Cx₁x₂) n z) (pr₂ IH x₁ x₂ (C-mono X δ δ₂ (max-≤-upper-bound' δ₂ δ₁) x₁ x₂ Cx₁x₂) n z)## Subtype closeness spaces↪-clospace : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X ↪ Y) → is-closeness-space Y → is-closeness-space X ↪-clospace {𝓤} {𝓥} {X} {Y} (f , η) (cy , ey , iy , sy , uy) = c , e , i , s , u where c : X → X → ℕ∞ c x y = cy (f x) (f y) e : indistinguishable-are-equal c e x y cxy＝∞ = ap pr₁ (η (f y) (x , ey (f x) (f y) cxy＝∞) (y , refl)) i : self-indistinguishable c i x = iy (f x) s : is-symmetric c s x y = sy (f x) (f y) u : is-ultra c u x y z = uy (f x) (f y) (f z) ↪-ClosenessSpace : {X : 𝓤 ̇ } (Y : ClosenessSpace 𝓥) → X ↪ ⟨ Y ⟩ → ClosenessSpace 𝓤 ↪-ClosenessSpace {𝓤} {𝓥} {X} Y f = X , ↪-clospace f (pr₂ Y) Σ-clospace : {X : 𝓤 ̇ } → (P : X → 𝓥 ̇ ) → (p : (x : X) → is-prop (P x)) → is-closeness-space X → is-closeness-space (Σ P) Σ-clospace P p i = ↪-clospace (pr₁ , pr₁-is-embedding p) i Σ-ClosenessSpace : (X : ClosenessSpace 𝓤) → (P : ⟨ X ⟩ → 𝓥 ̇ ) → (p : (x : ⟨ X ⟩) → is-prop (P x)) → ClosenessSpace (𝓤 ⊔ 𝓥) Σ-ClosenessSpace {𝓤} {𝓥} X P p = Σ P , Σ-clospace P p (pr₂ X) ≃-ClosenessSpace : {X : 𝓤 ̇ } (Y : ClosenessSpace 𝓥) → X ≃ ⟨ Y ⟩ → ClosenessSpace 𝓤 ≃-ClosenessSpace Y e = ↪-ClosenessSpace Y (equivs-embedding e) ≃-preserves-nets : {X : 𝓤 ̇ } (Y : ClosenessSpace 𝓥) → (e : X ≃ ⟨ Y ⟩) → (ε : ℕ) → (Y' : 𝓥' ̇ ) → Y' is ε net-of Y → Y' is ε net-of (≃-ClosenessSpace Y e) ≃-preserves-nets Y (f , ((g , η) , (h , μ))) ε Y' ((gₙ , hₙ , ηₙ) , fₙ) = (g ∘ gₙ , hₙ ∘ f , λ x → C-trans Y ε (f x) (gₙ (hₙ (f x))) (f (g (gₙ (hₙ (f x))))) (ηₙ (f x)) (closeness-∞-implies-ϵ-close Y (gₙ (hₙ (f x))) (f (g (gₙ (hₙ (f x))))) (identical-implies-closeness-∞ Y _ _ (η (gₙ (hₙ (f x))) ⁻¹)) ε)) , fₙ ≃-totally-bounded : {X : 𝓤 ̇ } → (Y : ClosenessSpace 𝓥) → (e : X ≃ ⟨ Y ⟩) → totally-bounded Y 𝓥' → totally-bounded (≃-ClosenessSpace Y e) 𝓥' ≃-totally-bounded Y e t ε = pr₁ (t ε) , ≃-preserves-nets Y e ε (pr₁ (t ε)) (pr₂ (t ε))## Discrete sequence closeness spacesdecidable-𝟚 : {X : 𝓤 ̇ } → is-decidable X → 𝟚 decidable-𝟚 (inl _) = ₁ decidable-𝟚 (inr _) = ₀ decidable-𝟚₁ : {X : 𝓤 ̇ } (d : is-decidable X) → X → decidable-𝟚 d ＝ ₁ decidable-𝟚₁ (inl x) _ = refl decidable-𝟚₁ (inr ¬x) x = 𝟘-elim (¬x x) decidable-𝟚₀ : {X : 𝓤 ̇ } (d : is-decidable X) → ¬ X → decidable-𝟚 d ＝ ₀ decidable-𝟚₀ (inl x) ¬x = 𝟘-elim (¬x x) decidable-𝟚₀ (inr ¬x) _ = refl 𝟚-decidable₁ : {X : 𝓤 ̇ } (d : is-decidable X) → decidable-𝟚 d ＝ ₁ → X 𝟚-decidable₁ (inl x) _ = x 𝟚-decidable₀ : {X : 𝓤 ̇ } (d : is-decidable X) → decidable-𝟚 d ＝ ₀ → ¬ X 𝟚-decidable₀ (inr ¬x) _ = ¬x decidable-seq-𝟚 : {X : ℕ → 𝓤 ̇ } → is-complemented X → (ℕ → 𝟚) decidable-seq-𝟚 d n = decidable-𝟚 (d (succ n)) discrete-seq-clofun' : {X : ℕ → 𝓤 ̇ } → ((i : ℕ) → is-discrete (X i)) → Π X → Π X → (ℕ → 𝟚) discrete-seq-clofun' d α β = decidable-seq-𝟚 (∼ⁿ-decidable d α β) discrete-seq-clofun'-e : {X : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (X i)) → (α β : Π X) → ((n : ℕ) → discrete-seq-clofun' d α β n ＝ ₁) → α ＝ β discrete-seq-clofun'-e d α β f = dfunext (fe _ _) (λ n → 𝟚-decidable₁ (∼ⁿ-decidable d α β (succ n)) (f n) n (<-succ n)) discrete-seq-clofun'-i : {X : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (X i)) → (α : Π X) → (n : ℕ) → discrete-seq-clofun' d α α n ＝ ₁ discrete-seq-clofun'-i d α n = decidable-𝟚₁ (∼ⁿ-decidable d α α (succ n)) (λ _ _ → refl) discrete-seq-clofun'-s : {X : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (X i)) → (α β : Π X) → (n : ℕ) → discrete-seq-clofun' d α β n ＝ discrete-seq-clofun' d β α n discrete-seq-clofun'-s d α β n = γ (∼ⁿ-decidable d α β (succ n)) (∼ⁿ-decidable d β α (succ n)) where γ : (dαβ : is-decidable ((α ∼ⁿ β) (succ n))) → (dβα : is-decidable ((β ∼ⁿ α) (succ n))) → decidable-𝟚 dαβ ＝ decidable-𝟚 dβα γ (inl _) (inl _) = refl γ (inr _) (inr _) = refl γ (inl f) (inr g) = 𝟘-elim (g (∼ⁿ-sym α β (succ n) f)) γ (inr f) (inl g) = 𝟘-elim (f (∼ⁿ-sym β α (succ n) g)) discrete-seq-clofun'-u : {X : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (X i)) → (α β ζ : Π X) → (n : ℕ) → min𝟚 (discrete-seq-clofun' d α β n) (discrete-seq-clofun' d β ζ n) ＝ ₁ → discrete-seq-clofun' d α ζ n ＝ ₁ discrete-seq-clofun'-u d α β ζ n = γ (∼ⁿ-decidable d α β (succ n)) (∼ⁿ-decidable d β ζ (succ n)) (∼ⁿ-decidable d α ζ (succ n)) where γ : (dαβ : is-decidable ((α ∼ⁿ β) (succ n))) → (dβζ : is-decidable ((β ∼ⁿ ζ) (succ n))) → (dαζ : is-decidable ((α ∼ⁿ ζ) (succ n))) → min𝟚 (decidable-𝟚 dαβ) (decidable-𝟚 dβζ) ＝ ₁ → decidable-𝟚 dαζ ＝ ₁ γ _ _ (inl _) _ = refl γ (inl α∼ⁿβ) (inl β∼ⁿζ) (inr ¬α∼ⁿζ) m = 𝟘-elim (¬α∼ⁿζ (λ i i<n → α∼ⁿβ i i<n ∙ β∼ⁿζ i i<n)) ∼ⁿ-decidable-𝟚-decreasing : {X : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (X i)) → (α β : Π X) → is-decreasing (discrete-seq-clofun' d α β) ∼ⁿ-decidable-𝟚-decreasing d α β n = ≤₂-criterion (γ (∼ⁿ-decidable d α β (succ n)) (∼ⁿ-decidable d α β (succ (succ n)))) where γ : (dαβₛₙ : is-decidable ((α ∼ⁿ β) (succ n))) → (dαβₛₛₙ : is-decidable ((α ∼ⁿ β) (succ (succ n)))) → decidable-𝟚 dαβₛₛₙ ＝ ₁ → decidable-𝟚 dαβₛₙ ＝ ₁ γ (inl _) (inl _) _ = refl γ (inl _) (inr _) _ = refl γ (inr ¬α∼ˢⁿβ) (inl α∼ˢˢⁿβ) _ = (𝟘-elim ∘ ¬α∼ˢⁿβ) (λ i i<sn → α∼ˢˢⁿβ i (<-trans i (succ n) (succ (succ n)) i<sn (<-succ (succ n)))) discrete-seq-clofun : {X : ℕ → 𝓤 ̇ } → ((i : ℕ) → is-discrete (X i)) → Π X → Π X → ℕ∞ discrete-seq-clofun d α β = discrete-seq-clofun' d α β , ∼ⁿ-decidable-𝟚-decreasing d α β discrete-seq-clofun-e : {X : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (X i)) → indistinguishable-are-equal (discrete-seq-clofun d) discrete-seq-clofun-e d α β cαβ=∞ = discrete-seq-clofun'-e d α β (λ n → ap (λ - → ℕ∞-to-ℕ→𝟚 - n) cαβ=∞) discrete-seq-clofun-i : {X : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (X i)) → self-indistinguishable (discrete-seq-clofun d) discrete-seq-clofun-i d α = to-subtype-＝ (being-decreasing-is-prop (fe _ _)) (dfunext (fe _ _) (discrete-seq-clofun'-i d α)) discrete-seq-clofun-s : {X : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (X i)) → is-symmetric (discrete-seq-clofun d) discrete-seq-clofun-s d α β = to-subtype-＝ (being-decreasing-is-prop (fe _ _)) (dfunext (fe _ _) (discrete-seq-clofun'-s d α β)) discrete-seq-clofun-u : {X : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (X i)) → is-ultra (discrete-seq-clofun d) discrete-seq-clofun-u = discrete-seq-clofun'-u discrete-seq-clofun-c : {X : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (X i)) → is-closeness (discrete-seq-clofun d) discrete-seq-clofun-c d = discrete-seq-clofun-e d , discrete-seq-clofun-i d , discrete-seq-clofun-s d , discrete-seq-clofun-u d discrete-seq-clospace : {X : ℕ → 𝓤 ̇ } → ((i : ℕ) → is-discrete (X i)) → is-closeness-space (Π X) discrete-seq-clospace d = discrete-seq-clofun d , discrete-seq-clofun-c d ΠD-ClosenessSpace : {X : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (X i)) → ClosenessSpace 𝓤 ΠD-ClosenessSpace {𝓤} {X} d = Π X , discrete-seq-clospace d ∼ⁿ-to-C' : {X : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (X i)) → (α β : Π X) (n : ℕ) → (α ∼ⁿ β) n → C (ΠD-ClosenessSpace d) n α β ∼ⁿ-to-C' d α β (succ n) α∼ⁿβ i i<n = is-decreasing' (discrete-seq-clofun d α β) n i (⊏-gives-< i (succ n) i<n) (decidable-𝟚₁ (∼ⁿ-decidable d α β (succ n)) α∼ⁿβ) C-to-∼ⁿ' : {X : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (X i)) → (α β : Π X) (n : ℕ) → C (ΠD-ClosenessSpace d) n α β → (α ∼ⁿ β) n C-to-∼ⁿ' d α β (succ n) Cαβ i i<n = 𝟚-decidable₁ (∼ⁿ-decidable d α β (succ n)) (Cαβ n (<-gives-⊏ n (succ n) (<-succ n))) i i<n ℕ→D-ClosenessSpace : {X : 𝓤 ̇ } → (d : is-discrete X) → ClosenessSpace 𝓤 ℕ→D-ClosenessSpace {𝓤} {X} d = ΠD-ClosenessSpace (λ _ → d) ∼ⁿ-to-C : {X : 𝓤 ̇ } → (d : is-discrete X) → (α β : (ℕ → X)) (n : ℕ) → (α ∼ⁿ β) n → C (ℕ→D-ClosenessSpace d) n α β ∼ⁿ-to-C d = ∼ⁿ-to-C' (λ _ → d) C-to-∼ⁿ : {X : 𝓤 ̇ } → (d : is-discrete X) → (α β : (ℕ → X)) (n : ℕ) → C (ℕ→D-ClosenessSpace d) n α β → (α ∼ⁿ β) n C-to-∼ⁿ d = C-to-∼ⁿ' (λ _ → d) ΠF-totally-bounded : {F : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (F i)) → (f : (i : ℕ) → finite-linear-order (F i)) → Π F → totally-bounded (ΠD-ClosenessSpace d) 𝓤 ΠF-totally-bounded {𝓤} {F} d f α ϵ = vec ϵ (F ∘ ⟦_⟧) , (Vec-to-Seq ϵ (α ∘ succ ^ ϵ) , Seq-to-Vec ϵ , γ) , vec-is-finite ϵ (f ∘ ⟦_⟧) where γ : (β : ⟨ ΠD-ClosenessSpace d ⟩) → C (ΠD-ClosenessSpace d) ϵ β (Vec-to-Seq ϵ (α ∘ succ ^ ϵ) (Seq-to-Vec ϵ β)) γ β n n⊏ϵ = decidable-𝟚₁ (∼ⁿ-decidable d _ _ _) (λ i i<sn → Seq-to-Vec-∼ ϵ (α ∘ succ ^ ϵ) β i (≤-<-trans i n ϵ i<sn (⊏-gives-< n ϵ n⊏ϵ))) ℕ→F-totally-bounded : {F : 𝓤 ̇ } → (d : is-discrete F) → (f : finite-linear-order F) → F → totally-bounded (ℕ→D-ClosenessSpace d) 𝓤 ℕ→F-totally-bounded {𝓤} {F} d f x₀ = ΠF-totally-bounded (λ _ → d) (λ _ → f) (λ _ → x₀)## Infinitary product of closeness spacesΠ-clofun' : (T : ℕ → ClosenessSpace 𝓤) → Π (⟨_⟩ ∘ T) → Π (⟨_⟩ ∘ T) → (ℕ → 𝟚) Π-clofun' T x y zero = ℕ∞-to-ℕ→𝟚 (c⟨ T 0 ⟩ (x 0) (y 0)) 0 Π-clofun' T x y (succ n) = min𝟚 (ℕ∞-to-ℕ→𝟚 (c⟨ T 0 ⟩ (x 0) (y 0)) (succ n)) (Π-clofun' (T ∘ succ) (x ∘ succ) (y ∘ succ) n) Π-clofun'-d : (T : ℕ → ClosenessSpace 𝓤) → (x y : Π (⟨_⟩ ∘ T)) → is-decreasing (Π-clofun' T x y) Π-clofun'-d T x y zero = ≤₂-trans _ _ _ Lemma[minab≤₂a] (pr₂ (c⟨ T 0 ⟩ (x 0) (y 0)) 0) Π-clofun'-d T x y (succ n) = min𝟚-preserves-≤ (pr₂ (c⟨ T 0 ⟩ (x 0) (y 0)) (succ n)) (Π-clofun'-d (T ∘ succ) (x ∘ succ) (y ∘ succ) n) Π-clofun'-all : (T : ℕ → ClosenessSpace 𝓤) → (x y : Π (⟨_⟩ ∘ T)) → Π-clofun' T x y ∼ (λ i → ₁) → (n : ℕ) → (ℕ∞-to-ℕ→𝟚 (c⟨ T n ⟩ (x n) (y n))) ∼ (λ i → ₁) Π-clofun'-all T x y cxy∼∞ 0 zero = cxy∼∞ 0 Π-clofun'-all T x y cxy∼∞ 0 (succ i) = Lemma[min𝟚ab＝₁→a＝₁] (cxy∼∞ (succ i)) Π-clofun'-all T x y cxy∼∞ (succ n) = Π-clofun'-all (T ∘ succ) (x ∘ succ) (y ∘ succ) (λ i → Lemma[min𝟚ab＝₁→b＝₁] (cxy∼∞ (succ i))) n Π-clofun'-e : (T : ℕ → ClosenessSpace 𝓤) → (x y : Π (⟨_⟩ ∘ T)) → Π-clofun' T x y ∼ (λ i → ₁) → x ＝ y Π-clofun'-e T x y f = dfunext (fe _ _) (λ i → e⟨ T i ⟩ (x i) (y i) (to-subtype-＝ (being-decreasing-is-prop (fe _ _)) (dfunext (fe _ _) (Π-clofun'-all T x y f i)))) Π-clofun'-i : (T : ℕ → ClosenessSpace 𝓤) → (x : Π (⟨_⟩ ∘ T)) → Π-clofun' T x x ∼ (λ i → ₁) Π-clofun'-i T x 0 = ap (λ - → ℕ∞-to-ℕ→𝟚 - 0) (i⟨ T 0 ⟩ (x 0)) Π-clofun'-i T x (succ n) = Lemma[a＝₁→b＝₁→min𝟚ab＝₁] (ap (λ - → ℕ∞-to-ℕ→𝟚 - (succ n)) (i⟨ T 0 ⟩ (x 0))) (Π-clofun'-i (T ∘ succ) (x ∘ succ) n) Π-clofun'-s : (T : ℕ → ClosenessSpace 𝓤) → (x y : Π (⟨_⟩ ∘ T)) → Π-clofun' T x y ∼ Π-clofun' T y x Π-clofun'-s T x y zero = ap (λ - → ℕ∞-to-ℕ→𝟚 - 0) (s⟨ T 0 ⟩ (x 0) (y 0)) Π-clofun'-s T x y (succ n) = ap (λ - → min𝟚 - (Π-clofun' (T ∘ succ) (x ∘ succ) (y ∘ succ) n)) (ap (λ - → pr₁ - (succ n)) (s⟨ T 0 ⟩ (x 0) (y 0))) ∙ ap (λ - → min𝟚 (pr₁ (c⟨ T 0 ⟩ (y 0) (x 0)) (succ n)) -) (Π-clofun'-s (T ∘ succ) (x ∘ succ) (y ∘ succ) n) Lemma[min𝟚abcd＝₁→min𝟚ac＝₁] : (a b c d : 𝟚) → min𝟚 (min𝟚 a b) (min𝟚 c d) ＝ ₁ → min𝟚 a c ＝ ₁ Lemma[min𝟚abcd＝₁→min𝟚ac＝₁] ₁ ₁ ₁ ₁ e = refl Lemma[min𝟚abcd＝₁→min𝟚bd＝₁] : (a b c d : 𝟚) → min𝟚 (min𝟚 a b) (min𝟚 c d) ＝ ₁ → min𝟚 b d ＝ ₁ Lemma[min𝟚abcd＝₁→min𝟚bd＝₁] ₁ ₁ ₁ ₁ e = refl Π-clofun'-u : (T : ℕ → ClosenessSpace 𝓤) → (x y z : Π (⟨_⟩ ∘ T)) → (n : ℕ) → min𝟚 (Π-clofun' T x y n) (Π-clofun' T y z n) ＝ ₁ → Π-clofun' T x z n ＝ ₁ Π-clofun'-u T x y z 0 η = u⟨ T 0 ⟩ (x 0) (y 0) (z 0) 0 η Π-clofun'-u T x y z (succ n) η = Lemma[a＝₁→b＝₁→min𝟚ab＝₁] (u⟨ T 0 ⟩ (x 0) (y 0) (z 0) (succ n) (Lemma[min𝟚abcd＝₁→min𝟚ac＝₁] (ℕ∞-to-ℕ→𝟚 (c⟨ T 0 ⟩ (x 0) (y 0)) (succ n)) (Π-clofun' (T ∘ succ) (x ∘ succ) (y ∘ succ) n) (ℕ∞-to-ℕ→𝟚 (c⟨ T 0 ⟩ (y 0) (z 0)) (succ n)) (Π-clofun' (T ∘ succ) (y ∘ succ) (z ∘ succ) n) η)) (Π-clofun'-u (T ∘ succ) (x ∘ succ) (y ∘ succ) (z ∘ succ) n (Lemma[min𝟚abcd＝₁→min𝟚bd＝₁] (ℕ∞-to-ℕ→𝟚 (c⟨ T 0 ⟩ (x 0) (y 0)) (succ n)) (Π-clofun' (T ∘ succ) (x ∘ succ) (y ∘ succ) n) (ℕ∞-to-ℕ→𝟚 (c⟨ T 0 ⟩ (y 0) (z 0)) (succ n)) (Π-clofun' (T ∘ succ) (y ∘ succ) (z ∘ succ) n) η)) Π-clofun : (T : ℕ → ClosenessSpace 𝓤) → Π (⟨_⟩ ∘ T) → Π (⟨_⟩ ∘ T) → ℕ∞ Π-clofun T x y = (Π-clofun' T x y) , (Π-clofun'-d T x y) Π-clofun-e : (T : ℕ → ClosenessSpace 𝓤) → indistinguishable-are-equal (Π-clofun T) Π-clofun-e T x y f = Π-clofun'-e T x y (λ i → ap (λ - → pr₁ - i) f) Π-clofun-i : (T : ℕ → ClosenessSpace 𝓤) → self-indistinguishable (Π-clofun T) Π-clofun-i T x = to-subtype-＝ (being-decreasing-is-prop (fe _ _)) (dfunext (fe _ _) (Π-clofun'-i T x)) Π-clofun-s : (T : ℕ → ClosenessSpace 𝓤) → is-symmetric (Π-clofun T) Π-clofun-s T x y = to-subtype-＝ (being-decreasing-is-prop (fe _ _)) (dfunext (fe _ _) (Π-clofun'-s T x y)) Π-clofun-u : (T : ℕ → ClosenessSpace 𝓤) → is-ultra (Π-clofun T) Π-clofun-u = Π-clofun'-u Π-clofun-c : (T : ℕ → ClosenessSpace 𝓤) → is-closeness (Π-clofun T) Π-clofun-c T = Π-clofun-e T , Π-clofun-i T , Π-clofun-s T , Π-clofun-u T Π-clospace : (T : ℕ → ClosenessSpace 𝓤) → is-closeness-space (Π (⟨_⟩ ∘ T)) Π-clospace T = Π-clofun T , Π-clofun-c T Π-ClosenessSpace : (T : ℕ → ClosenessSpace 𝓤) → ClosenessSpace 𝓤 Π-ClosenessSpace T = Π (⟨_⟩ ∘ T) , Π-clospace T Π-totally-bounded : (T : ℕ → ClosenessSpace 𝓤) → ((n : ℕ) → ⟨ T n ⟩) → ((n : ℕ) → totally-bounded (T n) 𝓦) → totally-bounded (Π-ClosenessSpace T) 𝓦 Π-totally-bounded {𝓤} {𝓦} T p t 0 = pointed-has-a-0-net (Π-ClosenessSpace T) p Π-totally-bounded {𝓤} {𝓦} T p t (succ ϵ) = (t₀' × IH') , (g , h , η) , f where c₀ = pr₁ (pr₂ (T 0)) t₀ = t 0 (succ ϵ) t₀' = pr₁ t₀ t₀'-is-sϵ-net = pr₂ t₀ g₀' = pr₁ (pr₁ t₀'-is-sϵ-net) h₀' = pr₁ (pr₂ (pr₁ t₀'-is-sϵ-net)) η₀' = pr₂ (pr₂ (pr₁ t₀'-is-sϵ-net)) IH = Π-totally-bounded (T ∘ succ) (p ∘ succ) (t ∘ succ) ϵ IH' = pr₁ IH IH'-is-ϵ-net = pr₂ IH gₛ' = pr₁ (pr₁ IH'-is-ϵ-net) hₛ' = pr₁ (pr₂ (pr₁ IH'-is-ϵ-net)) ηₛ' = pr₂ (pr₂ (pr₁ IH'-is-ϵ-net)) g : t₀' × IH' → Π (⟨_⟩ ∘ T) g (x' , αₛ') = g₀' x' ∷ gₛ' αₛ' h : Π (⟨_⟩ ∘ T) → t₀' × IH' h α = h₀' (α 0) , hₛ' (α ∘ succ) η : (x : Π (⟨_⟩ ∘ T)) → C (Π-ClosenessSpace T) (succ ϵ) x (g (h x)) η α 0 = η₀' (α 0) 0 η α (succ n) n⊏ϵ = Lemma[a＝₁→b＝₁→min𝟚ab＝₁] (η₀' (α 0) (succ n) n⊏ϵ) (ηₛ' (α ∘ succ) n n⊏ϵ) f : finite-linear-order (t₀' × IH') f = ×-is-finite (pr₂ t₀'-is-sϵ-net) (pr₂ IH'-is-ϵ-net) Π-clofuns-id' : {T : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (T i)) → (x y : Π T) → discrete-seq-clofun' d x y ∼ Π-clofun' (λ n → D-ClosenessSpace (d n)) x y Π-clofuns-id' d x y 0 = γ (∼ⁿ-decidable d x y 1) (d 0 (x 0) (y 0)) where γ : (dx∼¹y : is-decidable ((x ∼ⁿ y) 1)) → (dxy₀ : is-decidable (x 0 ＝ y 0)) → decidable-𝟚 dx∼¹y ＝ pr₁ (discrete-clofun'' (x 0) (y 0) dxy₀) 0 γ (inl _) (inl _) = refl γ (inr _) (inr _) = refl γ (inl x∼¹y) (inr x₀≠y₀) = 𝟘-elim (x₀≠y₀ (x∼¹y 0 ⋆)) γ (inr ¬x∼¹y) (inl x₀=y₀) = 𝟘-elim (¬x∼¹y γ') where γ' : (x ∼ⁿ y) 1 γ' 0 ⋆ = x₀=y₀ Π-clofuns-id' d x y (succ i) = γ (∼ⁿ-decidable d x y (succ (succ i))) (d 0 (x 0) (y 0)) where γ' : x 0 ＝ y 0 → ((x ∘ succ) ∼ⁿ (y ∘ succ)) (succ i) → (x ∼ⁿ y) (succ (succ i)) γ' x₀=y₀ tx∼ˢⁱty 0 _ = x₀=y₀ γ' x₀=y₀ tx∼ˢⁱty (succ j) = tx∼ˢⁱty j γ : (dx∼ˢˢⁱy : is-decidable ((x ∼ⁿ y) (succ (succ i)))) → (dxy₀ : is-decidable (x 0 ＝ y 0)) → decidable-𝟚 dx∼ˢˢⁱy ＝ min𝟚 (pr₁ (discrete-clofun'' (x 0) (y 0) dxy₀) (succ i)) (Π-clofun' (λ n → D-ClosenessSpace (d (succ n))) (x ∘ succ) (y ∘ succ) i) γ (inl x∼ˢˢⁱy) (inl _) = Lemma[a＝₁→b＝₁→min𝟚ab＝₁] refl (Π-clofuns-id' (d ∘ succ) (x ∘ succ) (y ∘ succ) i ⁻¹ ∙ decidable-𝟚₁ (∼ⁿ-decidable (d ∘ succ) _ _ _) (x∼ˢˢⁱy ∘ succ)) ⁻¹ γ (inl x∼ˢˢⁱy) (inr x₀≠y₀) = 𝟘-elim (x₀≠y₀ (x∼ˢˢⁱy 0 ⋆)) γ (inr ¬x∼ˢˢⁱy) (inl x₀=y₀) = Lemma[min𝟚ab＝₀] (inr (Π-clofuns-id' (d ∘ succ) (x ∘ succ) (y ∘ succ) i ⁻¹ ∙ decidable-𝟚₀ (∼ⁿ-decidable (d ∘ succ) _ _ _) (λ tx∼ˢⁱty → ¬x∼ˢˢⁱy (γ' x₀=y₀ tx∼ˢⁱty)))) ⁻¹ γ (inr ¬x∼ˢˢⁱy) (inr x₀≠y₀) = refl Π-clofuns-id : {T : ℕ → 𝓤 ̇ } → (d : (i : ℕ) → is-discrete (T i)) → c⟨ ΠD-ClosenessSpace d ⟩ ＝ c⟨ Π-ClosenessSpace (λ n → D-ClosenessSpace (d n)) ⟩ Π-clofuns-id d = dfunext (fe _ _) (λ x → dfunext (fe _ _) (λ y → to-subtype-＝ (being-decreasing-is-prop (fe _ _)) (dfunext (fe _ _) (Π-clofuns-id' d x y)))) Π-C-combine : (T : ℕ → ClosenessSpace 𝓤) → (x₁ x₂ : ⟨ T 0 ⟩) (y₁ y₂ : Π (⟨_⟩ ∘ T ∘ succ)) → (ε : ℕ) → C (T 0) (succ ε) x₁ x₂ → C (Π-ClosenessSpace (T ∘ succ)) ε y₁ y₂ → C (Π-ClosenessSpace T) (succ ε) (x₁ ∷ y₁) (x₂ ∷ y₂) Π-C-combine T x₁ x₂ y₁ y₂ ε Cεx₁x₂ Cεy₁y₂ 0 = Cεx₁x₂ 0 Π-C-combine T x₁ x₂ y₁ y₂ ε Cεx₁x₂ Cεy₁y₂ (succ n) sn⊏ε = Lemma[a＝₁→b＝₁→min𝟚ab＝₁] (Cεx₁x₂ (succ n) sn⊏ε) (Cεy₁y₂ n sn⊏ε) Π-C-eta : (T : ℕ → ClosenessSpace 𝓤) → (α : Π (⟨_⟩ ∘ T)) → (ε : ℕ) → C (Π-ClosenessSpace T) ε α (α 0 ∷ (α ∘ succ)) Π-C-eta T α ε 0 = C-refl (T 0) ε (α 0) 0 Π-C-eta T α (succ ε) (succ n) = Π-C-combine T (α 0) (α 0) (α ∘ succ) (α ∘ succ) ε (C-refl (T 0) (succ ε) (α 0)) (C-refl (Π-ClosenessSpace (T ∘ succ)) ε (α ∘ succ)) (succ n)## Specific examples of closeness spaces𝟚ᴺ-ClosenessSpace : ClosenessSpace 𝓤₀ 𝟚ᴺ-ClosenessSpace = ℕ→D-ClosenessSpace 𝟚-is-discrete 𝟚ᴺ×𝟚ᴺ-ClosenessSpace : ClosenessSpace 𝓤₀ 𝟚ᴺ×𝟚ᴺ-ClosenessSpace = ×-ClosenessSpace 𝟚ᴺ-ClosenessSpace 𝟚ᴺ-ClosenessSpace ℕ∞-ClosenessSpace : ClosenessSpace 𝓤₀ ℕ∞-ClosenessSpace = Σ-ClosenessSpace 𝟚ᴺ-ClosenessSpace is-decreasing (being-decreasing-is-prop (fe _ _)) open import TWA.Thesis.Chapter5.SignedDigit 𝟛ᴺ-ClosenessSpace : ClosenessSpace 𝓤₀ 𝟛ᴺ-ClosenessSpace = ℕ→D-ClosenessSpace 𝟛-is-discrete 𝟛ᴺ×𝟛ᴺ-ClosenessSpace : ClosenessSpace 𝓤₀ 𝟛ᴺ×𝟛ᴺ-ClosenessSpace = ×-ClosenessSpace 𝟛ᴺ-ClosenessSpace 𝟛ᴺ-ClosenessSpace