Todd Waugh Ambridge, January 2024
# Examples of closeness spaces
\begin{code}
{-# 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)
\end{code}
## Trivial closeness spaces
\begin{code}
𝟘-clospace : is-closeness-space (𝟘 {𝓤})
𝟘-clospace = (λ ()) , ((λ ()) , (λ ()) , ((λ ()) , (λ ())))
𝟙-clospace : is-closeness-space (𝟙 {𝓤})
𝟙-clospace
= (λ _ _ → ∞)
, (λ _ _ _ → refl)
, (λ _ → refl)
, (λ _ _ → refl)
, (λ _ _ _ _ _ → refl)
\end{code}
## Discrete closeness spaces
\begin{code}
discrete-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ₙ=₁)
\end{code}
## Disjoint union of closeness spaces
\begin{code}
+-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
\end{code}
## Binary product of closeness spaces
\begin{code}
×-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 ε)
\end{code}
## Vector closeness spaces
\begin{code}
vec-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)
\end{code}
## Least closeness pseudocloseness space
\begin{code}
Least-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)
\end{code}
## Subtype closeness spaces
\begin{code}
↪-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 ε))
\end{code}
## Discrete sequence closeness spaces
\begin{code}
decidable-𝟚 : {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₀)
\end{code}
## Infinitary product of closeness spaces
\begin{code}
Π-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)
\end{code}
## Specific examples of closeness spaces
\begin{code}
𝟚ᴺ-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
\end{code}