Lemmas metric spaces (#1618)

This PR introduces a few lemmas on (pseudo)metric spaces.

- any complete metric space is a retract of its metric space of Cauchy
approximations;
- constant Cauchy approximations are convergent;
- any metric space is a retract of its convergent Cauchy approximations;
- short maps from a pseudometric space to a metric space reflect
similarity.

Author: malarbol

src/metric-spaces/cauchy-sequences-complete-metric-spaces.lagda.md

@@ -90,8 +90,8 @@ module _
       ( metric-space-Complete-Metric-Space M)
       ( x)
   has-limit-cauchy-sequence-Complete-Metric-Space =
-    limit-cauchy-sequence-Complete-Metric-Space ,
-    is-limit-limit-cauchy-sequence-Complete-Metric-Space
+    ( limit-cauchy-sequence-Complete-Metric-Space ,
+      is-limit-limit-cauchy-sequence-Complete-Metric-Space)
 ```
 
 ### If every Cauchy sequence has a limit in a metric space, the metric space is complete
@@ -123,5 +123,5 @@ module _
   complete-metric-space-cauchy-sequences-have-limits-Metric-Space :
     Complete-Metric-Space l1 l2
   complete-metric-space-cauchy-sequences-have-limits-Metric-Space =
-    M , is-complete-metric-space-cauchy-sequences-have-limits-Metric-Space
+    ( M , is-complete-metric-space-cauchy-sequences-have-limits-Metric-Space)
 ```

src/metric-spaces/complete-metric-spaces.lagda.md

@@ -12,9 +12,12 @@ open import elementary-number-theory.positive-rational-numbers
 open import foundation.binary-relations
 open import foundation.dependent-pair-types
 open import foundation.equivalences
+open import foundation.function-types
+open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.retractions
+open import foundation.retracts-of-types
 open import foundation.sections
 open import foundation.subtypes
 open import foundation.universe-levels
@@ -23,6 +26,7 @@ open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.convergent-cauchy-approximations-metric-spaces
 open import metric-spaces.limits-of-cauchy-approximations-metric-spaces
 open import metric-spaces.metric-spaces
+open import metric-spaces.pseudometric-spaces
 ```
 
 </details>
@@ -80,6 +84,10 @@ module _
   metric-space-Complete-Metric-Space : Metric-Space l1 l2
   metric-space-Complete-Metric-Space = pr1 A
 
+  pseudometric-space-Complete-Metric-Space : Pseudometric-Space l1 l2
+  pseudometric-space-Complete-Metric-Space =
+    pseudometric-Metric-Space metric-space-Complete-Metric-Space
+
   type-Complete-Metric-Space : UU l1
   type-Complete-Metric-Space =
     type-Metric-Space metric-space-Complete-Metric-Space
@@ -122,13 +130,13 @@ module _
         ( metric-space-Complete-Metric-Space A))
       ( refl)
 
-  is-retraction-convergent-cauchy-approximation-Metric-Space :
+  is-retraction-convergent-cauchy-approximation-Complete-Metric-Space :
     is-retraction
       ( convergent-cauchy-approximation-Complete-Metric-Space)
       ( inclusion-subtype
         ( is-convergent-prop-cauchy-approximation-Metric-Space
           ( metric-space-Complete-Metric-Space A)))
-  is-retraction-convergent-cauchy-approximation-Metric-Space u = refl
+  is-retraction-convergent-cauchy-approximation-Complete-Metric-Space u = refl
 
   is-equiv-convergent-cauchy-approximation-Complete-Metric-Space :
     is-equiv convergent-cauchy-approximation-Complete-Metric-Space
@@ -141,7 +149,7 @@ module _
     ( inclusion-subtype
       ( is-convergent-prop-cauchy-approximation-Metric-Space
         ( metric-space-Complete-Metric-Space A))) ,
-    ( is-retraction-convergent-cauchy-approximation-Metric-Space)
+    ( is-retraction-convergent-cauchy-approximation-Complete-Metric-Space)
 ```
 
 ### The limit of a Cauchy approximation in a complete metric space
@@ -172,6 +180,52 @@ module _
       ( convergent-cauchy-approximation-Complete-Metric-Space A u)
 ```
 
+### Any complete metric space is a retract of its type of Cauchy approximations
+
+```agda
+module _
+  {l1 l2 : Level} (A : Complete-Metric-Space l1 l2)
+  where
+
+  abstract
+    is-retraction-limit-cauchy-approximation-Complete-Metric-Space :
+      ( limit-cauchy-approximation-Complete-Metric-Space A ∘
+        const-cauchy-approximation-Metric-Space
+          ( metric-space-Complete-Metric-Space A)) ~
+      ( id)
+    is-retraction-limit-cauchy-approximation-Complete-Metric-Space x =
+      all-eq-is-limit-cauchy-approximation-Metric-Space
+        ( metric-space-Complete-Metric-Space A)
+        ( const-cauchy-approximation-Metric-Space
+          ( metric-space-Complete-Metric-Space A)
+          ( x))
+        ( limit-cauchy-approximation-Complete-Metric-Space
+          ( A)
+          ( const-cauchy-approximation-Metric-Space
+            ( metric-space-Complete-Metric-Space A)
+            ( x)))
+        ( x)
+        ( is-limit-limit-cauchy-approximation-Complete-Metric-Space
+          ( A)
+          ( const-cauchy-approximation-Metric-Space
+            ( metric-space-Complete-Metric-Space A)
+            ( x)))
+        ( is-limit-const-cauchy-approximation-Metric-Space
+          ( metric-space-Complete-Metric-Space A)
+          ( x))
+
+  retract-limit-cauchy-approximation-Complete-Metric-Space :
+    retract
+      ( cauchy-approximation-Metric-Space
+        ( metric-space-Complete-Metric-Space A))
+      ( type-Complete-Metric-Space A)
+  retract-limit-cauchy-approximation-Complete-Metric-Space =
+    ( ( const-cauchy-approximation-Metric-Space
+        ( metric-space-Complete-Metric-Space A)) ,
+      ( limit-cauchy-approximation-Complete-Metric-Space A) ,
+      ( is-retraction-limit-cauchy-approximation-Complete-Metric-Space))
+```
+
 ### Saturation of the limit
 
 ```agda

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

@@ -12,8 +12,10 @@ open import elementary-number-theory.positive-rational-numbers
 
 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.retracts-of-types
 open import foundation.subtypes
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
@@ -141,3 +143,51 @@ module _
       ( limit-convergent-cauchy-approximation-Metric-Space)
   is-limit-limit-convergent-cauchy-approximation-Metric-Space = pr2 (pr2 f)
 ```
+
+## Properties
+
+### Constant Cauchy approximations are convergent
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  (x : type-Metric-Space A)
+  where
+
+  is-convergent-const-cauchy-approximation-Metric-Space :
+    is-convergent-cauchy-approximation-Metric-Space
+      ( A)
+      ( const-cauchy-approximation-Metric-Space A x)
+  is-convergent-const-cauchy-approximation-Metric-Space =
+    ( x , is-limit-const-cauchy-approximation-Metric-Space A x)
+
+  convergent-const-cauchy-approximation-Metric-Space :
+    convergent-cauchy-approximation-Metric-Space A
+  convergent-const-cauchy-approximation-Metric-Space =
+    ( const-cauchy-approximation-Metric-Space A x ,
+      is-convergent-const-cauchy-approximation-Metric-Space)
+```
+
+### Any metric space is a retract of its type of convergent Cauchy approximations
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  where
+
+  abstract
+    is-retraction-convergent-cauchy-approximation-Metric-Space :
+      ( limit-convergent-cauchy-approximation-Metric-Space A ∘
+        convergent-const-cauchy-approximation-Metric-Space A) ~
+      ( id)
+    is-retraction-convergent-cauchy-approximation-Metric-Space x = refl
+
+  retract-convergent-cauchy-approximation-Metric-Space :
+    retract
+      ( convergent-cauchy-approximation-Metric-Space A)
+      ( type-Metric-Space A)
+  retract-convergent-cauchy-approximation-Metric-Space =
+    ( convergent-const-cauchy-approximation-Metric-Space A ,
+      limit-convergent-cauchy-approximation-Metric-Space A ,
+      is-retraction-convergent-cauchy-approximation-Metric-Space)
+```

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

@@ -123,6 +123,25 @@ module _
       ( all-sim-is-limit-cauchy-approximation-Metric-Space lim-x lim-y)
 ```
 
+### The value of a constant Cauchy approximation is its limit
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  (x : type-Metric-Space A)
+  where
+
+  is-limit-const-cauchy-approximation-Metric-Space :
+    is-limit-cauchy-approximation-Metric-Space
+      ( A)
+      ( const-cauchy-approximation-Metric-Space A x)
+      ( x)
+  is-limit-const-cauchy-approximation-Metric-Space =
+    is-limit-const-cauchy-approximation-Pseudometric-Space
+      ( pseudometric-Metric-Space A)
+      ( x)
+```
+
 ## See also
 
 - [Convergent cauchy approximations](metric-spaces.convergent-cauchy-approximations-metric-spaces.md)

src/metric-spaces/limits-of-cauchy-approximations-pseudometric-spaces.lagda.md

@@ -145,6 +145,23 @@ module _
         ( Nxy)
 ```
 
+### The value of a constant Cauchy approximation is its limit
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
+  (x : type-Pseudometric-Space A)
+  where
+
+  is-limit-const-cauchy-approximation-Pseudometric-Space :
+    is-limit-cauchy-approximation-Pseudometric-Space
+      ( A)
+      ( const-cauchy-approximation-Pseudometric-Space A x)
+      ( x)
+  is-limit-const-cauchy-approximation-Pseudometric-Space ε δ =
+    refl-neighborhood-Pseudometric-Space A _ x
+```
+
 ## References
 
 Our definition of limit of Cauchy approximation follows Definition 11.2.10 of

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

@@ -21,6 +21,7 @@ open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions
+open import foundation.reflecting-maps-equivalence-relations
 open import foundation.sets
 open import foundation.subtypes
 open import foundation.transport-along-identifications
@@ -34,6 +35,7 @@ open import metric-spaces.pseudometric-spaces
 open import metric-spaces.rational-neighborhood-relations
 open import metric-spaces.reflexive-rational-neighborhood-relations
 open import metric-spaces.saturated-rational-neighborhood-relations
+open import metric-spaces.short-functions-pseudometric-spaces
 open import metric-spaces.similarity-of-elements-pseudometric-spaces
 open import metric-spaces.symmetric-rational-neighborhood-relations
 open import metric-spaces.triangular-rational-neighborhood-relations
@@ -340,6 +342,63 @@ module _
     map-inv-equiv (equiv-sim-eq-Metric-Space x y)
 ```
 
+### Short maps from a pseudometric space to a metric space reflect similarity
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2)
+  (B : Metric-Space l1' l2')
+  (f : short-function-Pseudometric-Space A (pseudometric-Metric-Space B))
+  where
+
+  abstract
+    reflects-sim-map-short-function-metric-space-Pseudometric-Space :
+      {x y : type-Pseudometric-Space A} →
+      sim-Pseudometric-Space A x y →
+      map-short-function-Pseudometric-Space
+        ( A)
+        ( pseudometric-Metric-Space B)
+        ( f)
+        ( x) ＝
+      map-short-function-Pseudometric-Space
+        ( A)
+        ( pseudometric-Metric-Space B)
+        ( f)
+        ( y)
+    reflects-sim-map-short-function-metric-space-Pseudometric-Space
+      {x} {y} x~y =
+      eq-sim-Metric-Space B
+        ( map-short-function-Pseudometric-Space
+          ( A)
+          ( pseudometric-Metric-Space B)
+          ( f)
+          ( x))
+        ( map-short-function-Pseudometric-Space
+          ( A)
+          ( pseudometric-Metric-Space B)
+          ( f)
+          ( y))
+        ( preserves-sim-map-short-function-Pseudometric-Space
+          ( A)
+          ( pseudometric-Metric-Space B)
+          ( f)
+          ( x)
+          ( y)
+          ( x~y))
+
+  reflecting-map-short-function-metric-space-Pseudometric-Space :
+    reflecting-map-equivalence-relation
+      ( equivalence-relation-sim-Pseudometric-Space A)
+      ( type-Metric-Space B)
+  reflecting-map-short-function-metric-space-Pseudometric-Space =
+    ( ( map-short-function-Pseudometric-Space
+        ( A)
+        ( pseudometric-Metric-Space B)
+        ( f)) ,
+      ( reflects-sim-map-short-function-metric-space-Pseudometric-Space))
+```
+
 ## See also
 
 - Metric spaces that _are_ defined by a distance function are defined in

src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md

@@ -232,13 +232,21 @@ module _
   {l1 l2 : Level}
   (A B : Metric-Space l1 l2)
   where
+
   equiv-isometric-equiv-iso-short-function-Metric-Space' :
     iso-Precategory precategory-short-function-Metric-Space A B ≃
     isometric-equiv-Metric-Space' A B
   equiv-isometric-equiv-iso-short-function-Metric-Space' =
     ( equiv-tot
       ( equiv-is-isometric-equiv-is-iso-short-function-Metric-Space A B)) ∘e
     ( associative-Σ)
+
+  map-equiv-isometric-equiv-iso-short-function-Metric-Space' :
+    iso-Precategory precategory-short-function-Metric-Space A B →
+    isometric-equiv-Metric-Space' A B
+  map-equiv-isometric-equiv-iso-short-function-Metric-Space' =
+    map-equiv
+      ( equiv-isometric-equiv-iso-short-function-Metric-Space')
 ```
 
 ## See also