Metric pseudocompletion of pseudometric spaces

src/metric-spaces.lagda.md

@@ -89,6 +89,9 @@ 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-pseudocompletion-of-metric-spaces public
+open import metric-spaces.metric-pseudocompletion-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
 open import metric-spaces.metric-space-of-convergent-cauchy-approximations-metric-spaces public
@@ -112,6 +115,8 @@ 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.preimages-rational-neighborhood-relations public
+open import metric-spaces.pseudometric-completion-of-metric-spaces public
+open import metric-spaces.pseudometric-completion-of-pseudometric-spaces public
 open import metric-spaces.pseudometric-spaces public
 open import metric-spaces.rational-approximations-of-zero public
 open import metric-spaces.rational-cauchy-approximations public

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

@@ -11,8 +11,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
@@ -140,3 +142,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

@@ -143,6 +143,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