Refactor metric spaces

src/literature/100-theorems.lagda.md

@@ -140,7 +140,7 @@ open import elementary-number-theory.fundamental-theorem-of-arithmetic using
 
 ```agda
 open import real-numbers.metric-space-of-real-numbers using
-  ( is-triangular-premetric-leq-ℝ)
+  ( is-triangular-neighborhood-ℝ)
 open import real-numbers.distance-real-numbers using
   ( triangle-inequality-dist-ℝ)
 ```

src/metric-spaces.lagda.md

@@ -48,71 +48,61 @@ module metric-spaces where
 open import metric-spaces.category-of-metric-spaces-and-isometries public
 open import metric-spaces.category-of-metric-spaces-and-short-functions public
 open import metric-spaces.cauchy-approximations-metric-spaces public
-open import metric-spaces.cauchy-approximations-premetric-spaces public
+open import metric-spaces.cauchy-approximations-pseudometric-spaces public
 open import metric-spaces.cauchy-sequences-complete-metric-spaces public
 open import metric-spaces.cauchy-sequences-metric-spaces public
-open import metric-spaces.closed-premetric-structures public
 open import metric-spaces.complete-metric-spaces public
 open import metric-spaces.continuous-functions-metric-spaces public
-open import metric-spaces.continuous-functions-premetric-spaces public
 open import metric-spaces.convergent-cauchy-approximations-metric-spaces public
 open import metric-spaces.convergent-sequences-metric-spaces public
 open import metric-spaces.dependent-products-metric-spaces public
-open import metric-spaces.discrete-premetric-structures public
+open import metric-spaces.discrete-metric-spaces public
+open import metric-spaces.disjoint-sums-metric-spaces public
 open import metric-spaces.elements-at-bounded-distance-metric-spaces public
 open import metric-spaces.equality-of-metric-spaces public
-open import metric-spaces.equality-of-premetric-spaces public
-open import metric-spaces.extensional-premetric-structures public
+open import metric-spaces.extensional-pseudometric-spaces public
 open import metric-spaces.functions-metric-spaces public
+open import metric-spaces.functions-pseudometric-spaces public
 open import metric-spaces.functor-category-set-functions-isometry-metric-spaces public
 open import metric-spaces.functor-category-short-isometry-metric-spaces public
-open import metric-spaces.induced-premetric-structures-on-preimages public
-open import metric-spaces.isometric-equivalences-premetric-spaces public
 open import metric-spaces.isometries-metric-spaces public
-open import metric-spaces.isometries-premetric-spaces public
-open import metric-spaces.limits-of-cauchy-approximations-premetric-spaces public
+open import metric-spaces.isometries-pseudometric-spaces public
+open import metric-spaces.limits-of-cauchy-approximations-metric-spaces public
+open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces public
+open import metric-spaces.limits-of-functions-metric-spaces public
 open import metric-spaces.limits-of-sequences-metric-spaces public
-open import metric-spaces.limits-of-sequences-premetric-spaces public
-open import metric-spaces.limits-of-sequences-pseudometric-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.metric-space-of-cauchy-approximations-complete-metric-spaces public
 open import metric-spaces.metric-space-of-cauchy-approximations-metric-spaces public
-open import metric-spaces.metric-space-of-cauchy-approximations-saturated-complete-metric-spaces public
 open import metric-spaces.metric-space-of-convergent-cauchy-approximations-metric-spaces public
 open import metric-spaces.metric-space-of-convergent-sequences-metric-spaces public
 open import metric-spaces.metric-space-of-functions-metric-spaces public
 open import metric-spaces.metric-space-of-isometries-metric-spaces public
 open import metric-spaces.metric-space-of-lipschitz-functions-metric-spaces public
 open import metric-spaces.metric-space-of-rational-numbers public
-open import metric-spaces.metric-space-of-rational-numbers-with-open-neighborhoods public
 open import metric-spaces.metric-space-of-short-functions-metric-spaces public
 open import metric-spaces.metric-spaces public
-open import metric-spaces.metric-structures public
-open import metric-spaces.monotonic-premetric-structures public
-open import metric-spaces.ordering-premetric-structures public
+open import metric-spaces.monotonic-rational-neighborhoods public
+open import metric-spaces.ordering-rational-neighborhoods public
 open import metric-spaces.precategory-of-metric-spaces-and-functions public
 open import metric-spaces.precategory-of-metric-spaces-and-isometries public
 open import metric-spaces.precategory-of-metric-spaces-and-short-functions public
-open import metric-spaces.premetric-spaces public
-open import metric-spaces.premetric-structures public
+open import metric-spaces.preimage-rational-neighborhoods public
 open import metric-spaces.pseudometric-spaces public
-open import metric-spaces.pseudometric-structures public
 open import metric-spaces.rational-approximations-of-zero public
 open import metric-spaces.rational-cauchy-approximations public
+open import metric-spaces.rational-neighborhoods public
 open import metric-spaces.rational-sequences-approximating-zero public
-open import metric-spaces.reflexive-premetric-structures public
-open import metric-spaces.saturated-complete-metric-spaces public
-open import metric-spaces.saturated-metric-spaces public
+open import metric-spaces.reflexive-rational-neighborhoods public
+open import metric-spaces.saturated-rational-neighborhoods public
 open import metric-spaces.sequences-metric-spaces public
-open import metric-spaces.sequences-premetric-spaces public
-open import metric-spaces.sequences-pseudometric-spaces public
 open import metric-spaces.short-functions-metric-spaces public
-open import metric-spaces.short-functions-premetric-spaces public
+open import metric-spaces.similarity-of-elements-pseudometric-spaces public
 open import metric-spaces.subspaces-metric-spaces public
-open import metric-spaces.symmetric-premetric-structures public
-open import metric-spaces.triangular-premetric-structures public
+open import metric-spaces.symmetric-rational-neighborhoods public
+open import metric-spaces.triangular-rational-neighborhoods public
 open import metric-spaces.uniformly-continuous-functions-metric-spaces public
-open import metric-spaces.uniformly-continuous-functions-premetric-spaces public
 ```
 
 ## References

src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md

@@ -9,18 +9,16 @@ module metric-spaces.cauchy-approximations-metric-spaces where
 ```agda
 open import elementary-number-theory.positive-rational-numbers
 
-open import foundation.binary-relations
 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
 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-premetric-spaces
-open import metric-spaces.limits-of-cauchy-approximations-premetric-spaces
 open import metric-spaces.metric-spaces
 open import metric-spaces.short-functions-metric-spaces
 ```
@@ -31,9 +29,11 @@ open import metric-spaces.short-functions-metric-spaces
 
 A
 {{#concept "Cauchy approximation" Disambiguation="in a metric space" Agda=is-cauchy-approximation-Metric-Space}}
-in a [metric space](metric-spaces.metric-spaces.md) is a
-[Cauchy approximation](metric-spaces.cauchy-approximations-premetric-spaces.md)
-in the carrier [premetric space](metric-spaces.premetric-spaces.md).
+in a [metric space](metric-spaces.metric-spaces.md) `A` is a map `f` from
+[`ℚ⁺`](elementary-number-theory.positive-rational-numbers.md) to its carrier
+type such that for all `(ε δ : ℚ⁺)`, `f ε` and `f δ` are in a
+(`ε + δ`)-[neighborhood](metric-spaces.rational-neighborhoods.md), i.e. the
+distance between `f ε` and `f δ` is bounded by `ε + δ`.
 
 ## Definitions
 
@@ -46,9 +46,14 @@ module _
 
   is-cauchy-approximation-prop-Metric-Space :
     (ℚ⁺ → type-Metric-Space A) → Prop l2
-  is-cauchy-approximation-prop-Metric-Space =
-    is-cauchy-approximation-prop-Premetric-Space
-      ( premetric-Metric-Space A)
+  is-cauchy-approximation-prop-Metric-Space f =
+    Π-Prop
+      ( ℚ⁺)
+      ( λ ε →
+        Π-Prop
+          ( ℚ⁺)
+          ( λ δ →
+            neighborhood-prop-Metric-Space A (ε +ℚ⁺ δ) (f ε) (f δ)))
 
   is-cauchy-approximation-Metric-Space :
     (ℚ⁺ → type-Metric-Space A) → UU l2
@@ -93,10 +98,10 @@ module _
   const-cauchy-approximation-Metric-Space :
     cauchy-approximation-Metric-Space A
   const-cauchy-approximation-Metric-Space =
-    (const ℚ⁺ x) , (λ ε δ → is-reflexive-structure-Metric-Space A (ε +ℚ⁺ δ) x)
+    (const ℚ⁺ x) , (λ ε δ → refl-neighborhood-Metric-Space A (ε +ℚ⁺ δ) x)
 ```
 
-### Short maps between metric spaces preserve Cauchy approximations
+### Short maps between metric spaces are functorial on Cauchy approximations
 
 ```agda
 module _
@@ -108,9 +113,69 @@ module _
   map-short-function-cauchy-approximation-Metric-Space :
     cauchy-approximation-Metric-Space A →
     cauchy-approximation-Metric-Space B
-  map-short-function-cauchy-approximation-Metric-Space =
-    map-short-function-cauchy-approximation-Premetric-Space
-      ( premetric-Metric-Space A)
-      ( premetric-Metric-Space B)
+  map-short-function-cauchy-approximation-Metric-Space (u , H) =
+    ( map-short-function-Metric-Space A B f ∘ u) ,
+    ( λ ε δ →
+      is-short-map-short-function-Metric-Space
+      ( A)
+      ( B)
       ( f)
+      ( ε +ℚ⁺ δ)
+      ( u ε)
+      ( u δ)
+      ( H ε δ))
+
+module _
+  {l1 l2 : Level}
+  (A : Metric-Space l1 l2)
+  where
+
+  eq-id-map-short-function-cauchy-approximation-Metric-Space :
+    map-short-function-cauchy-approximation-Metric-Space
+      ( A)
+      ( A)
+      ( short-id-Metric-Space A) ＝
+    id
+  eq-id-map-short-function-cauchy-approximation-Metric-Space = refl
+
+module _
+  {l1a l2a l1b l2b l1c l2c : Level}
+  (A : Metric-Space l1a l2a)
+  (B : Metric-Space l1b l2b)
+  (C : Metric-Space l1c l2c)
+  (g : short-function-Metric-Space B C)
+  (f : short-function-Metric-Space A B)
+  where
+
+  eq-comp-map-short-function-cauchy-approximation-Metric-Space :
+    ( map-short-function-cauchy-approximation-Metric-Space B C g ∘
+      map-short-function-cauchy-approximation-Metric-Space A B f) ＝
+    ( map-short-function-cauchy-approximation-Metric-Space A C
+      (comp-short-function-Metric-Space A B C g f))
+  eq-comp-map-short-function-cauchy-approximation-Metric-Space = refl
 ```
+
+### Homotopic cauchy approximations are equal
+
+```agda
+module _
+  { l1 l2 : Level} (A : Metric-Space l1 l2)
+  { f g : cauchy-approximation-Metric-Space A}
+  ( f~g :
+    map-cauchy-approximation-Metric-Space A f ~
+    map-cauchy-approximation-Metric-Space A g)
+  where
+
+  eq-htpy-cauchy-approximation-Metric-Space : f ＝ g
+  eq-htpy-cauchy-approximation-Metric-Space =
+    eq-type-subtype
+      ( is-cauchy-approximation-prop-Metric-Space A)
+      ( eq-htpy f~g)
+```
+
+## References
+
+Our definition of Cauchy approximation follows Definition 4.5.5 of
+{{#cite Booij20PhD}} and Definition 11.2.10 of {{#cite UF13}}.
+
+{{#bibliography}}