From 6508a945f5bf9cff6e39cb6a331361d6257d5eee Mon Sep 17 00:00:00 2001 From: malarbol Date: Sat, 22 Nov 2025 18:28:07 +0100 Subject: [PATCH 01/30] misc results --- ...-quotients-of-pseudometric-spaces.lagda.md | 2 +- ...uchy-approximations-metric-spaces.lagda.md | 2 +- ...pproximations-pseudometric-spaces.lagda.md | 24 ++- ...pseudocompletion-of-metric-spaces.lagda.md | 100 +++++++++++ ...completion-of-pseudometric-spaces.lagda.md | 160 ++++++++++++++++-- ...-quotients-of-pseudometric-spaces.lagda.md | 14 ++ ...y-of-elements-pseudometric-spaces.lagda.md | 40 +++-- 7 files changed, 318 insertions(+), 24 deletions(-) diff --git a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md index 9184f29af6a..4c46e7a886c 100644 --- a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md @@ -107,7 +107,7 @@ module _ ( cauchy-pseudocompletion-Metric-Space ( metric-quotient-Pseudometric-Space M)) short-map-metric-quotient-cauchy-apprtoximation-Pseudometric-Space = - short-map-short-function-cauchy-approximation-Pseudometric-Space + short-map-cauchy-approximation-short-function-Pseudometric-Space ( M) ( pseudometric-metric-quotient-Pseudometric-Space M) ( short-map-metric-quotient-Pseudometric-Space M) diff --git a/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md index caf5ee3d31c..d8bf919a55c 100644 --- a/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md @@ -123,7 +123,7 @@ module _ cauchy-approximation-Metric-Space A → cauchy-approximation-Metric-Space B map-short-function-cauchy-approximation-Metric-Space = - map-short-function-cauchy-approximation-Pseudometric-Space + map-cauchy-approximation-short-function-Pseudometric-Space ( pseudometric-Metric-Space A) ( pseudometric-Metric-Space B) ( f) diff --git a/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md index 3f7b863d422..b6b0b62a391 100644 --- a/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md @@ -19,6 +19,7 @@ open import foundation.propositions open import foundation.subtypes open import foundation.universe-levels +open import metric-spaces.isometries-pseudometric-spaces open import metric-spaces.pseudometric-spaces open import metric-spaces.short-functions-pseudometric-spaces ``` @@ -112,10 +113,10 @@ module _ (f : short-function-Pseudometric-Space A B) where - map-short-function-cauchy-approximation-Pseudometric-Space : + map-cauchy-approximation-short-function-Pseudometric-Space : cauchy-approximation-Pseudometric-Space A → cauchy-approximation-Pseudometric-Space B - map-short-function-cauchy-approximation-Pseudometric-Space (u , H) = + map-cauchy-approximation-short-function-Pseudometric-Space (u , H) = ( map-short-function-Pseudometric-Space A B f ∘ u , λ ε δ → is-short-map-short-function-Pseudometric-Space @@ -128,6 +129,25 @@ module _ ( H ε δ)) ``` +### The action of isometries on Cauchy approximations + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2') + (f : isometry-Pseudometric-Space A B) + where + + map-cauchy-approximation-isometry-Pseudometric-Space : + cauchy-approximation-Pseudometric-Space A → + cauchy-approximation-Pseudometric-Space B + map-cauchy-approximation-isometry-Pseudometric-Space = + map-cauchy-approximation-short-function-Pseudometric-Space + ( A) + ( B) + ( short-isometry-Pseudometric-Space A B f) +``` + ### Homotopic Cauchy approximations are equal ```agda diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md index 9dad3ad6549..2cdba77681c 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md @@ -437,3 +437,103 @@ module _ ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u) ( is-limit-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u) ``` + +### The isometry from the Cauchy pseudocompletion of a complete metric space to its limit + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + (is-complete-M : is-complete-Metric-Space M) + where + + abstract + reflects-neighborhood-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space : + (δ : ℚ⁺) → + (u v : cauchy-approximation-Metric-Space M) → + neighborhood-Metric-Space + ( M) + ( δ) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + ( M) + ( is-complete-M) + ( u)) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + ( M) + ( is-complete-M) + ( v)) → + neighborhood-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Space M) + ( δ) + ( u) + ( v) + reflects-neighborhood-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + δ x y Nδ = + reflects-neighborhood-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Space M) + { x} + { const-cauchy-approximation-Metric-Space + ( M) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + ( M) + ( is-complete-M) + ( x))} + { y} + { const-cauchy-approximation-Metric-Space + ( M) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + ( M) + ( is-complete-M) + ( y))} + ( sim-const-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + ( M) + ( is-complete-M) + ( x)) + ( sim-const-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + ( M) + ( is-complete-M) + ( y)) + ( δ) + ( preserves-neighborhood-map-isometry-Pseudometric-Space + ( pseudometric-Metric-Space M) + ( cauchy-pseudocompletion-Metric-Space M) + ( isometry-cauchy-pseudocompletion-Metric-Space M) + ( δ) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + ( M) + ( is-complete-M) + ( x)) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + ( M) + ( is-complete-M) + ( y)) + ( Nδ)) + + is-isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space : + is-isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Space M) + ( pseudometric-Metric-Space M) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + ( M) + ( is-complete-M)) + is-isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space d x y = + ( ( is-short-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + ( M) + ( is-complete-M) + ( d) + ( x) + ( y)) , + ( reflects-neighborhood-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + ( d) + ( x) + ( y))) + + isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space : + isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Space M) + ( pseudometric-Metric-Space M) + isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space = + ( ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + ( M) + ( is-complete-M)) , + ( is-isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space)) +``` diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index 5bc301fcc11..d4b849e8777 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -412,6 +412,64 @@ module _ ( λ d → H d α β) ``` +### Similarity in the Cauchy pseudocompletion preserves and reflects limits + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + (u v : cauchy-approximation-Pseudometric-Space M) + (x : type-Pseudometric-Space M) + where + + has-same-limit-sim-cauchy-approximation-Pseudometric-Space : + sim-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( u) + ( v) → + is-limit-cauchy-approximation-Pseudometric-Space M u x → + is-limit-cauchy-approximation-Pseudometric-Space M v x + has-same-limit-sim-cauchy-approximation-Pseudometric-Space u~v lim-u = + is-limit-sim-const-cauchy-approximation-Pseudometric-Space + ( M) + ( v) + ( x) + ( transitive-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( v) + ( u) + ( const-cauchy-approximation-Pseudometric-Space M x) + ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space + ( M) + ( u) + ( x) + ( lim-u)) + ( inv-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( u~v))) + + sim-has-same-limit-cauchy-approximation-Pseudometric-Space : + is-limit-cauchy-approximation-Pseudometric-Space M u x → + is-limit-cauchy-approximation-Pseudometric-Space M v x → + sim-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( u) + ( v) + sim-has-same-limit-cauchy-approximation-Pseudometric-Space lim-u lim-v = + transitive-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( u) + ( const-cauchy-approximation-Pseudometric-Space M x) + ( v) + ( inv-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space + ( M) + ( v) + ( x) + ( lim-v))) + ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space M u x lim-u) +``` + ### Any Cauchy approximation in the Cauchy pseudocompletion of a pseudometric space has a limit ```agda @@ -772,12 +830,12 @@ module _ (f : short-function-Pseudometric-Space A B) where - is-short-map-short-function-cauchy-approximation-Pseudometric-Space : + is-short-map-cauchy-approximation-short-function-Pseudometric-Space : is-short-function-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space A) ( cauchy-pseudocompletion-Pseudometric-Space B) - ( map-short-function-cauchy-approximation-Pseudometric-Space A B f) - is-short-map-short-function-cauchy-approximation-Pseudometric-Space + ( map-cauchy-approximation-short-function-Pseudometric-Space A B f) + is-short-map-cauchy-approximation-short-function-Pseudometric-Space d x y Nxy α β = is-short-map-short-function-Pseudometric-Space A B f ( α +ℚ⁺ β +ℚ⁺ d) @@ -785,13 +843,95 @@ module _ ( map-cauchy-approximation-Pseudometric-Space A y β) ( Nxy α β) - short-map-short-function-cauchy-approximation-Pseudometric-Space : + short-map-cauchy-approximation-short-function-Pseudometric-Space : short-function-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space A) ( cauchy-pseudocompletion-Pseudometric-Space B) - short-map-short-function-cauchy-approximation-Pseudometric-Space = - ( map-short-function-cauchy-approximation-Pseudometric-Space A B f , - is-short-map-short-function-cauchy-approximation-Pseudometric-Space) + short-map-cauchy-approximation-short-function-Pseudometric-Space = + ( map-cauchy-approximation-short-function-Pseudometric-Space A B f , + is-short-map-cauchy-approximation-short-function-Pseudometric-Space) +``` + +### The action of isometries on Cauchy approximations is an isometry + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2') + (f : isometry-Pseudometric-Space A B) + where abstract + + preserves-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space : + (d : ℚ⁺) → + (x y : cauchy-approximation-Pseudometric-Space A) → + neighborhood-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space A) + ( d) + ( x) + ( y) → + neighborhood-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space B) + ( d) + ( map-cauchy-approximation-isometry-Pseudometric-Space A B f x) + ( map-cauchy-approximation-isometry-Pseudometric-Space A B f y) + preserves-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space = + is-short-map-cauchy-approximation-short-function-Pseudometric-Space + ( A) + ( B) + ( short-isometry-Pseudometric-Space A B f) + + reflects-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space : + (d : ℚ⁺) → + (x y : cauchy-approximation-Pseudometric-Space A) → + neighborhood-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space B) + ( d) + ( map-cauchy-approximation-isometry-Pseudometric-Space A B f x) + ( map-cauchy-approximation-isometry-Pseudometric-Space A B f y) → + neighborhood-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space A) + ( d) + ( x) + ( y) + reflects-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space + d x y Nxy α β = + reflects-neighborhood-map-isometry-Pseudometric-Space + ( A) + ( B) + ( f) + ( α +ℚ⁺ β +ℚ⁺ d) + ( map-cauchy-approximation-Pseudometric-Space A x α) + ( map-cauchy-approximation-Pseudometric-Space A y β) + ( Nxy α β) + + is-isometry-map-cauchy-approximation-isometry-Pseudometric-Space : + is-isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space A) + ( cauchy-pseudocompletion-Pseudometric-Space B) + ( map-cauchy-approximation-isometry-Pseudometric-Space A B f) + is-isometry-map-cauchy-approximation-isometry-Pseudometric-Space d x y = + ( ( preserves-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space + ( d) + ( x) + ( y)) , + ( reflects-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space + ( d) + ( x) + ( y))) + +module _ + {l1 l2 l1' l2' : Level} + (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2') + (f : isometry-Pseudometric-Space A B) + where + + isometry-map-cauchy-approximation-isometry-Pseudometric-Space : + isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space A) + ( cauchy-pseudocompletion-Pseudometric-Space B) + isometry-map-cauchy-approximation-isometry-Pseudometric-Space = + ( map-cauchy-approximation-isometry-Pseudometric-Space A B f , + is-isometry-map-cauchy-approximation-isometry-Pseudometric-Space A B f) ``` ### The image of a Cauchy approximation in the Cauchy pseudocompletion is convergent @@ -805,7 +945,7 @@ module _ is-limit-map-cauchy-approximation-cauchy-pseudocompletion-Ppseudometric-Space : is-limit-cauchy-approximation-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M) - ( map-short-function-cauchy-approximation-Pseudometric-Space + ( map-cauchy-approximation-short-function-Pseudometric-Space ( M) ( cauchy-pseudocompletion-Pseudometric-Space M) ( short-map-cauchy-pseudocompletion-Pseudometric-Space M) @@ -839,7 +979,7 @@ module _ sim-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M)) - ( map-short-function-cauchy-approximation-Pseudometric-Space + ( map-cauchy-approximation-short-function-Pseudometric-Space ( M) ( cauchy-pseudocompletion-Pseudometric-Space M) ( short-map-cauchy-pseudocompletion-Pseudometric-Space M) @@ -850,7 +990,7 @@ module _ sim-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space = sim-const-is-limit-cauchy-approximation-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M) - ( map-short-function-cauchy-approximation-Pseudometric-Space + ( map-cauchy-approximation-short-function-Pseudometric-Space ( M) ( cauchy-pseudocompletion-Pseudometric-Space M) ( short-map-cauchy-pseudocompletion-Pseudometric-Space M) diff --git a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md index ffecd0aafca..3f48274856b 100644 --- a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md @@ -386,6 +386,20 @@ module _ map-subtype-metric-quotient-Pseudometric-Space = inhabitant-equivalence-class-quotient-map-set-quotient ( equivalence-relation-sim-Pseudometric-Space M) + + eq-map-is-in-class-metric-quotient-Pseudometric-Space : + (X : type-metric-quotient-Pseudometric-Space M) → + {x : type-Pseudometric-Space M} → + is-in-class-metric-quotient-Pseudometric-Space + ( M) + ( X) + ( x) → + map-metric-quotient-Pseudometric-Space x ＝ X + eq-map-is-in-class-metric-quotient-Pseudometric-Space X {x} x∈X = + eq-set-quotient-equivalence-class-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + ( X) + ( x∈X) ``` ### The mapping from a pseudometric space its quotient metric space is an isometry diff --git a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md index f9caa041d21..168c7d67105 100644 --- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md @@ -22,6 +22,7 @@ open import foundation.propositions open import foundation.transport-along-identifications open import foundation.universe-levels +open import metric-spaces.isometries-pseudometric-spaces open import metric-spaces.pseudometric-spaces open import metric-spaces.rational-neighborhood-relations open import metric-spaces.short-functions-pseudometric-spaces @@ -314,15 +315,34 @@ module _ ( A : Pseudometric-Space l1 l2) ( B : Pseudometric-Space l1' l2') ( f : short-function-Pseudometric-Space A B) - where + where abstract + + preserves-sim-map-short-function-Pseudometric-Space : + ( x y : type-Pseudometric-Space A) → + ( sim-Pseudometric-Space A x y) → + ( sim-Pseudometric-Space B + ( map-short-function-Pseudometric-Space A B f x) + ( map-short-function-Pseudometric-Space A B f y)) + preserves-sim-map-short-function-Pseudometric-Space x y x~y d = + is-short-map-short-function-Pseudometric-Space A B f d x y (x~y d) +``` - abstract - preserves-sim-map-short-function-Pseudometric-Space : - ( x y : type-Pseudometric-Space A) → - ( sim-Pseudometric-Space A x y) → - ( sim-Pseudometric-Space B - ( map-short-function-Pseudometric-Space A B f x) - ( map-short-function-Pseudometric-Space A B f y)) - preserves-sim-map-short-function-Pseudometric-Space x y x~y d = - is-short-map-short-function-Pseudometric-Space A B f d x y (x~y d) +### Isometries between pseudometric spaces reflect similarity + +```agda +module _ + { l1 l2 l1' l2' : Level} + ( A : Pseudometric-Space l1 l2) + ( B : Pseudometric-Space l1' l2') + ( f : isometry-Pseudometric-Space A B) + where abstract + + reflects-sim-map-isometry-Pseudometric-Space : + ( x y : type-Pseudometric-Space A) → + ( sim-Pseudometric-Space B + ( map-isometry-Pseudometric-Space A B f x) + ( map-isometry-Pseudometric-Space A B f y)) → + ( sim-Pseudometric-Space A x y) + reflects-sim-map-isometry-Pseudometric-Space x y fx~fy d = + reflects-neighborhood-map-isometry-Pseudometric-Space A B f d x y (fx~fy d) ``` From 02e4ae067ab829386dfce8bacd5c0a67ced06ef1 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sat, 22 Nov 2025 18:47:20 +0100 Subject: [PATCH 02/30] metric extensions --- src/metric-spaces.lagda.md | 1 + ...extensions-of-pseudometric-spaces.lagda.md | 231 ++++++++++++++++++ 2 files changed, 232 insertions(+) create mode 100644 src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md index bc48c2ee7e7..bb1b20c3bec 100644 --- a/src/metric-spaces.lagda.md +++ b/src/metric-spaces.lagda.md @@ -106,6 +106,7 @@ open import metric-spaces.limits-of-sequences-metric-spaces public open import metric-spaces.lipschitz-functions-metric-spaces public open import metric-spaces.locally-constant-functions-metric-spaces public open import metric-spaces.located-metric-spaces public +open import metric-spaces.metric-extensions-of-pseudometric-spaces public open import metric-spaces.metric-quotients-of-pseudometric-spaces public open import metric-spaces.metric-space-of-cauchy-approximations-complete-metric-spaces public open import metric-spaces.metric-space-of-cauchy-approximations-metric-spaces public diff --git a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md new file mode 100644 index 00000000000..c6e0fe412fe --- /dev/null +++ b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md @@ -0,0 +1,231 @@ +# Metric extensions of pseudometric spaces + +```agda +module metric-spaces.metric-extensions-of-pseudometric-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.strict-inequality-positive-rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.binary-relations +open import foundation.binary-transport +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.set-quotients +open import foundation.sets +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import metric-spaces.cauchy-approximations-metric-quotients-of-pseudometric-spaces +open import metric-spaces.cauchy-approximations-metric-spaces +open import metric-spaces.cauchy-approximations-pseudometric-spaces +open import metric-spaces.cauchy-pseudocompletion-of-metric-spaces +open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces +open import metric-spaces.complete-metric-spaces +open import metric-spaces.convergent-cauchy-approximations-metric-spaces +open import metric-spaces.equality-of-metric-spaces +open import metric-spaces.functions-metric-spaces +open import metric-spaces.functions-pseudometric-spaces +open import metric-spaces.isometries-metric-spaces +open import metric-spaces.isometries-pseudometric-spaces +open import metric-spaces.limits-of-cauchy-approximations-metric-spaces +open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces +open import metric-spaces.metric-quotients-of-pseudometric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.precategory-of-metric-spaces-and-short-functions +open import metric-spaces.pseudometric-spaces +open import metric-spaces.rational-neighborhood-relations +open import metric-spaces.short-functions-metric-spaces +open import metric-spaces.short-functions-pseudometric-spaces +open import metric-spaces.similarity-of-elements-pseudometric-spaces +``` + +
+ +## Idea + +A +{{#concept "metric extension" Disambiguation="of a pseudometric space" Agda=Metric-Extension}} +of a [pseudometric space](metric-spaces.pseudometric-spaces.md) `P` is a +[metric space](metric-spaces.metric-spaces.md) `M` together with an +[isometry](metric-spaces.isometries-pseudometric-spaces.md) `f : P → M`. + +## Definition + +### Metric extensions of pseudometric spaces + +```agda +module _ + {l1 l2 : Level} (l3 l4 : Level) (P : Pseudometric-Space l1 l2) + where + + Metric-Extension : UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4) + Metric-Extension = + Σ ( Metric-Space l3 l4) + ( isometry-Pseudometric-Space P ∘ pseudometric-Metric-Space) +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} (P : Pseudometric-Space l1 l2) + (M : Metric-Extension l3 l4 P) + where + + metric-space-Metric-Extension : Metric-Space l3 l4 + metric-space-Metric-Extension = pr1 M + + pseudometric-space-Metric-Extension : Pseudometric-Space l3 l4 + pseudometric-space-Metric-Extension = + pseudometric-Metric-Space metric-space-Metric-Extension + + type-metric-space-Metric-Extension : UU l3 + type-metric-space-Metric-Extension = + type-Metric-Space metric-space-Metric-Extension + + isometry-Metric-Extension : + isometry-Pseudometric-Space P pseudometric-space-Metric-Extension + isometry-Metric-Extension = pr2 M +``` + +## Properties + +### Action of metric extensions on Cauchy approximations + +```agda +module _ + {l1 l2 l3 l4 : Level} (P : Pseudometric-Space l1 l2) + (M : Metric-Extension l3 l4 P) + where + + isometry-cauchy-pseudocompletion-Metric-Extension : + isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space P) + ( cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Extension P M)) + isometry-cauchy-pseudocompletion-Metric-Extension = + isometry-map-cauchy-approximation-isometry-Pseudometric-Space + ( P) + ( pseudometric-space-Metric-Extension P M) + ( isometry-Metric-Extension P M) + + map-cauchy-pseudocompletion-Metric-Extension : + cauchy-approximation-Pseudometric-Space P → + cauchy-approximation-Metric-Space + ( metric-space-Metric-Extension P M) + map-cauchy-pseudocompletion-Metric-Extension = + map-isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space P) + ( cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Extension P M)) + ( isometry-cauchy-pseudocompletion-Metric-Extension) + + is-isometry-map-cauchy-pseudocompletion-Metric-Extension : + is-isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space P) + ( cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Extension P M)) + ( map-cauchy-pseudocompletion-Metric-Extension) + is-isometry-map-cauchy-pseudocompletion-Metric-Extension = + is-isometry-map-isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space P) + ( cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Extension P M)) + ( isometry-cauchy-pseudocompletion-Metric-Extension) +``` + +### Limit points in metric extensions + +```agda +module _ + {l1 l2 l3 l4 : Level} + (P : Pseudometric-Space l1 l2) + (M : Metric-Extension l3 l4 P) + (u : cauchy-approximation-Pseudometric-Space P) + (y : type-metric-space-Metric-Extension P M) + where + + is-limit-map-cauchy-pseudocompletion-prop-Metric-Extension : Prop l4 + is-limit-map-cauchy-pseudocompletion-prop-Metric-Extension = + is-limit-cauchy-approximation-prop-Metric-Space + ( metric-space-Metric-Extension P M) + ( map-cauchy-pseudocompletion-Metric-Extension P M u) + ( y) + + is-limit-map-cauchy-pseudocompletion-Metric-Extension : UU l4 + is-limit-map-cauchy-pseudocompletion-Metric-Extension = + type-Prop + is-limit-map-cauchy-pseudocompletion-prop-Metric-Extension + + is-prop-is-limit-map-cauchy-pseudocompletion-Metric-Extension : + is-prop is-limit-map-cauchy-pseudocompletion-Metric-Extension + is-prop-is-limit-map-cauchy-pseudocompletion-Metric-Extension = + is-prop-type-Prop + is-limit-map-cauchy-pseudocompletion-prop-Metric-Extension +``` + +### Cauchy approximations converging to the same image in a metric extension are similar in the Cauchy pseudocompletion + +```agda +module _ + {l1 l2 l3 l4 : Level} + (P : Pseudometric-Space l1 l2) + (M : Metric-Extension l3 l4 P) + (y : type-metric-space-Metric-Extension P M) + (u v : cauchy-approximation-Pseudometric-Space P) + where + + lemma-sim-is-limit-map-cauchy-pseudocompletion-Metric-Extension : + is-limit-map-cauchy-pseudocompletion-Metric-Extension P M u y → + is-limit-map-cauchy-pseudocompletion-Metric-Extension P M v y → + sim-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space P) + ( u) + ( v) + lemma-sim-is-limit-map-cauchy-pseudocompletion-Metric-Extension lim-u lim-v = + reflects-sim-map-isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space P) + ( cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Extension P M)) + ( isometry-cauchy-pseudocompletion-Metric-Extension P M) + ( u) + ( v) + ( transitive-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Extension P M)) + ( map-cauchy-pseudocompletion-Metric-Extension P M u) + ( const-cauchy-approximation-Metric-Space + ( metric-space-Metric-Extension P M) + ( y)) + ( map-cauchy-pseudocompletion-Metric-Extension P M v) + ( symmetric-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Extension P M)) + ( map-cauchy-pseudocompletion-Metric-Extension P M v) + ( const-cauchy-approximation-Metric-Space + ( metric-space-Metric-Extension P M) + ( y)) + ( sim-const-is-limit-cauchy-approximation-Metric-Space + ( metric-space-Metric-Extension P M) + ( map-cauchy-pseudocompletion-Metric-Extension P M v) + ( y) + ( lim-v))) + ( sim-const-is-limit-cauchy-approximation-Metric-Space + ( metric-space-Metric-Extension P M) + ( map-cauchy-pseudocompletion-Metric-Extension P M u) + ( y) + ( lim-u))) +``` From d36ea7a609a94b7795acab5a1275f9ff1c5d2659 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sat, 22 Nov 2025 19:10:00 +0100 Subject: [PATCH 03/30] unused imports --- .../cauchy-approximations-metric-spaces.lagda.md | 4 ---- .../cauchy-pseudocompletion-of-metric-spaces.lagda.md | 5 ----- ...auchy-pseudocompletion-of-pseudometric-spaces.lagda.md | 8 -------- ...limits-of-cauchy-approximations-metric-spaces.lagda.md | 3 --- 4 files changed, 20 deletions(-) diff --git a/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md index d8bf919a55c..a6651165e3e 100644 --- a/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md @@ -10,9 +10,6 @@ module metric-spaces.cauchy-approximations-metric-spaces where open import elementary-number-theory.addition-positive-rational-numbers open import elementary-number-theory.positive-rational-numbers -open import foundation.constant-maps -open import foundation.dependent-pair-types -open import foundation.function-extensionality open import foundation.function-types open import foundation.homotopies open import foundation.identity-types @@ -20,7 +17,6 @@ open import foundation.propositions open import foundation.subtypes open import foundation.universe-levels -open import metric-spaces.cartesian-products-metric-spaces open import metric-spaces.cauchy-approximations-pseudometric-spaces open import metric-spaces.metric-spaces open import metric-spaces.short-functions-metric-spaces diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md index 2cdba77681c..62e4bac8a72 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md @@ -9,17 +9,13 @@ module metric-spaces.cauchy-pseudocompletion-of-metric-spaces where ```agda open import elementary-number-theory.addition-positive-rational-numbers open import elementary-number-theory.positive-rational-numbers -open import elementary-number-theory.strict-inequality-rational-numbers -open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.binary-relations -open import foundation.binary-transport open import foundation.dependent-pair-types open import foundation.function-types open import foundation.homotopies open import foundation.identity-types -open import foundation.propositions open import foundation.transport-along-identifications open import foundation.universe-levels @@ -27,7 +23,6 @@ open import metric-spaces.cauchy-approximations-metric-spaces open import metric-spaces.cauchy-approximations-pseudometric-spaces open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces open import metric-spaces.complete-metric-spaces -open import metric-spaces.convergent-cauchy-approximations-metric-spaces open import metric-spaces.functions-pseudometric-spaces open import metric-spaces.isometries-pseudometric-spaces open import metric-spaces.limits-of-cauchy-approximations-metric-spaces diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index d4b849e8777..05628e7f6cd 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -17,24 +17,16 @@ open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.binary-relations -open import foundation.binary-transport open import foundation.dependent-pair-types open import foundation.function-types -open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.transport-along-identifications open import foundation.universe-levels -open import metric-spaces.cauchy-approximations-metric-spaces open import metric-spaces.cauchy-approximations-pseudometric-spaces -open import metric-spaces.complete-metric-spaces -open import metric-spaces.convergent-cauchy-approximations-metric-spaces -open import metric-spaces.functions-pseudometric-spaces open import metric-spaces.isometries-pseudometric-spaces -open import metric-spaces.limits-of-cauchy-approximations-metric-spaces open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces -open import metric-spaces.metric-spaces open import metric-spaces.pseudometric-spaces open import metric-spaces.rational-neighborhood-relations open import metric-spaces.short-functions-pseudometric-spaces diff --git a/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md b/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md index d9a5fe6ea14..84a29eb976c 100644 --- a/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md +++ b/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md @@ -10,12 +10,9 @@ module metric-spaces.limits-of-cauchy-approximations-metric-spaces where open import elementary-number-theory.addition-positive-rational-numbers open import elementary-number-theory.positive-rational-numbers -open import foundation.dependent-pair-types open import foundation.function-types open import foundation.identity-types open import foundation.propositions -open import foundation.subtypes -open import foundation.transport-along-identifications open import foundation.universe-levels open import metric-spaces.cauchy-approximations-metric-spaces From 03c3e2bbe1f0d9e5ea6e1b17a2549f8eb18a6555 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sat, 22 Nov 2025 20:01:48 +0100 Subject: [PATCH 04/30] refactor --- ...extensions-of-pseudometric-spaces.lagda.md | 58 ++++++++++--------- ...y-of-elements-pseudometric-spaces.lagda.md | 14 ++++- 2 files changed, 44 insertions(+), 28 deletions(-) diff --git a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md index c6e0fe412fe..d826e58e519 100644 --- a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md @@ -177,25 +177,25 @@ module _ is-limit-map-cauchy-pseudocompletion-prop-Metric-Extension ``` -### Cauchy approximations converging to the same image in a metric extension are similar in the Cauchy pseudocompletion +### Similarity in the Cauchy pseudocompletion of a pseudometric space preserves and reflects limits in a metric extension ```agda module _ {l1 l2 l3 l4 : Level} (P : Pseudometric-Space l1 l2) (M : Metric-Extension l3 l4 P) - (y : type-metric-space-Metric-Extension P M) (u v : cauchy-approximation-Pseudometric-Space P) + (y : type-metric-space-Metric-Extension P M) where - lemma-sim-is-limit-map-cauchy-pseudocompletion-Metric-Extension : + sim-has-same-limit-map-cauchy-pseudocompletion-Metric-Extension : is-limit-map-cauchy-pseudocompletion-Metric-Extension P M u y → is-limit-map-cauchy-pseudocompletion-Metric-Extension P M v y → sim-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space P) ( u) ( v) - lemma-sim-is-limit-map-cauchy-pseudocompletion-Metric-Extension lim-u lim-v = + sim-has-same-limit-map-cauchy-pseudocompletion-Metric-Extension lim-u lim-v = reflects-sim-map-isometry-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space P) ( cauchy-pseudocompletion-Metric-Space @@ -203,29 +203,33 @@ module _ ( isometry-cauchy-pseudocompletion-Metric-Extension P M) ( u) ( v) - ( transitive-sim-Pseudometric-Space - ( cauchy-pseudocompletion-Metric-Space - ( metric-space-Metric-Extension P M)) + ( sim-has-same-limit-cauchy-approximation-Pseudometric-Space + ( pseudometric-space-Metric-Extension P M) ( map-cauchy-pseudocompletion-Metric-Extension P M u) - ( const-cauchy-approximation-Metric-Space - ( metric-space-Metric-Extension P M) - ( y)) ( map-cauchy-pseudocompletion-Metric-Extension P M v) - ( symmetric-sim-Pseudometric-Space - ( cauchy-pseudocompletion-Metric-Space - ( metric-space-Metric-Extension P M)) - ( map-cauchy-pseudocompletion-Metric-Extension P M v) - ( const-cauchy-approximation-Metric-Space - ( metric-space-Metric-Extension P M) - ( y)) - ( sim-const-is-limit-cauchy-approximation-Metric-Space - ( metric-space-Metric-Extension P M) - ( map-cauchy-pseudocompletion-Metric-Extension P M v) - ( y) - ( lim-v))) - ( sim-const-is-limit-cauchy-approximation-Metric-Space - ( metric-space-Metric-Extension P M) - ( map-cauchy-pseudocompletion-Metric-Extension P M u) - ( y) - ( lim-u))) + ( y) + ( lim-u) + ( lim-v)) + + has-same-limit-map-cauchy-sim-pseudocompletion-Metric-Extension : + sim-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space P) + ( u) + ( v) → + is-limit-map-cauchy-pseudocompletion-Metric-Extension P M u y → + is-limit-map-cauchy-pseudocompletion-Metric-Extension P M v y + has-same-limit-map-cauchy-sim-pseudocompletion-Metric-Extension u~v = + has-same-limit-sim-cauchy-approximation-Pseudometric-Space + ( pseudometric-space-Metric-Extension P M) + ( map-cauchy-pseudocompletion-Metric-Extension P M u) + ( map-cauchy-pseudocompletion-Metric-Extension P M v) + ( y) + ( preserves-sim-map-isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space P) + ( cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Extension P M)) + ( isometry-cauchy-pseudocompletion-Metric-Extension P M) + ( u) + ( v) + ( u~v)) ``` diff --git a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md index 168c7d67105..205dd76d739 100644 --- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md @@ -327,7 +327,7 @@ module _ is-short-map-short-function-Pseudometric-Space A B f d x y (x~y d) ``` -### Isometries between pseudometric spaces reflect similarity +### Isometries between pseudometric spaces preserve and reflect similarity ```agda module _ @@ -337,6 +337,18 @@ module _ ( f : isometry-Pseudometric-Space A B) where abstract + preserves-sim-map-isometry-Pseudometric-Space : + ( x y : type-Pseudometric-Space A) → + ( sim-Pseudometric-Space A x y) → + ( sim-Pseudometric-Space B + ( map-isometry-Pseudometric-Space A B f x) + ( map-isometry-Pseudometric-Space A B f y)) + preserves-sim-map-isometry-Pseudometric-Space = + preserves-sim-map-short-function-Pseudometric-Space + ( A) + ( B) + ( short-isometry-Pseudometric-Space A B f) + reflects-sim-map-isometry-Pseudometric-Space : ( x y : type-Pseudometric-Space A) → ( sim-Pseudometric-Space B From 7a21f12076c561bbac36b3e4cd8fb68d8c6857ec Mon Sep 17 00:00:00 2001 From: malarbol Date: Sat, 22 Nov 2025 21:28:03 +0100 Subject: [PATCH 05/30] isometries between metric extensions --- src/metric-spaces.lagda.md | 1 + ...extensions-of-pseudometric-spaces.lagda.md | 274 ++++++++++++++++++ ...extensions-of-pseudometric-spaces.lagda.md | 8 + 3 files changed, 283 insertions(+) create mode 100644 src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md index bb1b20c3bec..ee5c43ff9ae 100644 --- a/src/metric-spaces.lagda.md +++ b/src/metric-spaces.lagda.md @@ -97,6 +97,7 @@ open import metric-spaces.images-uniformly-continuous-functions-metric-spaces pu open import metric-spaces.indexed-sums-metric-spaces public open import metric-spaces.inhabited-totally-bounded-subspaces-metric-spaces public open import metric-spaces.interior-subsets-metric-spaces public +open import metric-spaces.isometries-between-metric-extensions-of-pseudometric-spaces public open import metric-spaces.isometries-metric-spaces public open import metric-spaces.isometries-pseudometric-spaces public open import metric-spaces.limits-of-cauchy-approximations-metric-spaces public diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md new file mode 100644 index 00000000000..6bb5f93e15e --- /dev/null +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -0,0 +1,274 @@ +# Isometries between metric extensions of a pseudometric space + +```agda +module metric-spaces.isometries-between-metric-extensions-of-pseudometric-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.strict-inequality-positive-rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.binary-relations +open import foundation.binary-transport +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.set-quotients +open import foundation.sets +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import metric-spaces.cauchy-approximations-metric-quotients-of-pseudometric-spaces +open import metric-spaces.cauchy-approximations-metric-spaces +open import metric-spaces.cauchy-approximations-pseudometric-spaces +open import metric-spaces.cauchy-pseudocompletion-of-metric-spaces +open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces +open import metric-spaces.complete-metric-spaces +open import metric-spaces.convergent-cauchy-approximations-metric-spaces +open import metric-spaces.equality-of-metric-spaces +open import metric-spaces.functions-metric-spaces +open import metric-spaces.functions-pseudometric-spaces +open import metric-spaces.isometries-metric-spaces +open import metric-spaces.isometries-pseudometric-spaces +open import metric-spaces.limits-of-cauchy-approximations-metric-spaces +open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces +open import metric-spaces.metric-extensions-of-pseudometric-spaces +open import metric-spaces.metric-quotients-of-pseudometric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.precategory-of-metric-spaces-and-short-functions +open import metric-spaces.pseudometric-spaces +open import metric-spaces.rational-neighborhood-relations +open import metric-spaces.short-functions-metric-spaces +open import metric-spaces.short-functions-pseudometric-spaces +open import metric-spaces.similarity-of-elements-pseudometric-spaces +``` + +
+ +## Idea + +Given a [pseudometric space](metric-spaces.pseudometric-spaces.md) `P`, an +{{#concept "isometry" Disambiguation="between metric extensions of a pseudometric space Agda=hom-isometry-Metric-Extension}} +between two +[metric extensions](metric-spaces.metric-extensions-of-pseudometric-spaces.md) +`i : P → M` and `j : P → N` of `P` is an +[isometry](metric-spaces.isometry-metric-spaces.md) `f : M → N` such that + +```text +f ∘ i ~ j. +``` + +## Definitions + +### The property of being an homomorphic isometry between metric extensions + +```agda +module _ + { l1 l2 l3 l4 l5 l6 : Level} + ( P : Pseudometric-Space l1 l2) + ( M : Metric-Extension l3 l4 P) + ( N : Metric-Extension l5 l6 P) + ( f : isometry-Metric-Space + ( metric-space-Metric-Extension P M) + ( metric-space-Metric-Extension P N)) + where + + is-hom-prop-isometry-metric-space-Metric-Extension : Prop (l1 ⊔ l5) + is-hom-prop-isometry-metric-space-Metric-Extension = + Π-Prop + ( type-Pseudometric-Space P) + ( λ x → + Id-Prop + ( set-Metric-Space + ( metric-space-Metric-Extension P N)) + ( map-isometry-Pseudometric-Space + ( P) + ( pseudometric-space-Metric-Extension P N) + ( comp-isometry-Pseudometric-Space + ( P) + ( pseudometric-space-Metric-Extension P M) + ( pseudometric-space-Metric-Extension P N) + ( f) + ( isometry-Metric-Extension P M)) + ( x)) + ( map-isometry-Metric-Extension P N x)) + + is-hom-isometry-metric-space-Metric-Extension : UU (l1 ⊔ l5) + is-hom-isometry-metric-space-Metric-Extension = + type-Prop is-hom-prop-isometry-metric-space-Metric-Extension + + is-prop-is-hom-isometry-metric-space-Metric-Extension : + is-prop is-hom-isometry-metric-space-Metric-Extension + is-prop-is-hom-isometry-metric-space-Metric-Extension = + is-prop-type-Prop is-hom-prop-isometry-metric-space-Metric-Extension +``` + +### The type of isometries between metric extensions of a pseudometric space + +```agda +module _ + { l1 l2 l3 l4 l5 l6 : Level} + ( P : Pseudometric-Space l1 l2) + ( M : Metric-Extension l3 l4 P) + ( N : Metric-Extension l5 l6 P) + where + + hom-isometry-Metric-Extension : UU (l1 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) + hom-isometry-Metric-Extension = + type-subtype + ( is-hom-prop-isometry-metric-space-Metric-Extension P M N) + +module _ + { l1 l2 l3 l4 l5 l6 : Level} + ( P : Pseudometric-Space l1 l2) + ( M : Metric-Extension l3 l4 P) + ( N : Metric-Extension l5 l6 P) + ( f : hom-isometry-Metric-Extension P M N) + where + + isometry-metric-space-hom-isometry-Metric-Extension : + isometry-Metric-Space + ( metric-space-Metric-Extension P M) + ( metric-space-Metric-Extension P N) + isometry-metric-space-hom-isometry-Metric-Extension = pr1 f + + map-metric-space-hom-isometry-Metric-Extension : + type-metric-space-Metric-Extension P M → + type-metric-space-Metric-Extension P N + map-metric-space-hom-isometry-Metric-Extension = + map-isometry-Metric-Space + ( metric-space-Metric-Extension P M) + ( metric-space-Metric-Extension P N) + ( isometry-metric-space-hom-isometry-Metric-Extension) + + is-isometry-map-metric-space-hom-isometry-Metric-Extension : + is-isometry-Metric-Space + ( metric-space-Metric-Extension P M) + ( metric-space-Metric-Extension P N) + ( map-metric-space-hom-isometry-Metric-Extension) + is-isometry-map-metric-space-hom-isometry-Metric-Extension = + is-isometry-map-isometry-Metric-Space + ( metric-space-Metric-Extension P M) + ( metric-space-Metric-Extension P N) + ( isometry-metric-space-hom-isometry-Metric-Extension) + + is-hom-isometry-metric-space-hom-isometry-Metric-Extension : + ( ( map-metric-space-hom-isometry-Metric-Extension) ∘ + ( map-isometry-Metric-Extension P M)) ~ + ( map-isometry-Metric-Extension P N) + is-hom-isometry-metric-space-hom-isometry-Metric-Extension = pr2 f +``` + +## Properties + +### The identity isometry of a metric extension + +```agda +module _ + {l1 l2 l3 l4 : Level} + (P : Pseudometric-Space l1 l2) + (M : Metric-Extension l3 l4 P) + where + + isometry-id-metric-space-Metric-Extension : + isometry-Metric-Space + ( metric-space-Metric-Extension P M) + ( metric-space-Metric-Extension P M) + isometry-id-metric-space-Metric-Extension = + isometry-id-Metric-Space (metric-space-Metric-Extension P M) + + is-hom-isometry-id-metric-space-Metric-Extension : + is-hom-isometry-metric-space-Metric-Extension P M M + ( isometry-id-metric-space-Metric-Extension) + is-hom-isometry-id-metric-space-Metric-Extension x = + refl + + id-hom-isometry-Metric-Extension : hom-isometry-Metric-Extension P M M + id-hom-isometry-Metric-Extension = + ( isometry-id-metric-space-Metric-Extension , + is-hom-isometry-id-metric-space-Metric-Extension) +``` + +### Composition of isometries between metric extensions + +```agda +module _ + {l l' lu lu' lv lv' lw lw' : Level} + (P : Pseudometric-Space l l') + (U : Metric-Extension lu lu' P) + (V : Metric-Extension lv lv' P) + (W : Metric-Extension lw lw' P) + (g : hom-isometry-Metric-Extension P V W) + (f : hom-isometry-Metric-Extension P U V) + where + + abstract + is-hom-comp-hom-isometry-Metric-Extension : + is-hom-isometry-metric-space-Metric-Extension P U W + ( comp-isometry-Metric-Space + ( metric-space-Metric-Extension P U) + ( metric-space-Metric-Extension P V) + ( metric-space-Metric-Extension P W) + ( isometry-metric-space-hom-isometry-Metric-Extension P V W g) + ( isometry-metric-space-hom-isometry-Metric-Extension P U V f)) + is-hom-comp-hom-isometry-Metric-Extension x = + ( ap + ( map-metric-space-hom-isometry-Metric-Extension P V W g) + ( is-hom-isometry-metric-space-hom-isometry-Metric-Extension + ( P) + ( U) + ( V) + ( f) + ( x))) ∙ + ( is-hom-isometry-metric-space-hom-isometry-Metric-Extension P V W g x) + + comp-hom-isometry-Metric-Extension : hom-isometry-Metric-Extension P U W + pr1 comp-hom-isometry-Metric-Extension = + comp-isometry-Metric-Space + ( metric-space-Metric-Extension P U) + ( metric-space-Metric-Extension P V) + ( metric-space-Metric-Extension P W) + ( isometry-metric-space-hom-isometry-Metric-Extension P V W g) + ( isometry-metric-space-hom-isometry-Metric-Extension P U V f) + pr2 comp-hom-isometry-Metric-Extension = + is-hom-comp-hom-isometry-Metric-Extension +``` + +### Homotopic isometries between metric extensions are equal + +```agda +module _ + { l1 l2 l3 l4 l5 l6 : Level} + ( P : Pseudometric-Space l1 l2) + ( M : Metric-Extension l3 l4 P) + ( N : Metric-Extension l5 l6 P) + ( f g : hom-isometry-Metric-Extension P M N) + ( f~g : + map-metric-space-hom-isometry-Metric-Extension P M N f ~ + map-metric-space-hom-isometry-Metric-Extension P M N g) + where + + eq-htpy-map-metric-space-hom-isometry-Metric-Extension : f ＝ g + eq-htpy-map-metric-space-hom-isometry-Metric-Extension = + eq-type-subtype + ( is-hom-prop-isometry-metric-space-Metric-Extension P M N) + ( eq-htpy-map-isometry-Metric-Space + ( metric-space-Metric-Extension P M) + ( metric-space-Metric-Extension P N) + ( isometry-metric-space-hom-isometry-Metric-Extension P M N f) + ( isometry-metric-space-hom-isometry-Metric-Extension P M N g) + ( f~g)) +``` diff --git a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md index d826e58e519..ed49a0ca2ee 100644 --- a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md @@ -99,6 +99,14 @@ module _ isometry-Metric-Extension : isometry-Pseudometric-Space P pseudometric-space-Metric-Extension isometry-Metric-Extension = pr2 M + + map-isometry-Metric-Extension : + type-Pseudometric-Space P → type-metric-space-Metric-Extension + map-isometry-Metric-Extension = + map-isometry-Pseudometric-Space + ( P) + ( pseudometric-space-Metric-Extension) + ( isometry-Metric-Extension) ``` ## Properties From 4afd6bdf7152e15544bc35d9a36a45ff5c9b7fa0 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sat, 22 Nov 2025 21:34:12 +0100 Subject: [PATCH 06/30] fix link --- ...es-between-metric-extensions-of-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md index 6bb5f93e15e..01fd43e8c8e 100644 --- a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -65,7 +65,7 @@ Given a [pseudometric space](metric-spaces.pseudometric-spaces.md) `P`, an between two [metric extensions](metric-spaces.metric-extensions-of-pseudometric-spaces.md) `i : P → M` and `j : P → N` of `P` is an -[isometry](metric-spaces.isometry-metric-spaces.md) `f : M → N` such that +[isometry](metric-spaces.isometries-metric-spaces.md) `f : M → N` such that ```text f ∘ i ~ j. From 9fe2c5f02c2e9bcd84723f0b6ae83d6cf5548855 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sat, 22 Nov 2025 21:43:09 +0100 Subject: [PATCH 07/30] rephrase header --- ...between-metric-extensions-of-pseudometric-spaces.lagda.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md index 01fd43e8c8e..33bdd7b1924 100644 --- a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -60,11 +60,12 @@ open import metric-spaces.similarity-of-elements-pseudometric-spaces ## Idea -Given a [pseudometric space](metric-spaces.pseudometric-spaces.md) `P`, an +An {{#concept "isometry" Disambiguation="between metric extensions of a pseudometric space Agda=hom-isometry-Metric-Extension}} between two [metric extensions](metric-spaces.metric-extensions-of-pseudometric-spaces.md) -`i : P → M` and `j : P → N` of `P` is an +`(M , i : P → M)` and `(N , j : P → N)` of a +[pseudometric space](metric-spaces.pseudometric-spaces.md) `P` is an [isometry](metric-spaces.isometries-metric-spaces.md) `f : M → N` such that ```text From e3d49e863bf598f0596908f6fd37aae22d26eef9 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 23 Nov 2025 15:32:28 +0100 Subject: [PATCH 08/30] eq-prop-Metric-Space --- src/metric-spaces/metric-spaces.lagda.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/metric-spaces/metric-spaces.lagda.md b/src/metric-spaces/metric-spaces.lagda.md index 25fbe2e9822..36aac194256 100644 --- a/src/metric-spaces/metric-spaces.lagda.md +++ b/src/metric-spaces/metric-spaces.lagda.md @@ -317,6 +317,10 @@ module _ set-Metric-Space : Set l1 set-Metric-Space = (type-Metric-Space A , is-set-type-Metric-Space) + + eq-prop-Metric-Space : + (x y : type-Metric-Space A) → Prop l1 + eq-prop-Metric-Space = Id-Prop set-Metric-Space ``` ### Similarity of elements in a metric space is equivalent to equality From 83610c8a9a48178f8dca3bcc16222bb0d595bf79 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 23 Nov 2025 15:44:40 +0100 Subject: [PATCH 09/30] Update src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- ...es-between-metric-extensions-of-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md index 33bdd7b1924..903f82f5196 100644 --- a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -61,7 +61,7 @@ open import metric-spaces.similarity-of-elements-pseudometric-spaces ## Idea An -{{#concept "isometry" Disambiguation="between metric extensions of a pseudometric space Agda=hom-isometry-Metric-Extension}} +{{#concept "isometry" Disambiguation="between metric extensions of a pseudometric space" Agda=hom-isometry-Metric-Extension}} between two [metric extensions](metric-spaces.metric-extensions-of-pseudometric-spaces.md) `(M , i : P → M)` and `(N , j : P → N)` of a From 57e8c8072a4c404859fd6a58062e66cb34527b4b Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 23 Nov 2025 15:45:04 +0100 Subject: [PATCH 10/30] Update src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- ...s-between-metric-extensions-of-pseudometric-spaces.lagda.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md index 903f82f5196..07e640ac767 100644 --- a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -64,8 +64,7 @@ An {{#concept "isometry" Disambiguation="between metric extensions of a pseudometric space" Agda=hom-isometry-Metric-Extension}} between two [metric extensions](metric-spaces.metric-extensions-of-pseudometric-spaces.md) -`(M , i : P → M)` and `(N , j : P → N)` of a -[pseudometric space](metric-spaces.pseudometric-spaces.md) `P` is an +of a [pseudometric space](metric-spaces.pseudometric-spaces.md) `P`, `i : P → M` and `j : P → N`, is an [isometry](metric-spaces.isometries-metric-spaces.md) `f : M → N` such that ```text From f955463ded1a4d9038d5d5157224c3c85b722aff Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 23 Nov 2025 15:45:34 +0100 Subject: [PATCH 11/30] Update src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- ...tween-metric-extensions-of-pseudometric-spaces.lagda.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md index 07e640ac767..b59d21142f0 100644 --- a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -81,9 +81,10 @@ module _ ( P : Pseudometric-Space l1 l2) ( M : Metric-Extension l3 l4 P) ( N : Metric-Extension l5 l6 P) - ( f : isometry-Metric-Space - ( metric-space-Metric-Extension P M) - ( metric-space-Metric-Extension P N)) + ( f : + isometry-Metric-Space + ( metric-space-Metric-Extension P M) + ( metric-space-Metric-Extension P N)) where is-hom-prop-isometry-metric-space-Metric-Extension : Prop (l1 ⊔ l5) From 898e0b053786b2d42f469cfdac973c49fbf552a6 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 23 Nov 2025 15:46:54 +0100 Subject: [PATCH 12/30] Update src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- ...es-between-metric-extensions-of-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md index b59d21142f0..f0de5f38221 100644 --- a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -68,7 +68,7 @@ of a [pseudometric space](metric-spaces.pseudometric-spaces.md) `P`, `i : P → [isometry](metric-spaces.isometries-metric-spaces.md) `f : M → N` such that ```text -f ∘ i ~ j. + f ∘ i ~ j. ``` ## Definitions From 7e0a1f34555220206752a908aba053660a2f1df9 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 23 Nov 2025 15:44:17 +0100 Subject: [PATCH 13/30] fix names --- ...-pseudocompletion-of-metric-spaces.lagda.md | 6 +++--- ...ocompletion-of-pseudometric-spaces.lagda.md | 18 +++++++++--------- ...c-quotients-of-pseudometric-spaces.lagda.md | 5 +---- 3 files changed, 13 insertions(+), 16 deletions(-) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md index 62e4bac8a72..7be8a045c4c 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md @@ -442,7 +442,7 @@ module _ where abstract - reflects-neighborhood-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space : + reflects-neighborhoods-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space : (δ : ℚ⁺) → (u v : cauchy-approximation-Metric-Space M) → neighborhood-Metric-Space @@ -461,7 +461,7 @@ module _ ( δ) ( u) ( v) - reflects-neighborhood-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + reflects-neighborhoods-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space δ x y Nδ = reflects-neighborhood-sim-Pseudometric-Space ( cauchy-pseudocompletion-Metric-Space M) @@ -517,7 +517,7 @@ module _ ( d) ( x) ( y)) , - ( reflects-neighborhood-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space + ( reflects-neighborhoods-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space ( d) ( x) ( y))) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index 05628e7f6cd..cf682cb3e8c 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -730,7 +730,7 @@ module _ where abstract - reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : + reflects-neighborhoods-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : ( d : ℚ⁺) → ( u v : cauchy-approximation-Pseudometric-Space @@ -750,7 +750,7 @@ module _ ( d) ( u) ( v) - reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + reflects-neighborhoods-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space d u v N-lim = reflects-neighborhood-sim-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space @@ -798,7 +798,7 @@ module _ ( d) ( x) ( y)) , - ( reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + ( reflects-neighborhoods-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( d) ( x) ( y))) @@ -853,7 +853,7 @@ module _ (f : isometry-Pseudometric-Space A B) where abstract - preserves-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space : + preserves-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space : (d : ℚ⁺) → (x y : cauchy-approximation-Pseudometric-Space A) → neighborhood-Pseudometric-Space @@ -866,13 +866,13 @@ module _ ( d) ( map-cauchy-approximation-isometry-Pseudometric-Space A B f x) ( map-cauchy-approximation-isometry-Pseudometric-Space A B f y) - preserves-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space = + preserves-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space = is-short-map-cauchy-approximation-short-function-Pseudometric-Space ( A) ( B) ( short-isometry-Pseudometric-Space A B f) - reflects-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space : + reflects-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space : (d : ℚ⁺) → (x y : cauchy-approximation-Pseudometric-Space A) → neighborhood-Pseudometric-Space @@ -885,7 +885,7 @@ module _ ( d) ( x) ( y) - reflects-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space + reflects-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space d x y Nxy α β = reflects-neighborhood-map-isometry-Pseudometric-Space ( A) @@ -902,11 +902,11 @@ module _ ( cauchy-pseudocompletion-Pseudometric-Space B) ( map-cauchy-approximation-isometry-Pseudometric-Space A B f) is-isometry-map-cauchy-approximation-isometry-Pseudometric-Space d x y = - ( ( preserves-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space + ( ( preserves-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space ( d) ( x) ( y)) , - ( reflects-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space + ( reflects-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space ( d) ( x) ( y))) diff --git a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md index 3f48274856b..fb63b3dccab 100644 --- a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md @@ -390,10 +390,7 @@ module _ eq-map-is-in-class-metric-quotient-Pseudometric-Space : (X : type-metric-quotient-Pseudometric-Space M) → {x : type-Pseudometric-Space M} → - is-in-class-metric-quotient-Pseudometric-Space - ( M) - ( X) - ( x) → + is-in-class-metric-quotient-Pseudometric-Space M X x → map-metric-quotient-Pseudometric-Space x ＝ X eq-map-is-in-class-metric-quotient-Pseudometric-Space X {x} x∈X = eq-set-quotient-equivalence-class-set-quotient From 621ab658077b297a54dfd254c2e689971c5803c5 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 23 Nov 2025 16:33:03 +0100 Subject: [PATCH 14/30] fix names `isometry-Metric-Extension` --- ...extensions-of-pseudometric-spaces.lagda.md | 164 ++++++++++-------- ...extensions-of-pseudometric-spaces.lagda.md | 12 +- 2 files changed, 93 insertions(+), 83 deletions(-) diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md index f0de5f38221..55f4236e4c3 100644 --- a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -61,11 +61,12 @@ open import metric-spaces.similarity-of-elements-pseudometric-spaces ## Idea An -{{#concept "isometry" Disambiguation="between metric extensions of a pseudometric space" Agda=hom-isometry-Metric-Extension}} +{{#concept "isometry" Disambiguation="between metric extensions of a pseudometric space" Agda=isometry-Metric-Extension}} between two [metric extensions](metric-spaces.metric-extensions-of-pseudometric-spaces.md) -of a [pseudometric space](metric-spaces.pseudometric-spaces.md) `P`, `i : P → M` and `j : P → N`, is an -[isometry](metric-spaces.isometries-metric-spaces.md) `f : M → N` such that +of a [pseudometric space](metric-spaces.pseudometric-spaces.md) `P`, `i : P → M` +and `j : P → N`, is an [isometry](metric-spaces.isometries-metric-spaces.md) +`f : M → N` such that ```text f ∘ i ~ j. @@ -73,7 +74,7 @@ of a [pseudometric space](metric-spaces.pseudometric-spaces.md) `P`, `i : P → ## Definitions -### The property of being an homomorphic isometry between metric extensions +### The property of being an isometry between metric extensions ```agda module _ @@ -87,8 +88,9 @@ module _ ( metric-space-Metric-Extension P N)) where - is-hom-prop-isometry-metric-space-Metric-Extension : Prop (l1 ⊔ l5) - is-hom-prop-isometry-metric-space-Metric-Extension = + coherence-triangle-prop-isometry-metric-space-Metric-Extension : + Prop (l1 ⊔ l5) + coherence-triangle-prop-isometry-metric-space-Metric-Extension = Π-Prop ( type-Pseudometric-Space P) ( λ x → @@ -103,18 +105,20 @@ module _ ( pseudometric-space-Metric-Extension P M) ( pseudometric-space-Metric-Extension P N) ( f) - ( isometry-Metric-Extension P M)) + ( isometry-metric-space-Metric-Extension P M)) ( x)) - ( map-isometry-Metric-Extension P N x)) - - is-hom-isometry-metric-space-Metric-Extension : UU (l1 ⊔ l5) - is-hom-isometry-metric-space-Metric-Extension = - type-Prop is-hom-prop-isometry-metric-space-Metric-Extension - - is-prop-is-hom-isometry-metric-space-Metric-Extension : - is-prop is-hom-isometry-metric-space-Metric-Extension - is-prop-is-hom-isometry-metric-space-Metric-Extension = - is-prop-type-Prop is-hom-prop-isometry-metric-space-Metric-Extension + ( map-isometry-metric-space-Metric-Extension P N x)) + + coherence-triangle-isometry-metric-space-Metric-Extension : UU (l1 ⊔ l5) + coherence-triangle-isometry-metric-space-Metric-Extension = + type-Prop + coherence-triangle-prop-isometry-metric-space-Metric-Extension + + is-prop-coherence-triangle-isometry-metric-space-Metric-Extension : + is-prop coherence-triangle-isometry-metric-space-Metric-Extension + is-prop-coherence-triangle-isometry-metric-space-Metric-Extension = + is-prop-type-Prop + coherence-triangle-prop-isometry-metric-space-Metric-Extension ``` ### The type of isometries between metric extensions of a pseudometric space @@ -127,50 +131,52 @@ module _ ( N : Metric-Extension l5 l6 P) where - hom-isometry-Metric-Extension : UU (l1 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) - hom-isometry-Metric-Extension = + isometry-Metric-Extension : UU (l1 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) + isometry-Metric-Extension = type-subtype - ( is-hom-prop-isometry-metric-space-Metric-Extension P M N) + ( coherence-triangle-prop-isometry-metric-space-Metric-Extension P M N) module _ { l1 l2 l3 l4 l5 l6 : Level} ( P : Pseudometric-Space l1 l2) ( M : Metric-Extension l3 l4 P) ( N : Metric-Extension l5 l6 P) - ( f : hom-isometry-Metric-Extension P M N) + ( f : isometry-Metric-Extension P M N) where - isometry-metric-space-hom-isometry-Metric-Extension : + isometry-metric-space-isometry-Metric-Extension : isometry-Metric-Space ( metric-space-Metric-Extension P M) ( metric-space-Metric-Extension P N) - isometry-metric-space-hom-isometry-Metric-Extension = pr1 f + isometry-metric-space-isometry-Metric-Extension = pr1 f - map-metric-space-hom-isometry-Metric-Extension : + map-metric-space-isometry-Metric-Extension : type-metric-space-Metric-Extension P M → type-metric-space-Metric-Extension P N - map-metric-space-hom-isometry-Metric-Extension = + map-metric-space-isometry-Metric-Extension = map-isometry-Metric-Space ( metric-space-Metric-Extension P M) ( metric-space-Metric-Extension P N) - ( isometry-metric-space-hom-isometry-Metric-Extension) + ( isometry-metric-space-isometry-Metric-Extension) - is-isometry-map-metric-space-hom-isometry-Metric-Extension : + is-isometry-map-metric-space-isometry-Metric-Extension : is-isometry-Metric-Space ( metric-space-Metric-Extension P M) ( metric-space-Metric-Extension P N) - ( map-metric-space-hom-isometry-Metric-Extension) - is-isometry-map-metric-space-hom-isometry-Metric-Extension = + ( map-metric-space-isometry-Metric-Extension) + is-isometry-map-metric-space-isometry-Metric-Extension = is-isometry-map-isometry-Metric-Space ( metric-space-Metric-Extension P M) ( metric-space-Metric-Extension P N) - ( isometry-metric-space-hom-isometry-Metric-Extension) - - is-hom-isometry-metric-space-hom-isometry-Metric-Extension : - ( ( map-metric-space-hom-isometry-Metric-Extension) ∘ - ( map-isometry-Metric-Extension P M)) ~ - ( map-isometry-Metric-Extension P N) - is-hom-isometry-metric-space-hom-isometry-Metric-Extension = pr2 f + ( isometry-metric-space-isometry-Metric-Extension) + + coh-triangle-isometry-metric-space-isometry-Metric-Extension : + coherence-triangle-isometry-metric-space-Metric-Extension + ( P) + ( M) + ( N) + ( isometry-metric-space-isometry-Metric-Extension) + coh-triangle-isometry-metric-space-isometry-Metric-Extension = pr2 f ``` ## Properties @@ -184,23 +190,11 @@ module _ (M : Metric-Extension l3 l4 P) where - isometry-id-metric-space-Metric-Extension : - isometry-Metric-Space + id-isometry-Metric-Extension : isometry-Metric-Extension P M M + pr1 id-isometry-Metric-Extension = + isometry-id-Metric-Space ( metric-space-Metric-Extension P M) - ( metric-space-Metric-Extension P M) - isometry-id-metric-space-Metric-Extension = - isometry-id-Metric-Space (metric-space-Metric-Extension P M) - - is-hom-isometry-id-metric-space-Metric-Extension : - is-hom-isometry-metric-space-Metric-Extension P M M - ( isometry-id-metric-space-Metric-Extension) - is-hom-isometry-id-metric-space-Metric-Extension x = - refl - - id-hom-isometry-Metric-Extension : hom-isometry-Metric-Extension P M M - id-hom-isometry-Metric-Extension = - ( isometry-id-metric-space-Metric-Extension , - is-hom-isometry-id-metric-space-Metric-Extension) + pr2 id-isometry-Metric-Extension = refl-htpy ``` ### Composition of isometries between metric extensions @@ -212,40 +206,39 @@ module _ (U : Metric-Extension lu lu' P) (V : Metric-Extension lv lv' P) (W : Metric-Extension lw lw' P) - (g : hom-isometry-Metric-Extension P V W) - (f : hom-isometry-Metric-Extension P U V) + (g : isometry-Metric-Extension P V W) + (f : isometry-Metric-Extension P U V) where abstract - is-hom-comp-hom-isometry-Metric-Extension : - is-hom-isometry-metric-space-Metric-Extension P U W + coh-comp-isometry-Metric-Extension : + coherence-triangle-isometry-metric-space-Metric-Extension P U W ( comp-isometry-Metric-Space ( metric-space-Metric-Extension P U) ( metric-space-Metric-Extension P V) ( metric-space-Metric-Extension P W) - ( isometry-metric-space-hom-isometry-Metric-Extension P V W g) - ( isometry-metric-space-hom-isometry-Metric-Extension P U V f)) - is-hom-comp-hom-isometry-Metric-Extension x = + ( isometry-metric-space-isometry-Metric-Extension P V W g) + ( isometry-metric-space-isometry-Metric-Extension P U V f)) + coh-comp-isometry-Metric-Extension x = ( ap - ( map-metric-space-hom-isometry-Metric-Extension P V W g) - ( is-hom-isometry-metric-space-hom-isometry-Metric-Extension + ( map-metric-space-isometry-Metric-Extension P V W g) + ( coh-triangle-isometry-metric-space-isometry-Metric-Extension ( P) ( U) ( V) ( f) ( x))) ∙ - ( is-hom-isometry-metric-space-hom-isometry-Metric-Extension P V W g x) + ( coh-triangle-isometry-metric-space-isometry-Metric-Extension P V W g x) - comp-hom-isometry-Metric-Extension : hom-isometry-Metric-Extension P U W - pr1 comp-hom-isometry-Metric-Extension = + comp-isometry-Metric-Extension : isometry-Metric-Extension P U W + pr1 comp-isometry-Metric-Extension = comp-isometry-Metric-Space ( metric-space-Metric-Extension P U) ( metric-space-Metric-Extension P V) ( metric-space-Metric-Extension P W) - ( isometry-metric-space-hom-isometry-Metric-Extension P V W g) - ( isometry-metric-space-hom-isometry-Metric-Extension P U V f) - pr2 comp-hom-isometry-Metric-Extension = - is-hom-comp-hom-isometry-Metric-Extension + ( isometry-metric-space-isometry-Metric-Extension P V W g) + ( isometry-metric-space-isometry-Metric-Extension P U V f) + pr2 comp-isometry-Metric-Extension = coh-comp-isometry-Metric-Extension ``` ### Homotopic isometries between metric extensions are equal @@ -256,20 +249,37 @@ module _ ( P : Pseudometric-Space l1 l2) ( M : Metric-Extension l3 l4 P) ( N : Metric-Extension l5 l6 P) - ( f g : hom-isometry-Metric-Extension P M N) - ( f~g : - map-metric-space-hom-isometry-Metric-Extension P M N f ~ - map-metric-space-hom-isometry-Metric-Extension P M N g) + ( f g : isometry-Metric-Extension P M N) where - eq-htpy-map-metric-space-hom-isometry-Metric-Extension : f ＝ g - eq-htpy-map-metric-space-hom-isometry-Metric-Extension = + htpy-isometry-Metric-Extension : UU (l3 ⊔ l5) + htpy-isometry-Metric-Extension = + ( map-metric-space-isometry-Metric-Extension P M N f ~ + map-metric-space-isometry-Metric-Extension P M N g) + + is-prop-htpy-isometry-Metric-Extension : + is-prop htpy-isometry-Metric-Extension + is-prop-htpy-isometry-Metric-Extension = + is-prop-Π + ( λ x → + is-set-type-Metric-Space + ( metric-space-Metric-Extension P N) + ( map-metric-space-isometry-Metric-Extension P M N f x) + ( map-metric-space-isometry-Metric-Extension P M N g x)) + + htpy-prop-isometry-Metric-Extension : Prop (l3 ⊔ l5) + htpy-prop-isometry-Metric-Extension = + ( htpy-isometry-Metric-Extension , is-prop-htpy-isometry-Metric-Extension) + + eq-htpy-isometry-Metric-Extension : + htpy-isometry-Metric-Extension → f ＝ g + eq-htpy-isometry-Metric-Extension f~g = eq-type-subtype - ( is-hom-prop-isometry-metric-space-Metric-Extension P M N) + ( coherence-triangle-prop-isometry-metric-space-Metric-Extension P M N) ( eq-htpy-map-isometry-Metric-Space ( metric-space-Metric-Extension P M) ( metric-space-Metric-Extension P N) - ( isometry-metric-space-hom-isometry-Metric-Extension P M N f) - ( isometry-metric-space-hom-isometry-Metric-Extension P M N g) + ( isometry-metric-space-isometry-Metric-Extension P M N f) + ( isometry-metric-space-isometry-Metric-Extension P M N g) ( f~g)) ``` diff --git a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md index ed49a0ca2ee..73ff78856c9 100644 --- a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md @@ -96,17 +96,17 @@ module _ type-metric-space-Metric-Extension = type-Metric-Space metric-space-Metric-Extension - isometry-Metric-Extension : + isometry-metric-space-Metric-Extension : isometry-Pseudometric-Space P pseudometric-space-Metric-Extension - isometry-Metric-Extension = pr2 M + isometry-metric-space-Metric-Extension = pr2 M - map-isometry-Metric-Extension : + map-isometry-metric-space-Metric-Extension : type-Pseudometric-Space P → type-metric-space-Metric-Extension - map-isometry-Metric-Extension = + map-isometry-metric-space-Metric-Extension = map-isometry-Pseudometric-Space ( P) ( pseudometric-space-Metric-Extension) - ( isometry-Metric-Extension) + ( isometry-metric-space-Metric-Extension) ``` ## Properties @@ -128,7 +128,7 @@ module _ isometry-map-cauchy-approximation-isometry-Pseudometric-Space ( P) ( pseudometric-space-Metric-Extension P M) - ( isometry-Metric-Extension P M) + ( isometry-metric-space-Metric-Extension P M) map-cauchy-pseudocompletion-Metric-Extension : cauchy-approximation-Pseudometric-Space P → From aebfd7eef46347948c8b646543deabd273bcb98c Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 23 Nov 2025 16:41:42 +0100 Subject: [PATCH 15/30] shorter name --- ...ween-metric-extensions-of-pseudometric-spaces.lagda.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md index 55f4236e4c3..f4f5c3d59d8 100644 --- a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -170,13 +170,13 @@ module _ ( metric-space-Metric-Extension P N) ( isometry-metric-space-isometry-Metric-Extension) - coh-triangle-isometry-metric-space-isometry-Metric-Extension : + coh-isometry-Metric-Extension : coherence-triangle-isometry-metric-space-Metric-Extension ( P) ( M) ( N) ( isometry-metric-space-isometry-Metric-Extension) - coh-triangle-isometry-metric-space-isometry-Metric-Extension = pr2 f + coh-isometry-Metric-Extension = pr2 f ``` ## Properties @@ -222,13 +222,13 @@ module _ coh-comp-isometry-Metric-Extension x = ( ap ( map-metric-space-isometry-Metric-Extension P V W g) - ( coh-triangle-isometry-metric-space-isometry-Metric-Extension + ( coh-isometry-Metric-Extension ( P) ( U) ( V) ( f) ( x))) ∙ - ( coh-triangle-isometry-metric-space-isometry-Metric-Extension P V W g x) + ( coh-isometry-Metric-Extension P V W g x) comp-isometry-Metric-Extension : isometry-Metric-Extension P U W pr1 comp-isometry-Metric-Extension = From 19e422691c39f9ec810d306256b565a8f3a60841 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 23 Nov 2025 17:32:31 +0100 Subject: [PATCH 16/30] initial metric extensions --- src/metric-spaces.lagda.md | 1 + ...extensions-of-pseudometric-spaces.lagda.md | 244 ++++++++++++++++++ 2 files changed, 245 insertions(+) create mode 100644 src/metric-spaces/initial-metric-extensions-of-pseudometric-spaces.lagda.md diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md index ee5c43ff9ae..06819b5946b 100644 --- a/src/metric-spaces.lagda.md +++ b/src/metric-spaces.lagda.md @@ -96,6 +96,7 @@ open import metric-spaces.images-short-functions-metric-spaces public open import metric-spaces.images-uniformly-continuous-functions-metric-spaces public open import metric-spaces.indexed-sums-metric-spaces public open import metric-spaces.inhabited-totally-bounded-subspaces-metric-spaces public +open import metric-spaces.initial-metric-extensions-of-pseudometric-spaces public open import metric-spaces.interior-subsets-metric-spaces public open import metric-spaces.isometries-between-metric-extensions-of-pseudometric-spaces public open import metric-spaces.isometries-metric-spaces public diff --git a/src/metric-spaces/initial-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/initial-metric-extensions-of-pseudometric-spaces.lagda.md new file mode 100644 index 00000000000..abd240058f3 --- /dev/null +++ b/src/metric-spaces/initial-metric-extensions-of-pseudometric-spaces.lagda.md @@ -0,0 +1,244 @@ +# Initial metric extensions of pseudometric spaces + +```agda +{-# OPTIONS --lossy-unification #-} + +module metric-spaces.initial-metric-extensions-of-pseudometric-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.binary-relations +open import foundation.binary-transport +open import foundation.contractible-maps +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.equivalence-classes +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.fibers-of-maps +open import foundation.function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.inhabited-subtypes +open import foundation.logical-equivalences +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.reflecting-maps-equivalence-relations +open import foundation.retractions +open import foundation.sections +open import foundation.set-quotients +open import foundation.sets +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universal-property-set-quotients +open import foundation.universe-levels + +open import logic.functoriality-existential-quantification + +open import metric-spaces.cauchy-approximations-metric-spaces +open import metric-spaces.cauchy-approximations-pseudometric-spaces +open import metric-spaces.convergent-cauchy-approximations-metric-spaces +open import metric-spaces.equality-of-metric-spaces +open import metric-spaces.extensionality-pseudometric-spaces +open import metric-spaces.functions-metric-spaces +open import metric-spaces.isometries-between-metric-extensions-of-pseudometric-spaces +open import metric-spaces.isometries-metric-spaces +open import metric-spaces.isometries-pseudometric-spaces +open import metric-spaces.limits-of-cauchy-approximations-metric-spaces +open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces +open import metric-spaces.metric-extensions-of-pseudometric-spaces +open import metric-spaces.metric-quotients-of-pseudometric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.pseudometric-spaces +open import metric-spaces.rational-neighborhood-relations +open import metric-spaces.short-functions-metric-spaces +open import metric-spaces.short-functions-pseudometric-spaces +open import metric-spaces.similarity-of-elements-pseudometric-spaces +``` + +
+ +## Idea + +The [metric quotient](metric-spaces.metric-quotients-of-pseudometric-spaces.md) +of a [pseudometric space](metric-spaces.pseudometric-spaces.md) is the +{{concept "initial metric extension" Agda=initial-Metric-Extension}}: for any +metric extension `i : P → M` of a pseudometric space `P`, there exists a unique +[isometry of metric extensions](metric-spaces.isometries-between-metric-extensions-of-pseudometric-spaces.md) +`f : [P] → M`. + +## Definitions + +### The initial metric extension of a pseudometric space + +```agda +module _ + {l1 l2 : Level} + (P : Pseudometric-Space l1 l2) + where + + initial-Metric-Extension : Metric-Extension (l1 ⊔ l2) (l1 ⊔ l2) P + initial-Metric-Extension = + ( metric-quotient-Pseudometric-Space P , + isometry-metric-quotient-Pseudometric-Space P) +``` + +## Properties + +### The induced isometry from the metric quotient is an isometry of metric extensions + +```agda +module _ + {l1 l2 l3 l4 : Level} + (P : Pseudometric-Space l1 l2) + (M : Metric-Extension l3 l4 P) + where + + isometry-metric-space-initial-Metric-Extension : + isometry-Metric-Space + ( metric-quotient-Pseudometric-Space P) + ( metric-space-Metric-Extension P M) + isometry-metric-space-initial-Metric-Extension = + isometry-map-isometry-metric-quotient-Pseudometric-Space + ( P) + ( metric-space-Metric-Extension P M) + ( isometry-metric-space-Metric-Extension P M) + + coh-initial-Metric-Extension : + coherence-triangle-isometry-metric-space-Metric-Extension + ( P) + ( initial-Metric-Extension P) + ( M) + ( isometry-metric-space-initial-Metric-Extension) + coh-initial-Metric-Extension x = + compute-map-isometry-metric-quotient-Pseudometric-Space + ( P) + ( metric-space-Metric-Extension P M) + ( isometry-metric-space-Metric-Extension P M) + ( map-metric-quotient-Pseudometric-Space P x) + ( x) + ( is-in-class-map-quotient-Pseudometric-Space P x) + + isometry-initial-Metric-Extension : + isometry-Metric-Extension + ( P) + ( initial-Metric-Extension P) + ( M) + isometry-initial-Metric-Extension = + ( isometry-metric-space-initial-Metric-Extension , + coh-initial-Metric-Extension) +``` + +### The metric quotient is the initial metric extension + +```agda +module _ + { l1 l2 l3 l4 : Level} + ( P : Pseudometric-Space l1 l2) + ( M : Metric-Extension l3 l4 P) + ( f : + isometry-Metric-Extension + ( P) + ( initial-Metric-Extension P) + ( M)) + where abstract + + all-htpy-isometry-initial-Metric-Extension : + htpy-isometry-Metric-Extension + ( P) + ( initial-Metric-Extension P) + ( M) + ( isometry-initial-Metric-Extension P M) + ( f) + all-htpy-isometry-initial-Metric-Extension X = + let + map-ext = + map-isometry-metric-quotient-Pseudometric-Space + ( P) + ( metric-space-Metric-Extension P M) + ( isometry-metric-space-Metric-Extension P M) + + map-f = + map-metric-space-isometry-Metric-Extension + ( P) + ( initial-Metric-Extension P) + ( M) + ( f) + + open + do-syntax-trunc-Prop + ( eq-prop-Metric-Space + ( metric-space-Metric-Extension P M) + ( map-ext X) + ( map-f X)) + + in do + ( x , x∈X) ← + is-inhabited-class-metric-quotient-Pseudometric-Space P X + + let + lemma-lhs = + compute-map-isometry-metric-quotient-Pseudometric-Space + ( P) + ( metric-space-Metric-Extension P M) + ( isometry-metric-space-Metric-Extension P M) + ( X) + ( x) + ( x∈X) + + lemma-mhs = + coh-isometry-Metric-Extension + ( P) + ( initial-Metric-Extension P) + ( M) + ( f) + ( x) + + lemma-rhs = + ap + ( map-metric-space-isometry-Metric-Extension + ( P) + ( initial-Metric-Extension P) + ( M) + ( f)) + ( eq-map-is-in-class-metric-quotient-Pseudometric-Space + ( P) + ( X) + ( x∈X)) + + lemma-lhs ∙ (inv lemma-mhs) ∙ lemma-rhs + + contraction-isometry-initial-Metric-Extension : + isometry-initial-Metric-Extension P M ＝ f + contraction-isometry-initial-Metric-Extension = + eq-htpy-isometry-Metric-Extension + ( P) + ( initial-Metric-Extension P) + ( M) + ( isometry-initial-Metric-Extension P M) + ( f) + ( all-htpy-isometry-initial-Metric-Extension) + +module _ + { l1 l2 l3 l4 : Level} + ( P : Pseudometric-Space l1 l2) + ( M : Metric-Extension l3 l4 P) + where abstract + + is-contr-isometry-initial-Metric-Extension : + is-contr + ( isometry-Metric-Extension + ( P) + ( initial-Metric-Extension P) + ( M)) + is-contr-isometry-initial-Metric-Extension = + ( isometry-initial-Metric-Extension P M , + contraction-isometry-initial-Metric-Extension P M) +``` From 78d28663bf41b2573f1ed7c43120f125955fb415 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 23 Nov 2025 17:41:06 +0100 Subject: [PATCH 17/30] Update src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- ...tric-extensions-of-pseudometric-spaces.lagda.md | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md index f4f5c3d59d8..3876afec82c 100644 --- a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -219,16 +219,10 @@ module _ ( metric-space-Metric-Extension P W) ( isometry-metric-space-isometry-Metric-Extension P V W g) ( isometry-metric-space-isometry-Metric-Extension P U V f)) - coh-comp-isometry-Metric-Extension x = - ( ap - ( map-metric-space-isometry-Metric-Extension P V W g) - ( coh-isometry-Metric-Extension - ( P) - ( U) - ( V) - ( f) - ( x))) ∙ - ( coh-isometry-Metric-Extension P V W g x) + coh-comp-isometry-Metric-Extension = + ( ( map-metric-space-isometry-Metric-Extension P V W g) ·l + ( coh-isometry-Metric-Extension P U V f)) ∙h + ( coh-isometry-Metric-Extension P V W g) comp-isometry-Metric-Extension : isometry-Metric-Extension P U W pr1 comp-isometry-Metric-Extension = From 3b1d036c489f31614038656bafc997613ca18f94 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 23 Nov 2025 18:04:11 +0100 Subject: [PATCH 18/30] import whiskering --- ...ies-between-metric-extensions-of-pseudometric-spaces.lagda.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md index 3876afec82c..7d17f8789f4 100644 --- a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -30,6 +30,7 @@ open import foundation.sets open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition open import metric-spaces.cauchy-approximations-metric-quotients-of-pseudometric-spaces open import metric-spaces.cauchy-approximations-metric-spaces From dc35782b696b7ae083acc6c000b695cfb8b3512a Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 23 Nov 2025 18:25:15 +0100 Subject: [PATCH 19/30] fix name id-isometry-XX --- ...extensions-of-pseudometric-spaces.lagda.md | 3 +-- .../isometries-metric-spaces.lagda.md | 12 +++++------ .../isometries-pseudometric-spaces.lagda.md | 20 +++++++++---------- ...y-of-metric-spaces-and-isometries.lagda.md | 2 +- 4 files changed, 18 insertions(+), 19 deletions(-) diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md index 7d17f8789f4..27aae4dbe52 100644 --- a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -193,8 +193,7 @@ module _ id-isometry-Metric-Extension : isometry-Metric-Extension P M M pr1 id-isometry-Metric-Extension = - isometry-id-Metric-Space - ( metric-space-Metric-Extension P M) + id-isometry-Metric-Space (metric-space-Metric-Extension P M) pr2 id-isometry-Metric-Extension = refl-htpy ``` diff --git a/src/metric-spaces/isometries-metric-spaces.lagda.md b/src/metric-spaces/isometries-metric-spaces.lagda.md index 3fee4dcad8f..463b3396a2b 100644 --- a/src/metric-spaces/isometries-metric-spaces.lagda.md +++ b/src/metric-spaces/isometries-metric-spaces.lagda.md @@ -125,8 +125,8 @@ module _ is-isometry-Metric-Space A A (id-Metric-Space A) is-isometry-id-Metric-Space d x y = id-iff - isometry-id-Metric-Space : isometry-Metric-Space A A - isometry-id-Metric-Space = + id-isometry-Metric-Space : isometry-Metric-Space A A + id-isometry-Metric-Space = id-Metric-Space A , is-isometry-id-Metric-Space ``` @@ -238,7 +238,7 @@ module _ left-unit-law-comp-isometry-Metric-Space : ( comp-isometry-Metric-Space A B B - (isometry-id-Metric-Space B) + ( id-isometry-Metric-Space B) ( f)) ＝ ( f) left-unit-law-comp-isometry-Metric-Space = @@ -250,7 +250,7 @@ module _ right-unit-law-comp-isometry-Metric-Space : ( comp-isometry-Metric-Space A A B ( f) - ( isometry-id-Metric-Space A)) ＝ + ( id-isometry-Metric-Space A)) ＝ ( f) right-unit-law-comp-isometry-Metric-Space = right-unit-law-comp-isometry-Pseudometric-Space @@ -335,7 +335,7 @@ module _ B f isometry-inv-is-equiv-isometry-Metric-Space) ＝ - ( isometry-id-Metric-Space B) + ( id-isometry-Metric-Space B) is-section-isometry-inv-is-equiv-isometry-Metric-Space = is-section-isometry-inv-is-equiv-isometry-Pseudometric-Space ( pseudometric-Metric-Space A) @@ -350,7 +350,7 @@ module _ A isometry-inv-is-equiv-isometry-Metric-Space f) ＝ - ( isometry-id-Metric-Space A) + ( id-isometry-Metric-Space A) is-retraction-isometry-inv-is-equiv-isometry-Metric-Space = is-retraction-isometry-inv-is-equiv-isometry-Pseudometric-Space ( pseudometric-Metric-Space A) diff --git a/src/metric-spaces/isometries-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-pseudometric-spaces.lagda.md index 35d81a521c0..665040a49f9 100644 --- a/src/metric-spaces/isometries-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-pseudometric-spaces.lagda.md @@ -113,8 +113,8 @@ module _ is-isometry-Pseudometric-Space A A (id-Pseudometric-Space A) is-isometry-id-Pseudometric-Space d x y = id-iff - isometry-id-Pseudometric-Space : isometry-Pseudometric-Space A A - isometry-id-Pseudometric-Space = + id-isometry-Pseudometric-Space : isometry-Pseudometric-Space A A + id-isometry-Pseudometric-Space = ( id-Pseudometric-Space A , is-isometry-id-Pseudometric-Space) ``` @@ -232,7 +232,7 @@ module _ left-unit-law-comp-isometry-Pseudometric-Space : ( comp-isometry-Pseudometric-Space A B B - (isometry-id-Pseudometric-Space B) + ( id-isometry-Pseudometric-Space B) ( f)) ＝ ( f) left-unit-law-comp-isometry-Pseudometric-Space = @@ -243,7 +243,7 @@ module _ ( A) ( B) ( B) - (isometry-id-Pseudometric-Space B) + ( id-isometry-Pseudometric-Space B) ( f)) ( f) ( refl-htpy) @@ -251,7 +251,7 @@ module _ right-unit-law-comp-isometry-Pseudometric-Space : ( comp-isometry-Pseudometric-Space A A B ( f) - ( isometry-id-Pseudometric-Space A)) ＝ + ( id-isometry-Pseudometric-Space A)) ＝ ( f) right-unit-law-comp-isometry-Pseudometric-Space = eq-htpy-map-isometry-Pseudometric-Space @@ -263,7 +263,7 @@ module _ ( A) ( B) ( f) - ( isometry-id-Pseudometric-Space A)) + ( id-isometry-Pseudometric-Space A)) ( refl-htpy) ``` @@ -357,25 +357,25 @@ module _ ( comp-isometry-Pseudometric-Space B A B ( f) ( isometry-inv-is-equiv-isometry-Pseudometric-Space)) ＝ - ( isometry-id-Pseudometric-Space B) + ( id-isometry-Pseudometric-Space B) is-section-isometry-inv-is-equiv-isometry-Pseudometric-Space = eq-htpy-map-isometry-Pseudometric-Space B B ( comp-isometry-Pseudometric-Space B A B ( f) ( isometry-inv-is-equiv-isometry-Pseudometric-Space)) - ( isometry-id-Pseudometric-Space B) + ( id-isometry-Pseudometric-Space B) ( is-section-map-inv-is-equiv E) is-retraction-isometry-inv-is-equiv-isometry-Pseudometric-Space : ( comp-isometry-Pseudometric-Space A B A ( isometry-inv-is-equiv-isometry-Pseudometric-Space) ( f)) ＝ - ( isometry-id-Pseudometric-Space A) + ( id-isometry-Pseudometric-Space A) is-retraction-isometry-inv-is-equiv-isometry-Pseudometric-Space = eq-htpy-map-isometry-Pseudometric-Space A A ( comp-isometry-Pseudometric-Space A B A ( isometry-inv-is-equiv-isometry-Pseudometric-Space) ( f)) - ( isometry-id-Pseudometric-Space A) + ( id-isometry-Pseudometric-Space A) ( is-retraction-map-inv-is-equiv E) ``` diff --git a/src/metric-spaces/precategory-of-metric-spaces-and-isometries.lagda.md b/src/metric-spaces/precategory-of-metric-spaces-and-isometries.lagda.md index ba315c5ba83..04989c2beae 100644 --- a/src/metric-spaces/precategory-of-metric-spaces-and-isometries.lagda.md +++ b/src/metric-spaces/precategory-of-metric-spaces-and-isometries.lagda.md @@ -55,7 +55,7 @@ module _ ( Metric-Space l1 l2) ( set-isometry-Metric-Space) ( λ {A B C} → comp-isometry-Metric-Space A B C) - ( isometry-id-Metric-Space) + ( id-isometry-Metric-Space) ( λ {A B C D} → associative-comp-isometry-Metric-Space A B C D) ( λ {A B} → left-unit-law-comp-isometry-Metric-Space A B) ( λ {A B} → right-unit-law-comp-isometry-Metric-Space A B) From d0bc999d0440d0407a007ffd500f47ebf17deec9 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 23 Nov 2025 18:31:38 +0100 Subject: [PATCH 20/30] fix name id-short-function-XX --- .../cauchy-approximations-metric-spaces.lagda.md | 2 +- ...-of-metric-spaces-and-short-functions.lagda.md | 6 +++--- .../short-functions-metric-spaces.lagda.md | 10 +++++----- .../short-functions-pseudometric-spaces.lagda.md | 15 ++++++++------- 4 files changed, 17 insertions(+), 16 deletions(-) diff --git a/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md index a6651165e3e..e48cfc33262 100644 --- a/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md @@ -133,7 +133,7 @@ module _ map-short-function-cauchy-approximation-Metric-Space ( A) ( A) - ( short-id-Metric-Space A) ＝ + ( id-short-function-Metric-Space A) ＝ id eq-id-map-short-function-cauchy-approximation-Metric-Space = refl diff --git a/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md b/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md index 6d3251395db..c494f32b3d5 100644 --- a/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md +++ b/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md @@ -56,7 +56,7 @@ module _ ( Metric-Space l1 l2) ( set-short-function-Metric-Space) ( λ {A B C} → comp-short-function-Metric-Space A B C) - ( short-id-Metric-Space) + ( id-short-function-Metric-Space) ( λ {A B C D} → associative-comp-short-function-Metric-Space A B C D) ( λ {A B} → left-unit-law-comp-short-function-Metric-Space A B) ( λ {A B} → right-unit-law-comp-short-function-Metric-Space A B) @@ -149,7 +149,7 @@ module _ ( B) ( f) ( short-inverse)) - ( short-id-Metric-Space B) + ( id-short-function-Metric-Space B) ( is-section-map-inv-is-equiv E)) , ( eq-htpy-map-short-function-Metric-Space ( A) @@ -160,7 +160,7 @@ module _ ( A) ( short-inverse) ( f)) - ( short-id-Metric-Space A) + ( id-short-function-Metric-Space A) ( is-retraction-map-inv-is-equiv E))) where diff --git a/src/metric-spaces/short-functions-metric-spaces.lagda.md b/src/metric-spaces/short-functions-metric-spaces.lagda.md index 64e55931bc5..e0cb7d72f27 100644 --- a/src/metric-spaces/short-functions-metric-spaces.lagda.md +++ b/src/metric-spaces/short-functions-metric-spaces.lagda.md @@ -140,9 +140,9 @@ module _ is-short-id-Pseudometric-Space ( pseudometric-Metric-Space A) - short-id-Metric-Space : short-function-Metric-Space A A - short-id-Metric-Space = - short-id-Pseudometric-Space (pseudometric-Metric-Space A) + id-short-function-Metric-Space : short-function-Metric-Space A A + id-short-function-Metric-Space = + id-short-function-Pseudometric-Space (pseudometric-Metric-Space A) ``` ### Equality of short functions between metric spaces is characterized by homotopy of their carrier maps @@ -216,7 +216,7 @@ module _ left-unit-law-comp-short-function-Metric-Space : ( comp-short-function-Metric-Space A B B - ( short-id-Metric-Space B) + ( id-short-function-Metric-Space B) ( f)) ＝ ( f) left-unit-law-comp-short-function-Metric-Space = @@ -228,7 +228,7 @@ module _ right-unit-law-comp-short-function-Metric-Space : ( comp-short-function-Metric-Space A A B ( f) - ( short-id-Metric-Space A)) ＝ + ( id-short-function-Metric-Space A)) ＝ ( f) right-unit-law-comp-short-function-Metric-Space = right-unit-law-comp-short-function-Pseudometric-Space diff --git a/src/metric-spaces/short-functions-pseudometric-spaces.lagda.md b/src/metric-spaces/short-functions-pseudometric-spaces.lagda.md index 2075b6e1006..ca153a94086 100644 --- a/src/metric-spaces/short-functions-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/short-functions-pseudometric-spaces.lagda.md @@ -116,9 +116,10 @@ module _ is-short-function-Pseudometric-Space A A (id-Pseudometric-Space A) is-short-id-Pseudometric-Space d x y H = H - short-id-Pseudometric-Space : short-function-Pseudometric-Space A A - short-id-Pseudometric-Space = - id-Pseudometric-Space A , is-short-id-Pseudometric-Space + id-short-function-Pseudometric-Space : + short-function-Pseudometric-Space A A + id-short-function-Pseudometric-Space = + ( id-Pseudometric-Space A , is-short-id-Pseudometric-Space) ``` ### Equality of short functions between pseudometric spaces is characterized by homotopy of their carrier maps @@ -192,7 +193,7 @@ module _ left-unit-law-comp-short-function-Pseudometric-Space : ( comp-short-function-Pseudometric-Space A B B - ( short-id-Pseudometric-Space B) + ( id-short-function-Pseudometric-Space B) ( f)) ＝ ( f) left-unit-law-comp-short-function-Pseudometric-Space = @@ -203,7 +204,7 @@ module _ ( A) ( B) ( B) - ( short-id-Pseudometric-Space B) + ( id-short-function-Pseudometric-Space B) ( f)) ( f) ( λ x → refl) @@ -211,7 +212,7 @@ module _ right-unit-law-comp-short-function-Pseudometric-Space : ( comp-short-function-Pseudometric-Space A A B ( f) - ( short-id-Pseudometric-Space A)) ＝ + ( id-short-function-Pseudometric-Space A)) ＝ ( f) right-unit-law-comp-short-function-Pseudometric-Space = eq-htpy-map-short-function-Pseudometric-Space @@ -223,7 +224,7 @@ module _ ( A) ( B) ( f) - ( short-id-Pseudometric-Space A)) + ( id-short-function-Pseudometric-Space A)) ( λ x → refl) ``` From 2c385c34ade7709d0e349add56e3d7f3caee9001 Mon Sep 17 00:00:00 2001 From: malarbol Date: Mon, 24 Nov 2025 18:59:44 +0100 Subject: [PATCH 21/30] action of isometries on Cauchy approximations preserves homotopies --- ...approximations-pseudometric-spaces.lagda.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md index b6b0b62a391..95e4601e8b9 100644 --- a/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md @@ -166,6 +166,24 @@ module _ ( eq-htpy f~g) ``` +### The action of isometries on preserves homotopies + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2') + (f g : isometry-Pseudometric-Space A B) + where + + htpy-map-cauchy-approximation-isometry-Pseudometric-Space : + htpy-isometry-Pseudometric-Space A B f g → + map-cauchy-approximation-isometry-Pseudometric-Space A B f ~ + map-cauchy-approximation-isometry-Pseudometric-Space A B g + htpy-map-cauchy-approximation-isometry-Pseudometric-Space f~g u = + eq-htpy-cauchy-approximation-Pseudometric-Space B + ( f~g ∘ map-cauchy-approximation-Pseudometric-Space A u) +``` + ## References Our definition of Cauchy approximation follows Definition 4.5.5 of From 80f94177c4c547c08a07d0a82366d6c24d37dca3 Mon Sep 17 00:00:00 2001 From: malarbol Date: Mon, 24 Nov 2025 19:05:18 +0100 Subject: [PATCH 22/30] refactor htpy-isometry-Pseudometric-Space --- .../isometries-pseudometric-spaces.lagda.md | 51 +++++-------------- 1 file changed, 14 insertions(+), 37 deletions(-) diff --git a/src/metric-spaces/isometries-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-pseudometric-spaces.lagda.md index 665040a49f9..9492be54c5b 100644 --- a/src/metric-spaces/isometries-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-pseudometric-spaces.lagda.md @@ -127,10 +127,19 @@ module _ (f g : isometry-Pseudometric-Space A B) where + htpy-isometry-Pseudometric-Space : UU (l1 ⊔ l1') + htpy-isometry-Pseudometric-Space = + map-isometry-Pseudometric-Space A B f ~ + map-isometry-Pseudometric-Space A B g + +module _ + {l1 l2 l1' l2' : Level} + (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2') + {f g : isometry-Pseudometric-Space A B} + where + equiv-eq-htpy-map-isometry-Pseudometric-Space : - ( f ＝ g) ≃ - ( map-isometry-Pseudometric-Space A B f ~ - map-isometry-Pseudometric-Space A B g) + (f ＝ g) ≃ htpy-isometry-Pseudometric-Space A B f g equiv-eq-htpy-map-isometry-Pseudometric-Space = equiv-funext ∘e extensionality-type-subtype' @@ -139,16 +148,12 @@ module _ ( g) htpy-eq-map-isometry-Pseudometric-Space : - ( f ＝ g) → - ( map-isometry-Pseudometric-Space A B f ~ - map-isometry-Pseudometric-Space A B g) + (f ＝ g) → htpy-isometry-Pseudometric-Space A B f g htpy-eq-map-isometry-Pseudometric-Space = map-equiv equiv-eq-htpy-map-isometry-Pseudometric-Space eq-htpy-map-isometry-Pseudometric-Space : - ( map-isometry-Pseudometric-Space A B f ~ - map-isometry-Pseudometric-Space A B g) → - ( f ＝ g) + htpy-isometry-Pseudometric-Space A B f g → (f ＝ g) eq-htpy-map-isometry-Pseudometric-Space = map-inv-equiv equiv-eq-htpy-map-isometry-Pseudometric-Space ``` @@ -239,13 +244,6 @@ module _ eq-htpy-map-isometry-Pseudometric-Space ( A) ( B) - ( comp-isometry-Pseudometric-Space - ( A) - ( B) - ( B) - ( id-isometry-Pseudometric-Space B) - ( f)) - ( f) ( refl-htpy) right-unit-law-comp-isometry-Pseudometric-Space : @@ -257,13 +255,6 @@ module _ eq-htpy-map-isometry-Pseudometric-Space ( A) ( B) - ( f) - ( comp-isometry-Pseudometric-Space - ( A) - ( A) - ( B) - ( f) - ( id-isometry-Pseudometric-Space A)) ( refl-htpy) ``` @@ -292,12 +283,6 @@ module _ eq-htpy-map-isometry-Pseudometric-Space ( A) ( D) - ( comp-isometry-Pseudometric-Space A B D - ( comp-isometry-Pseudometric-Space B C D h g) - ( f)) - ( comp-isometry-Pseudometric-Space A C D - ( h) - ( comp-isometry-Pseudometric-Space A B C g f)) ( refl-htpy) ``` @@ -360,10 +345,6 @@ module _ ( id-isometry-Pseudometric-Space B) is-section-isometry-inv-is-equiv-isometry-Pseudometric-Space = eq-htpy-map-isometry-Pseudometric-Space B B - ( comp-isometry-Pseudometric-Space B A B - ( f) - ( isometry-inv-is-equiv-isometry-Pseudometric-Space)) - ( id-isometry-Pseudometric-Space B) ( is-section-map-inv-is-equiv E) is-retraction-isometry-inv-is-equiv-isometry-Pseudometric-Space : @@ -373,9 +354,5 @@ module _ ( id-isometry-Pseudometric-Space A) is-retraction-isometry-inv-is-equiv-isometry-Pseudometric-Space = eq-htpy-map-isometry-Pseudometric-Space A A - ( comp-isometry-Pseudometric-Space A B A - ( isometry-inv-is-equiv-isometry-Pseudometric-Space) - ( f)) - ( id-isometry-Pseudometric-Space A) ( is-retraction-map-inv-is-equiv E) ``` From b256c5aa5d624f6d143f94c3900cff2a5ed4a38b Mon Sep 17 00:00:00 2001 From: malarbol Date: Mon, 24 Nov 2025 19:08:24 +0100 Subject: [PATCH 23/30] typo --- .../cauchy-approximations-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md index 95e4601e8b9..aa81e260534 100644 --- a/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md @@ -166,7 +166,7 @@ module _ ( eq-htpy f~g) ``` -### The action of isometries on preserves homotopies +### The action of isometries preserves homotopies ```agda module _ From 8ac34b9690ce7218d6bc7e9f771f25205ef5e57f Mon Sep 17 00:00:00 2001 From: malarbol Date: Mon, 24 Nov 2025 19:16:15 +0100 Subject: [PATCH 24/30] fix isometries-Metric-Space --- .../isometries-metric-spaces.lagda.md | 34 ++++++++++++++----- 1 file changed, 26 insertions(+), 8 deletions(-) diff --git a/src/metric-spaces/isometries-metric-spaces.lagda.md b/src/metric-spaces/isometries-metric-spaces.lagda.md index 463b3396a2b..c384a34dfb2 100644 --- a/src/metric-spaces/isometries-metric-spaces.lagda.md +++ b/src/metric-spaces/isometries-metric-spaces.lagda.md @@ -139,25 +139,43 @@ module _ (f g : isometry-Metric-Space A B) where + htpy-isometry-Metric-Space : UU (l1 ⊔ l1') + htpy-isometry-Metric-Space = + map-isometry-Metric-Space A B f ~ map-isometry-Metric-Space A B g + + is-prop-htpy-isometry-Metric-Space : + is-prop htpy-isometry-Metric-Space + is-prop-htpy-isometry-Metric-Space = + is-prop-Π + ( λ x → + is-set-type-Metric-Space B + ( map-isometry-Metric-Space A B f x) + ( map-isometry-Metric-Space A B g x)) + + htpy-prop-isometry-Metric-Space : Prop (l1 ⊔ l1') + htpy-prop-isometry-Metric-Space = + ( htpy-isometry-Metric-Space , is-prop-htpy-isometry-Metric-Space) + +module _ + {l1 l2 l1' l2' : Level} + (A : Metric-Space l1 l2) (B : Metric-Space l1' l2') + {f g : isometry-Metric-Space A B} + where + equiv-eq-htpy-map-isometry-Metric-Space : - (f ＝ g) ≃ - (map-isometry-Metric-Space A B f ~ map-isometry-Metric-Space A B g) + (f ＝ g) ≃ htpy-isometry-Metric-Space A B f g equiv-eq-htpy-map-isometry-Metric-Space = equiv-eq-htpy-map-isometry-Pseudometric-Space ( pseudometric-Metric-Space A) ( pseudometric-Metric-Space B) - ( f) - ( g) htpy-eq-map-isometry-Metric-Space : - (f ＝ g) → - (map-isometry-Metric-Space A B f ~ map-isometry-Metric-Space A B g) + (f ＝ g) → htpy-isometry-Metric-Space A B f g htpy-eq-map-isometry-Metric-Space = map-equiv equiv-eq-htpy-map-isometry-Metric-Space eq-htpy-map-isometry-Metric-Space : - ( map-isometry-Metric-Space A B f ~ map-isometry-Metric-Space A B g) → - (f ＝ g) + htpy-isometry-Metric-Space A B f g → (f ＝ g) eq-htpy-map-isometry-Metric-Space = map-inv-equiv equiv-eq-htpy-map-isometry-Metric-Space ``` From cbc5f9d915ab20844e1f200c6c3b78cfb8e344cd Mon Sep 17 00:00:00 2001 From: malarbol Date: Mon, 24 Nov 2025 19:36:04 +0100 Subject: [PATCH 25/30] fix --- ...es-between-metric-extensions-of-pseudometric-spaces.lagda.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md index 27aae4dbe52..c28e456f756 100644 --- a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -273,7 +273,5 @@ module _ ( eq-htpy-map-isometry-Metric-Space ( metric-space-Metric-Extension P M) ( metric-space-Metric-Extension P N) - ( isometry-metric-space-isometry-Metric-Extension P M N f) - ( isometry-metric-space-isometry-Metric-Extension P M N g) ( f~g)) ``` From 6b2954485b88b1dc528e47bde79d7b7a64a78b2e Mon Sep 17 00:00:00 2001 From: malarbol Date: Mon, 24 Nov 2025 19:56:44 +0100 Subject: [PATCH 26/30] The action of isometries preserves composition --- ...pproximations-pseudometric-spaces.lagda.md | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md index aa81e260534..82b421ac35c 100644 --- a/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md @@ -184,6 +184,32 @@ module _ ( f~g ∘ map-cauchy-approximation-Pseudometric-Space A u) ``` +### The action of isometries preserves composition + +```agda +module _ + {la la' lb lb' lc lc' : Level} + (A : Pseudometric-Space la la') + (B : Pseudometric-Space lb lb') + (C : Pseudometric-Space lc lc') + (g : isometry-Pseudometric-Space B C) + (f : isometry-Pseudometric-Space A B) + where + + htpy-map-cauchy-approximation-comp-isometry-Pseudometric-Space : + ( map-cauchy-approximation-isometry-Pseudometric-Space B C g ∘ + map-cauchy-approximation-isometry-Pseudometric-Space A B f) ~ + ( map-cauchy-approximation-isometry-Pseudometric-Space A C + ( comp-isometry-Pseudometric-Space + ( A) + ( B) + ( C) + ( g) + ( f))) + htpy-map-cauchy-approximation-comp-isometry-Pseudometric-Space u = + eq-htpy-cauchy-approximation-Pseudometric-Space C refl-htpy +``` + ## References Our definition of Cauchy approximation follows Definition 4.5.5 of From f297243c62f383bb4f2f6a945d35fa6467233884 Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 25 Nov 2025 03:01:42 +0100 Subject: [PATCH 27/30] lemma --- ...extensions-of-pseudometric-spaces.lagda.md | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md index 73ff78856c9..52364057c97 100644 --- a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md @@ -155,6 +155,26 @@ module _ ( isometry-cauchy-pseudocompletion-Metric-Extension) ``` +### The action of metric extensions on Cauchy approximations is natural w.r.t. Cauchy pseudocompletions + +```agda +module _ + {l1 l2 l3 l4 : Level} (P : Pseudometric-Space l1 l2) + (M : Metric-Extension l3 l4 P) + where + + htpy-map-cauchy-pseudocompletion-Metric-Extension : + ( map-cauchy-pseudocompletion-Metric-Extension P M ∘ + map-cauchy-pseudocompletion-Pseudometric-Space P) ~ + ( ( map-cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Extension P M)) ∘ + ( map-isometry-metric-space-Metric-Extension P M)) + htpy-map-cauchy-pseudocompletion-Metric-Extension x = + eq-htpy-cauchy-approximation-Metric-Space + ( metric-space-Metric-Extension P M) + ( refl-htpy) +``` + ### Limit points in metric extensions ```agda From ba5385e7c9282be9b0447ce8677b42fa0053377a Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 25 Nov 2025 18:20:14 +0100 Subject: [PATCH 28/30] forgetful metric extensions of metric spaces --- ...extensions-of-pseudometric-spaces.lagda.md | 20 +++++++++++++++++++ ...extensions-of-pseudometric-spaces.lagda.md | 14 +++++++++++++ 2 files changed, 34 insertions(+) diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md index 27aae4dbe52..411d45fc060 100644 --- a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md @@ -1,6 +1,8 @@ # Isometries between metric extensions of a pseudometric space ```agda +{-# OPTIONS --lossy-unification #-} + module metric-spaces.isometries-between-metric-extensions-of-pseudometric-spaces where ``` @@ -182,6 +184,24 @@ module _ ## Properties +### Isometries of metric spaces are isometries of metric extensions + +```agda +module _ + {l1 l2 l3 l4 : Level} + (M : Metric-Space l1 l2) + (N : Metric-Space l3 l4) + (f : isometry-Metric-Space M N) + where + + forgetful-isometry-Metric-Extension : + isometry-Metric-Extension + ( pseudometric-Metric-Space M) + ( forgetful-Metric-Extension M) + ( N , f) + forgetful-isometry-Metric-Extension = (f , refl-htpy) +``` + ### The identity isometry of a metric extension ```agda diff --git a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md index 73ff78856c9..f8cd5045c8a 100644 --- a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md @@ -1,6 +1,8 @@ # Metric extensions of pseudometric spaces ```agda +{-# OPTIONS --lossy-unification #-} + module metric-spaces.metric-extensions-of-pseudometric-spaces where ``` @@ -111,6 +113,18 @@ module _ ## Properties +### The forgetful metric extension of a metric space into itself + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + where + + forgetful-Metric-Extension : + Metric-Extension l1 l2 (pseudometric-Metric-Space M) + forgetful-Metric-Extension = (M , id-isometry-Metric-Space M) +``` + ### Action of metric extensions on Cauchy approximations ```agda From fd43093c9145c2eb3a80eb10b856b07f97d5a5d8 Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 25 Nov 2025 18:39:12 +0100 Subject: [PATCH 29/30] plural (preserves|reflects)-neighborhoods-XXX --- ...e-decompositions-of-metric-spaces.lagda.md | 12 ++++---- ...-quotients-of-pseudometric-spaces.lagda.md | 2 +- ...pseudocompletion-of-metric-spaces.lagda.md | 6 ++-- ...completion-of-pseudometric-spaces.lagda.md | 22 +++++++------- .../indexed-sums-metric-spaces.lagda.md | 7 +++-- .../isometries-metric-spaces.lagda.md | 8 ++--- .../isometries-pseudometric-spaces.lagda.md | 8 ++--- ...-quotients-of-pseudometric-spaces.lagda.md | 30 +++++++++---------- ...ort-functions-pseudometric-spaces.lagda.md | 2 +- ...y-of-elements-pseudometric-spaces.lagda.md | 30 +++++++++---------- 10 files changed, 64 insertions(+), 63 deletions(-) diff --git a/src/metric-spaces/bounded-distance-decompositions-of-metric-spaces.lagda.md b/src/metric-spaces/bounded-distance-decompositions-of-metric-spaces.lagda.md index ea2bf3aa077..57bdd01bc5a 100644 --- a/src/metric-spaces/bounded-distance-decompositions-of-metric-spaces.lagda.md +++ b/src/metric-spaces/bounded-distance-decompositions-of-metric-spaces.lagda.md @@ -213,7 +213,7 @@ module _ {l1 l2 : Level} (A : Metric-Space l1 l2) where - preserves-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space : + preserves-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space : ( d : ℚ⁺) ( x y : type-bounded-distance-decomposition-Metric-Space A) → neighborhood-Metric-Space @@ -224,7 +224,7 @@ module _ neighborhood-Metric-Space A d ( map-equiv-bounded-distance-decomposition-Metric-Space A x) ( map-equiv-bounded-distance-decomposition-Metric-Space A y) - preserves-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space + preserves-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space d (X , x , x∈X) (Y , y , y∈Y) (X=Y , Nxy) = forward-implication ( lemma-iff-neighborhood-bounded-distance-decomposition-Metric-Space @@ -237,7 +237,7 @@ module _ ( y , y∈Y)) ( Nxy) - reflects-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space : + reflects-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space : ( d : ℚ⁺) ( x y : type-bounded-distance-decomposition-Metric-Space A) → neighborhood-Metric-Space A d @@ -248,7 +248,7 @@ module _ ( d) ( x) ( y) - reflects-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space + reflects-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space d (X , x , x∈X) (Y , y , y∈Y) Nxy = ( lemma-eq , backward-implication @@ -280,11 +280,11 @@ module _ ( map-equiv-bounded-distance-decomposition-Metric-Space A) is-isometry-map-equiv-bounded-distance-decomposition-Metric-Space d x y = - ( ( preserves-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space + ( ( preserves-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space ( d) ( x) ( y)) , - ( reflects-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space + ( reflects-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space ( d) ( x) ( y))) diff --git a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md index 4c46e7a886c..b5ce744455e 100644 --- a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md @@ -233,7 +233,7 @@ module _ ( x) ( x∈uε) in - preserves-neighborhood-sim-Pseudometric-Space + preserves-neighborhoods-sim-Pseudometric-Space ( M) ( uε~x) ( lim~y) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md index 7be8a045c4c..802663a17b7 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md @@ -349,7 +349,7 @@ module _ ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space)) is-short-const-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space d x y = - preserves-neighborhood-sim-Pseudometric-Space + preserves-neighborhoods-sim-Pseudometric-Space ( cauchy-pseudocompletion-Metric-Space M) { x} { const-cauchy-approximation-Metric-Space @@ -463,7 +463,7 @@ module _ ( v) reflects-neighborhoods-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space δ x y Nδ = - reflects-neighborhood-sim-Pseudometric-Space + reflects-neighborhoods-sim-Pseudometric-Space ( cauchy-pseudocompletion-Metric-Space M) { x} { const-cauchy-approximation-Metric-Space @@ -488,7 +488,7 @@ module _ ( is-complete-M) ( y)) ( δ) - ( preserves-neighborhood-map-isometry-Pseudometric-Space + ( preserves-neighborhoods-map-isometry-Pseudometric-Space ( pseudometric-Metric-Space M) ( cauchy-pseudocompletion-Metric-Space M) ( isometry-cauchy-pseudocompletion-Metric-Space M) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index cf682cb3e8c..41506234ff6 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -295,7 +295,7 @@ module _ const-cauchy-approximation-Pseudometric-Space M abstract - preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space : + preserves-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space : (d : ℚ⁺) (x y : type-Pseudometric-Space M) → neighborhood-Pseudometric-Space M d x y → neighborhood-cauchy-pseudocompletion-Pseudometric-Space @@ -303,13 +303,13 @@ module _ ( d) ( map-cauchy-pseudocompletion-Pseudometric-Space x) ( map-cauchy-pseudocompletion-Pseudometric-Space y) - preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space + preserves-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space d x y Nxy δ ε = monotonic-neighborhood-Pseudometric-Space M x y d (δ +ℚ⁺ ε +ℚ⁺ d) ( le-right-add-ℚ⁺ (δ +ℚ⁺ ε) d) ( Nxy) - reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space : + reflects-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space : (d : ℚ⁺) (x y : type-Pseudometric-Space M) → neighborhood-cauchy-pseudocompletion-Pseudometric-Space ( M) @@ -317,7 +317,7 @@ module _ ( map-cauchy-pseudocompletion-Pseudometric-Space x) ( map-cauchy-pseudocompletion-Pseudometric-Space y) → neighborhood-Pseudometric-Space M d x y - reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space + reflects-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space d x y Nxy = saturated-neighborhood-Pseudometric-Space M d x y ( λ δ → @@ -335,11 +335,11 @@ module _ ( cauchy-pseudocompletion-Pseudometric-Space M) ( map-cauchy-pseudocompletion-Pseudometric-Space) is-isometry-map-cauchy-pseudocompletion-Pseudometric-Space d x y = - ( ( preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space + ( ( preserves-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space ( d) ( x) ( y)) , - (reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space + (reflects-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space ( d) ( x) ( y))) @@ -666,7 +666,7 @@ module _ ( M))) is-short-function-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space d u v = - preserves-neighborhood-sim-Pseudometric-Space + preserves-neighborhoods-sim-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M)) { u} @@ -697,7 +697,7 @@ module _ ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M) is-short-function-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space d u v Nuv = - reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space + reflects-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M) ( d) ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space @@ -752,7 +752,7 @@ module _ ( v) reflects-neighborhoods-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space d u v N-lim = - reflects-neighborhood-sim-Pseudometric-Space + reflects-neighborhoods-sim-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M)) { u} @@ -774,7 +774,7 @@ module _ ( M) ( v)) ( d) - ( preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space + ( preserves-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M) ( d) ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space @@ -887,7 +887,7 @@ module _ ( y) reflects-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space d x y Nxy α β = - reflects-neighborhood-map-isometry-Pseudometric-Space + reflects-neighborhoods-map-isometry-Pseudometric-Space ( A) ( B) ( f) diff --git a/src/metric-spaces/indexed-sums-metric-spaces.lagda.md b/src/metric-spaces/indexed-sums-metric-spaces.lagda.md index 4ed15b71da2..c07e513fe37 100644 --- a/src/metric-spaces/indexed-sums-metric-spaces.lagda.md +++ b/src/metric-spaces/indexed-sums-metric-spaces.lagda.md @@ -295,7 +295,7 @@ module _ ( map-emb-fiber-indexed-sum-Metric-Space A P x , is-short-emb-fiber-indexed-sum-Metric-Space) - reflects-neighborhood-emb-fiber-indexed-sum-Metric-Space : + reflects-neighborhoods-emb-fiber-indexed-sum-Metric-Space : (d : ℚ⁺) (px px' : type-Metric-Space (P x)) → neighborhood-Metric-Space ( indexed-sum-Metric-Space A P) @@ -307,7 +307,8 @@ module _ ( d) ( px) ( px') - reflects-neighborhood-emb-fiber-indexed-sum-Metric-Space d px px' (e , Nxx') = + reflects-neighborhoods-emb-fiber-indexed-sum-Metric-Space + d px px' (e , Nxx') = inv-tr ( λ e' → neighborhood-Metric-Space @@ -328,7 +329,7 @@ module _ ( map-emb-fiber-indexed-sum-Metric-Space A P x) is-isometry-emb-fiber-indexed-sum-Metric-Space d px px' = ( is-short-emb-fiber-indexed-sum-Metric-Space d px px' , - reflects-neighborhood-emb-fiber-indexed-sum-Metric-Space d px px') + reflects-neighborhoods-emb-fiber-indexed-sum-Metric-Space d px px') isometry-emb-fiber-indexed-Metric-Space : isometry-Metric-Space (P x) (indexed-sum-Metric-Space A P) diff --git a/src/metric-spaces/isometries-metric-spaces.lagda.md b/src/metric-spaces/isometries-metric-spaces.lagda.md index 463b3396a2b..92c1c0a3e88 100644 --- a/src/metric-spaces/isometries-metric-spaces.lagda.md +++ b/src/metric-spaces/isometries-metric-spaces.lagda.md @@ -171,7 +171,7 @@ module _ (f : isometry-Metric-Space A B) where - preserves-neighborhood-map-isometry-Metric-Space : + preserves-neighborhoods-map-isometry-Metric-Space : (d : ℚ⁺) (x y : type-Metric-Space A) → neighborhood-Metric-Space A d x y → neighborhood-Metric-Space @@ -179,11 +179,11 @@ module _ ( d) ( map-isometry-Metric-Space A B f x) ( map-isometry-Metric-Space A B f y) - preserves-neighborhood-map-isometry-Metric-Space d x y = + preserves-neighborhoods-map-isometry-Metric-Space d x y = forward-implication ( is-isometry-map-isometry-Metric-Space A B f d x y) - reflects-neighborhood-map-isometry-Metric-Space : + reflects-neighborhoods-map-isometry-Metric-Space : (d : ℚ⁺) (x y : type-Metric-Space A) → neighborhood-Metric-Space ( B) @@ -191,7 +191,7 @@ module _ ( map-isometry-Metric-Space A B f x) ( map-isometry-Metric-Space A B f y) → neighborhood-Metric-Space A d x y - reflects-neighborhood-map-isometry-Metric-Space d x y = + reflects-neighborhoods-map-isometry-Metric-Space d x y = backward-implication ( is-isometry-map-isometry-Metric-Space A B f d x y) ``` diff --git a/src/metric-spaces/isometries-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-pseudometric-spaces.lagda.md index 665040a49f9..7147daf5c02 100644 --- a/src/metric-spaces/isometries-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/isometries-pseudometric-spaces.lagda.md @@ -162,7 +162,7 @@ module _ (f : isometry-Pseudometric-Space A B) where - preserves-neighborhood-map-isometry-Pseudometric-Space : + preserves-neighborhoods-map-isometry-Pseudometric-Space : (d : ℚ⁺) (x y : type-Pseudometric-Space A) → neighborhood-Pseudometric-Space A d x y → neighborhood-Pseudometric-Space @@ -170,11 +170,11 @@ module _ ( d) ( map-isometry-Pseudometric-Space A B f x) ( map-isometry-Pseudometric-Space A B f y) - preserves-neighborhood-map-isometry-Pseudometric-Space d x y = + preserves-neighborhoods-map-isometry-Pseudometric-Space d x y = forward-implication ( is-isometry-map-isometry-Pseudometric-Space A B f d x y) - reflects-neighborhood-map-isometry-Pseudometric-Space : + reflects-neighborhoods-map-isometry-Pseudometric-Space : (d : ℚ⁺) (x y : type-Pseudometric-Space A) → neighborhood-Pseudometric-Space ( B) @@ -182,7 +182,7 @@ module _ ( map-isometry-Pseudometric-Space A B f x) ( map-isometry-Pseudometric-Space A B f y) → neighborhood-Pseudometric-Space A d x y - reflects-neighborhood-map-isometry-Pseudometric-Space d x y = + reflects-neighborhoods-map-isometry-Pseudometric-Space d x y = backward-implication ( is-isometry-map-isometry-Pseudometric-Space A B f d x y) ``` diff --git a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md index fb63b3dccab..d4228503f38 100644 --- a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md @@ -408,7 +408,7 @@ module _ where abstract - preserves-neighborhood-map-metric-quotient-Pseudometric-Space : + preserves-neighborhoods-map-metric-quotient-Pseudometric-Space : (d : ℚ⁺) (x y : type-Pseudometric-Space M) → neighborhood-Pseudometric-Space M d x y → neighborhood-metric-quotient-Pseudometric-Space @@ -416,7 +416,7 @@ module _ ( d) ( map-metric-quotient-Pseudometric-Space M x) ( map-metric-quotient-Pseudometric-Space M y) - preserves-neighborhood-map-metric-quotient-Pseudometric-Space + preserves-neighborhoods-map-metric-quotient-Pseudometric-Space d x y d⟨x,y⟩ (x' , x≈x') (y' , y≈y') = let x~x' = @@ -434,15 +434,15 @@ module _ ( y≈y') in - preserves-neighborhood-right-sim-Pseudometric-Space M y~y' d x' - ( preserves-neighborhood-left-sim-Pseudometric-Space + preserves-neighborhoods-right-sim-Pseudometric-Space M y~y' d x' + ( preserves-neighborhoods-left-sim-Pseudometric-Space ( M) ( x~x') ( d) ( y) ( d⟨x,y⟩)) - reflects-neighborhood-map-metric-quotient-Pseudometric-Space : + reflects-neighborhoods-map-metric-quotient-Pseudometric-Space : (d : ℚ⁺) (x y : type-Pseudometric-Space M) → neighborhood-metric-quotient-Pseudometric-Space ( M) @@ -450,7 +450,7 @@ module _ ( map-metric-quotient-Pseudometric-Space M x) ( map-metric-quotient-Pseudometric-Space M y) → neighborhood-Pseudometric-Space M d x y - reflects-neighborhood-map-metric-quotient-Pseudometric-Space + reflects-neighborhoods-map-metric-quotient-Pseudometric-Space d x y Nxy = Nxy ( map-subtype-metric-quotient-Pseudometric-Space M x) @@ -462,8 +462,8 @@ module _ ( pseudometric-metric-quotient-Pseudometric-Space M) ( map-metric-quotient-Pseudometric-Space M) is-isometry-map-metric-quotient-Pseudometric-Space d x y = - ( preserves-neighborhood-map-metric-quotient-Pseudometric-Space d x y , - reflects-neighborhood-map-metric-quotient-Pseudometric-Space d x y) + ( preserves-neighborhoods-map-metric-quotient-Pseudometric-Space d x y , + reflects-neighborhoods-map-metric-quotient-Pseudometric-Space d x y) ``` ### The isometry from a pseudometric space to its quotient metric space @@ -769,7 +769,7 @@ module _ ( f)) abstract - preserves-neighborhood-map-isometry-metric-quotient-Pseudometric-Space : + preserves-neighborhoods-map-isometry-metric-quotient-Pseudometric-Space : (d : ℚ⁺) → (x y : type-metric-quotient-Pseudometric-Space A) → neighborhood-metric-quotient-Pseudometric-Space @@ -782,7 +782,7 @@ module _ ( d) ( map-isometry-metric-quotient-Pseudometric-Space x) ( map-isometry-metric-quotient-Pseudometric-Space y) - preserves-neighborhood-map-isometry-metric-quotient-Pseudometric-Space = + preserves-neighborhoods-map-isometry-metric-quotient-Pseudometric-Space = is-short-map-short-function-metric-quotient-Pseudometric-Space ( A) ( B) @@ -791,7 +791,7 @@ module _ ( pseudometric-Metric-Space B) ( f)) - reflects-neighborhood-map-isometry-metric-quotient-Pseudometric-Space : + reflects-neighborhoods-map-isometry-metric-quotient-Pseudometric-Space : (d : ℚ⁺) → (x y : type-metric-quotient-Pseudometric-Space A) → neighborhood-Metric-Space @@ -804,9 +804,9 @@ module _ ( d) ( x) ( y) - reflects-neighborhood-map-isometry-metric-quotient-Pseudometric-Space + reflects-neighborhoods-map-isometry-metric-quotient-Pseudometric-Space d X Y N⟨fX,fY⟩ (x , x∈X) (y , y∈Y) = - reflects-neighborhood-map-isometry-Pseudometric-Space + reflects-neighborhoods-map-isometry-Pseudometric-Space ( A) ( pseudometric-Metric-Space B) ( f) @@ -825,11 +825,11 @@ module _ ( B) ( map-isometry-metric-quotient-Pseudometric-Space) is-isometry-map-isometry-metric-quotient-Pseudometric-Space d x y = - ( preserves-neighborhood-map-isometry-metric-quotient-Pseudometric-Space + ( preserves-neighborhoods-map-isometry-metric-quotient-Pseudometric-Space ( d) ( x) ( y) , - reflects-neighborhood-map-isometry-metric-quotient-Pseudometric-Space + reflects-neighborhoods-map-isometry-metric-quotient-Pseudometric-Space ( d) ( x) ( y)) diff --git a/src/metric-spaces/short-functions-pseudometric-spaces.lagda.md b/src/metric-spaces/short-functions-pseudometric-spaces.lagda.md index ca153a94086..c4e262d3a3d 100644 --- a/src/metric-spaces/short-functions-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/short-functions-pseudometric-spaces.lagda.md @@ -296,7 +296,7 @@ module _ is-isometry-Pseudometric-Space A B f → is-short-function-Pseudometric-Space A B f is-short-is-isometry-Pseudometric-Space I = - preserves-neighborhood-map-isometry-Pseudometric-Space A B (f , I) + preserves-neighborhoods-map-isometry-Pseudometric-Space A B (f , I) ``` ### The embedding of isometries of pseudometric spaces into short maps diff --git a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md index 205dd76d739..6a249158e43 100644 --- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md @@ -173,13 +173,13 @@ module _ where abstract - preserves-neighborhood-left-sim-Pseudometric-Space : + preserves-neighborhoods-left-sim-Pseudometric-Space : { x y : type-Pseudometric-Space A} → ( sim-Pseudometric-Space A x y) → ( d : ℚ⁺) (z : type-Pseudometric-Space A) → neighborhood-Pseudometric-Space A d x z → neighborhood-Pseudometric-Space A d y z - preserves-neighborhood-left-sim-Pseudometric-Space {x} {y} x≍y d z Nxz = + preserves-neighborhoods-left-sim-Pseudometric-Space {x} {y} x≍y d z Nxz = saturated-neighborhood-Pseudometric-Space ( A) ( d) @@ -204,46 +204,46 @@ module _ ( y) ( x≍y δ)))) - preserves-neighborhood-right-sim-Pseudometric-Space : + preserves-neighborhoods-right-sim-Pseudometric-Space : { x y : type-Pseudometric-Space A} → ( sim-Pseudometric-Space A x y) → ( d : ℚ⁺) (z : type-Pseudometric-Space A) → neighborhood-Pseudometric-Space A d z x → neighborhood-Pseudometric-Space A d z y - preserves-neighborhood-right-sim-Pseudometric-Space {x} {y} x≍y d z Nzx = + preserves-neighborhoods-right-sim-Pseudometric-Space {x} {y} x≍y d z Nzx = symmetric-neighborhood-Pseudometric-Space A d y z - ( preserves-neighborhood-left-sim-Pseudometric-Space x≍y d z + ( preserves-neighborhoods-left-sim-Pseudometric-Space x≍y d z ( symmetric-neighborhood-Pseudometric-Space A d z x Nzx)) - preserves-neighborhood-sim-Pseudometric-Space : + preserves-neighborhoods-sim-Pseudometric-Space : {x x' y y' : type-Pseudometric-Space A} → sim-Pseudometric-Space A x x' → sim-Pseudometric-Space A y y' → (d : ℚ⁺) → neighborhood-Pseudometric-Space A d x y → neighborhood-Pseudometric-Space A d x' y' - preserves-neighborhood-sim-Pseudometric-Space + preserves-neighborhoods-sim-Pseudometric-Space {x} {x'} {y} {y'} x~x' y~y' d Nxy = - preserves-neighborhood-left-sim-Pseudometric-Space + preserves-neighborhoods-left-sim-Pseudometric-Space ( x~x') ( d) ( y') - ( preserves-neighborhood-right-sim-Pseudometric-Space + ( preserves-neighborhoods-right-sim-Pseudometric-Space ( y~y') ( d) ( x) ( Nxy)) - reflects-neighborhood-sim-Pseudometric-Space : + reflects-neighborhoods-sim-Pseudometric-Space : {x x' y y' : type-Pseudometric-Space A} → sim-Pseudometric-Space A x x' → sim-Pseudometric-Space A y y' → (d : ℚ⁺) → neighborhood-Pseudometric-Space A d x' y' → neighborhood-Pseudometric-Space A d x y - reflects-neighborhood-sim-Pseudometric-Space + reflects-neighborhoods-sim-Pseudometric-Space {x} {x'} {y} {y'} x~x' y~y' = - preserves-neighborhood-sim-Pseudometric-Space + preserves-neighborhoods-sim-Pseudometric-Space ( inv-sim-Pseudometric-Space A x~x') ( inv-sim-Pseudometric-Space A y~y') @@ -255,8 +255,8 @@ module _ neighborhood-Pseudometric-Space A d y z) same-neighbors-iff-sim-Pseudometric-Space = ( λ x≍y d z → - ( preserves-neighborhood-left-sim-Pseudometric-Space x≍y d z) , - ( preserves-neighborhood-left-sim-Pseudometric-Space + ( preserves-neighborhoods-left-sim-Pseudometric-Space x≍y d z) , + ( preserves-neighborhoods-left-sim-Pseudometric-Space ( inv-sim-Pseudometric-Space A x≍y) ( d) ( z))) , @@ -356,5 +356,5 @@ module _ ( map-isometry-Pseudometric-Space A B f y)) → ( sim-Pseudometric-Space A x y) reflects-sim-map-isometry-Pseudometric-Space x y fx~fy d = - reflects-neighborhood-map-isometry-Pseudometric-Space A B f d x y (fx~fy d) + reflects-neighborhoods-map-isometry-Pseudometric-Space A B f d x y (fx~fy d) ``` From 1e8202cd2fda258df106f56a519a85b46345e607 Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 25 Nov 2025 20:20:11 +0100 Subject: [PATCH 30/30] remove --lossy-unification --lossy-unification breaks some proof of #1726 --- .../metric-extensions-of-pseudometric-spaces.lagda.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md index f8cd5045c8a..4868e97993a 100644 --- a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md @@ -1,8 +1,6 @@ # Metric extensions of pseudometric spaces ```agda -{-# OPTIONS --lossy-unification #-} - module metric-spaces.metric-extensions-of-pseudometric-spaces where ```