Pseudometric completion

src/metric-spaces.lagda.md

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

@@ -38,13 +38,13 @@ module _
 
   cauchy-sequence-Complete-Metric-Space : UU (l1 ⊔ l2)
   cauchy-sequence-Complete-Metric-Space =
-    cauchy-sequence-Metric-Space (metric-space-Complete-Metric-Space M)
+    cauchy-sequence-Metric-Space (metric-Complete-Metric-Space M)
 
   is-limit-cauchy-sequence-Complete-Metric-Space :
     cauchy-sequence-Complete-Metric-Space → type-Complete-Metric-Space M → UU l2
   is-limit-cauchy-sequence-Complete-Metric-Space x l =
     is-limit-cauchy-sequence-Metric-Space
-      ( metric-space-Complete-Metric-Space M)
+      ( metric-Complete-Metric-Space M)
       ( x)
       ( l)
 ```
@@ -62,10 +62,10 @@ module _
   limit-cauchy-sequence-Complete-Metric-Space : type-Complete-Metric-Space M
   limit-cauchy-sequence-Complete-Metric-Space =
     pr1
-      ( is-complete-metric-space-Complete-Metric-Space
+      ( is-complete-metric-Complete-Metric-Space
         ( M)
         ( cauchy-approximation-cauchy-sequence-Metric-Space
-          ( metric-space-Complete-Metric-Space M)
+          ( metric-Complete-Metric-Space M)
           ( x)))
 
   is-limit-limit-cauchy-sequence-Complete-Metric-Space :
@@ -75,23 +75,23 @@ module _
       ( limit-cauchy-sequence-Complete-Metric-Space)
   is-limit-limit-cauchy-sequence-Complete-Metric-Space =
     is-limit-cauchy-sequence-limit-cauchy-approximation-cauchy-sequence-Metric-Space
-      ( metric-space-Complete-Metric-Space M)
+      ( metric-Complete-Metric-Space M)
       ( x)
       ( limit-cauchy-sequence-Complete-Metric-Space)
       ( pr2
-        ( is-complete-metric-space-Complete-Metric-Space
+        ( is-complete-metric-Complete-Metric-Space
           ( M)
           ( cauchy-approximation-cauchy-sequence-Metric-Space
-            ( metric-space-Complete-Metric-Space M)
+            ( metric-Complete-Metric-Space M)
             ( x))))
 
   has-limit-cauchy-sequence-Complete-Metric-Space :
     has-limit-cauchy-sequence-Metric-Space
-      ( metric-space-Complete-Metric-Space M)
+      ( metric-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

@@ -22,6 +22,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>
@@ -76,16 +77,20 @@ module _
   (A : Complete-Metric-Space l1 l2)
   where
 
-  metric-space-Complete-Metric-Space : Metric-Space l1 l2
-  metric-space-Complete-Metric-Space = pr1 A
+  metric-Complete-Metric-Space : Metric-Space l1 l2
+  metric-Complete-Metric-Space = pr1 A
+
+  pseudometric-Complete-Metric-Space : Pseudometric-Space l1 l2
+  pseudometric-Complete-Metric-Space =
+    pseudometric-Metric-Space metric-Complete-Metric-Space
 
   type-Complete-Metric-Space : UU l1
   type-Complete-Metric-Space =
-    type-Metric-Space metric-space-Complete-Metric-Space
+    type-Metric-Space metric-Complete-Metric-Space
 
-  is-complete-metric-space-Complete-Metric-Space :
-    is-complete-Metric-Space metric-space-Complete-Metric-Space
-  is-complete-metric-space-Complete-Metric-Space = pr2 A
+  is-complete-metric-Complete-Metric-Space :
+    is-complete-Metric-Space metric-Complete-Metric-Space
+  is-complete-metric-Complete-Metric-Space = pr2 A
 ```
 
 ### The equivalence between Cauchy approximations and convergent Cauchy approximations in a complete metric space
@@ -98,43 +103,43 @@ module _
 
   convergent-cauchy-approximation-Complete-Metric-Space :
     cauchy-approximation-Metric-Space
-      ( metric-space-Complete-Metric-Space A) →
+      ( metric-Complete-Metric-Space A) →
     convergent-cauchy-approximation-Metric-Space
-      ( metric-space-Complete-Metric-Space A)
+      ( metric-Complete-Metric-Space A)
   convergent-cauchy-approximation-Complete-Metric-Space u =
-    ( u , is-complete-metric-space-Complete-Metric-Space A u)
+    ( u , is-complete-metric-Complete-Metric-Space A u)
 
   is-section-convergent-cauchy-approximation-Complete-Metric-Space :
     is-section
       ( convergent-cauchy-approximation-Complete-Metric-Space)
       ( inclusion-subtype
         ( is-convergent-prop-cauchy-approximation-Metric-Space
-          ( metric-space-Complete-Metric-Space A)))
+          ( metric-Complete-Metric-Space A)))
   is-section-convergent-cauchy-approximation-Complete-Metric-Space u =
     eq-type-subtype
       ( is-convergent-prop-cauchy-approximation-Metric-Space
-        ( metric-space-Complete-Metric-Space A))
+        ( metric-Complete-Metric-Space A))
       ( refl)
 
   is-retraction-convergent-cauchy-approximation-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)))
+          ( metric-Complete-Metric-Space A)))
   is-retraction-convergent-cauchy-approximation-Metric-Space u = refl
 
   is-equiv-convergent-cauchy-approximation-Complete-Metric-Space :
     is-equiv convergent-cauchy-approximation-Complete-Metric-Space
   pr1 is-equiv-convergent-cauchy-approximation-Complete-Metric-Space =
     ( inclusion-subtype
       ( is-convergent-prop-cauchy-approximation-Metric-Space
-        ( metric-space-Complete-Metric-Space A))) ,
+        ( metric-Complete-Metric-Space A))) ,
     ( is-section-convergent-cauchy-approximation-Complete-Metric-Space)
   pr2 is-equiv-convergent-cauchy-approximation-Complete-Metric-Space =
     ( inclusion-subtype
       ( is-convergent-prop-cauchy-approximation-Metric-Space
-        ( metric-space-Complete-Metric-Space A))) ,
+        ( metric-Complete-Metric-Space A))) ,
     ( is-retraction-convergent-cauchy-approximation-Metric-Space)
 ```
 
@@ -145,24 +150,24 @@ module _
   { l1 l2 : Level}
   ( A : Complete-Metric-Space l1 l2)
   ( u : cauchy-approximation-Metric-Space
-    ( metric-space-Complete-Metric-Space A))
+    ( metric-Complete-Metric-Space A))
   where
 
   limit-cauchy-approximation-Complete-Metric-Space :
     type-Complete-Metric-Space A
   limit-cauchy-approximation-Complete-Metric-Space =
     limit-convergent-cauchy-approximation-Metric-Space
-      ( metric-space-Complete-Metric-Space A)
+      ( metric-Complete-Metric-Space A)
       ( convergent-cauchy-approximation-Complete-Metric-Space A u)
 
   is-limit-limit-cauchy-approximation-Complete-Metric-Space :
     is-limit-cauchy-approximation-Metric-Space
-      ( metric-space-Complete-Metric-Space A)
+      ( metric-Complete-Metric-Space A)
       ( u)
       ( limit-cauchy-approximation-Complete-Metric-Space)
   is-limit-limit-cauchy-approximation-Complete-Metric-Space =
     is-limit-limit-convergent-cauchy-approximation-Metric-Space
-      ( metric-space-Complete-Metric-Space A)
+      ( metric-Complete-Metric-Space A)
       ( convergent-cauchy-approximation-Complete-Metric-Space A u)
 ```
 

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

@@ -140,3 +140,26 @@ 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)
+
+  const-convergent-cauchy-approximation-Metric-Space :
+    convergent-cauchy-approximation-Metric-Space A
+  const-convergent-cauchy-approximation-Metric-Space =
+    ( const-cauchy-approximation-Metric-Space A x ,
+      is-convergent-const-cauchy-approximation-Metric-Space)
+```

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

@@ -259,10 +259,10 @@ module _
 
   Π-Complete-Metric-Space : Complete-Metric-Space (l ⊔ l1) (l ⊔ l2)
   pr1 Π-Complete-Metric-Space =
-    Π-Metric-Space A (metric-space-Complete-Metric-Space ∘ C)
+    Π-Metric-Space A (metric-Complete-Metric-Space ∘ C)
   pr2 Π-Complete-Metric-Space =
     is-complete-Π-Metric-Space
       ( A)
-      ( metric-space-Complete-Metric-Space ∘ C)
-      ( is-complete-metric-space-Complete-Metric-Space ∘ C)
+      ( metric-Complete-Metric-Space ∘ C)
+      ( is-complete-metric-Complete-Metric-Space ∘ C)
 ```

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

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

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