diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md
index 63dca9f747..a1a56b6100 100644
--- a/src/metric-spaces.lagda.md
+++ b/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
diff --git a/src/metric-spaces/cauchy-sequences-complete-metric-spaces.lagda.md b/src/metric-spaces/cauchy-sequences-complete-metric-spaces.lagda.md
index 7a77f2ac4e..fa7095efe7 100644
--- a/src/metric-spaces/cauchy-sequences-complete-metric-spaces.lagda.md
+++ b/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)
 ```
diff --git a/src/metric-spaces/complete-metric-spaces.lagda.md b/src/metric-spaces/complete-metric-spaces.lagda.md
index 6914e67ad3..8cc91ef79d 100644
--- a/src/metric-spaces/complete-metric-spaces.lagda.md
+++ b/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,22 +103,22 @@ 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 :
@@ -121,7 +126,7 @@ module _
       ( 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 :
@@ -129,12 +134,12 @@ module _
   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)
 ```
 
diff --git a/src/metric-spaces/convergent-cauchy-approximations-metric-spaces.lagda.md b/src/metric-spaces/convergent-cauchy-approximations-metric-spaces.lagda.md
index 4f90c77140..47e2e50ccf 100644
--- a/src/metric-spaces/convergent-cauchy-approximations-metric-spaces.lagda.md
+++ b/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)
+```
diff --git a/src/metric-spaces/dependent-products-metric-spaces.lagda.md b/src/metric-spaces/dependent-products-metric-spaces.lagda.md
index 2675d11b69..b0f89b30a2 100644
--- a/src/metric-spaces/dependent-products-metric-spaces.lagda.md
+++ b/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)
 ```
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 57833b4662..83918ce0a7 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
@@ -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)
diff --git a/src/metric-spaces/limits-of-cauchy-approximations-pseudometric-spaces.lagda.md b/src/metric-spaces/limits-of-cauchy-approximations-pseudometric-spaces.lagda.md
index 39065cd977..1a7fdbe625 100644
--- a/src/metric-spaces/limits-of-cauchy-approximations-pseudometric-spaces.lagda.md
+++ b/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
diff --git a/src/metric-spaces/metric-space-of-cauchy-approximations-complete-metric-spaces.lagda.md b/src/metric-spaces/metric-space-of-cauchy-approximations-complete-metric-spaces.lagda.md
index f5837b183e..ab1c863cc4 100644
--- a/src/metric-spaces/metric-space-of-cauchy-approximations-complete-metric-spaces.lagda.md
+++ b/src/metric-spaces/metric-space-of-cauchy-approximations-complete-metric-spaces.lagda.md
@@ -61,7 +61,7 @@ module _
     Metric-Space (l1 ⊔ l2) l2
   metric-space-of-cauchy-approximations-Complete-Metric-Space =
     metric-space-of-cauchy-approximations-Metric-Space
-      ( metric-space-Complete-Metric-Space A)
+      ( metric-Complete-Metric-Space A)
 ```
 
 ## Properties
@@ -77,7 +77,7 @@ module _
     is-isometry-Metric-Space
       ( metric-space-of-cauchy-approximations-Complete-Metric-Space A)
       ( metric-space-of-convergent-cauchy-approximations-Metric-Space
-        ( metric-space-Complete-Metric-Space A))
+        ( metric-Complete-Metric-Space A))
       ( convergent-cauchy-approximation-Complete-Metric-Space A)
   is-isometry-convergent-cauchy-approximation-Complete-Metric-Space d x y =
     (id , id)
@@ -86,7 +86,7 @@ module _
     isometry-Metric-Space
       ( metric-space-of-cauchy-approximations-Complete-Metric-Space A)
       ( metric-space-of-convergent-cauchy-approximations-Metric-Space
-        ( metric-space-Complete-Metric-Space A))
+        ( metric-Complete-Metric-Space A))
   isometry-convergent-cauchy-approximation-Complete-Metric-Space =
     convergent-cauchy-approximation-Complete-Metric-Space A ,
     is-isometry-convergent-cauchy-approximation-Complete-Metric-Space
@@ -102,12 +102,12 @@ module _
   eq-metric-space-convergent-cauchy-approximations-Complete-Metric-Space :
     ( metric-space-of-cauchy-approximations-Complete-Metric-Space A) ＝
     ( metric-space-of-convergent-cauchy-approximations-Metric-Space
-      ( metric-space-Complete-Metric-Space A))
+      ( metric-Complete-Metric-Space A))
   eq-metric-space-convergent-cauchy-approximations-Complete-Metric-Space =
     eq-isometric-equiv-Metric-Space'
       ( metric-space-of-cauchy-approximations-Complete-Metric-Space A)
       ( metric-space-of-convergent-cauchy-approximations-Metric-Space
-        ( metric-space-Complete-Metric-Space A))
+        ( metric-Complete-Metric-Space A))
       ( convergent-cauchy-approximation-Complete-Metric-Space A ,
         is-equiv-convergent-cauchy-approximation-Complete-Metric-Space A ,
         is-isometry-convergent-cauchy-approximation-Complete-Metric-Space A)
@@ -124,25 +124,25 @@ module _
     short-function-Metric-Space
       ( metric-space-of-cauchy-approximations-Complete-Metric-Space A)
       ( metric-space-of-convergent-cauchy-approximations-Metric-Space
-        ( metric-space-Complete-Metric-Space A))
+        ( metric-Complete-Metric-Space A))
   short-convergent-cauchy-approximation-Complete-Metric-Space =
     short-isometry-Metric-Space
       ( metric-space-of-cauchy-approximations-Complete-Metric-Space A)
       ( metric-space-of-convergent-cauchy-approximations-Metric-Space
-        ( metric-space-Complete-Metric-Space A))
+        ( metric-Complete-Metric-Space A))
       ( isometry-convergent-cauchy-approximation-Complete-Metric-Space A)
 
   is-short-convergent-cauchy-approximation-Complete-Metric-Space :
     is-short-function-Metric-Space
       ( metric-space-of-cauchy-approximations-Complete-Metric-Space A)
       ( metric-space-of-convergent-cauchy-approximations-Metric-Space
-        ( metric-space-Complete-Metric-Space A))
+        ( metric-Complete-Metric-Space A))
       ( convergent-cauchy-approximation-Complete-Metric-Space A)
   is-short-convergent-cauchy-approximation-Complete-Metric-Space =
     is-short-map-short-function-Metric-Space
       ( metric-space-of-cauchy-approximations-Complete-Metric-Space A)
       ( metric-space-of-convergent-cauchy-approximations-Metric-Space
-        ( metric-space-Complete-Metric-Space A))
+        ( metric-Complete-Metric-Space A))
       ( short-convergent-cauchy-approximation-Complete-Metric-Space)
 ```
 
@@ -156,26 +156,26 @@ module _
   short-limit-cauchy-approximation-Complete-Metric-Space :
     short-function-Metric-Space
       ( metric-space-of-cauchy-approximations-Complete-Metric-Space A)
-      ( metric-space-Complete-Metric-Space A)
+      ( metric-Complete-Metric-Space A)
   short-limit-cauchy-approximation-Complete-Metric-Space =
     comp-short-function-Metric-Space
       ( metric-space-of-cauchy-approximations-Complete-Metric-Space A)
       ( metric-space-of-convergent-cauchy-approximations-Metric-Space
-        ( metric-space-Complete-Metric-Space A))
-      ( metric-space-Complete-Metric-Space A)
+        ( metric-Complete-Metric-Space A))
+      ( metric-Complete-Metric-Space A)
       ( short-limit-convergent-cauchy-approximation-Metric-Space
-        ( metric-space-Complete-Metric-Space A))
+        ( metric-Complete-Metric-Space A))
       ( short-convergent-cauchy-approximation-Complete-Metric-Space A)
 
   is-short-limit-cauchy-approximation-Complete-Metric-Space :
     is-short-function-Metric-Space
       ( metric-space-of-cauchy-approximations-Complete-Metric-Space A)
-      ( metric-space-Complete-Metric-Space A)
+      ( metric-Complete-Metric-Space A)
       ( limit-cauchy-approximation-Complete-Metric-Space A)
   is-short-limit-cauchy-approximation-Complete-Metric-Space =
     is-short-map-short-function-Metric-Space
       ( metric-space-of-cauchy-approximations-Complete-Metric-Space A)
-      ( metric-space-Complete-Metric-Space A)
+      ( metric-Complete-Metric-Space A)
       ( short-limit-cauchy-approximation-Complete-Metric-Space)
 ```
 
@@ -204,13 +204,13 @@ module _
     limit-cauchy-approximation-Complete-Metric-Space
       ( A)
       ( map-swap-cauchy-approximation-Metric-Space
-        ( metric-space-Complete-Metric-Space A)
+        ( metric-Complete-Metric-Space A)
         ( U)
         ( η))
 
   is-cauchy-map-lim-cauchy-approximation-cauchy-approximations-Complete-Metric-Space :
     is-cauchy-approximation-Metric-Space
-      ( metric-space-Complete-Metric-Space A)
+      ( metric-Complete-Metric-Space A)
       ( map-lim-cauchy-approximation-cauchy-approximations-Complete-Metric-Space)
   is-cauchy-map-lim-cauchy-approximation-cauchy-approximations-Complete-Metric-Space
     ε δ =
@@ -218,16 +218,16 @@ module _
       ( A)
       ( ε +ℚ⁺ δ)
       ( map-swap-cauchy-approximation-Metric-Space
-        ( metric-space-Complete-Metric-Space A)
+        ( metric-Complete-Metric-Space A)
         ( U)
         ( ε))
       ( map-swap-cauchy-approximation-Metric-Space
-        ( metric-space-Complete-Metric-Space A)
+        ( metric-Complete-Metric-Space A)
         ( U)
         ( δ))
       ( λ η →
         is-cauchy-approximation-map-cauchy-approximation-Metric-Space
-          ( metric-space-Complete-Metric-Space A)
+          ( metric-Complete-Metric-Space A)
           ( map-cauchy-approximation-Metric-Space
             ( metric-space-of-cauchy-approximations-Complete-Metric-Space
               ( A))
@@ -237,8 +237,7 @@ module _
           ( δ))
 
   lim-cauchy-approximation-cauchy-approximations-Complete-Metric-Space :
-    cauchy-approximation-Metric-Space
-      (metric-space-Complete-Metric-Space A)
+    cauchy-approximation-Metric-Space (metric-Complete-Metric-Space A)
   lim-cauchy-approximation-cauchy-approximations-Complete-Metric-Space
     =
     map-lim-cauchy-approximation-cauchy-approximations-Complete-Metric-Space ,
@@ -255,7 +254,7 @@ module _
     is-limit-limit-cauchy-approximation-Complete-Metric-Space
       ( A)
       ( map-swap-cauchy-approximation-Metric-Space
-        ( metric-space-Complete-Metric-Space A)
+        ( metric-Complete-Metric-Space A)
         ( U)
         ( η))
       ( ε)
diff --git a/src/metric-spaces/pseudometric-completion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/pseudometric-completion-of-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..60fa9a4d9f
--- /dev/null
+++ b/src/metric-spaces/pseudometric-completion-of-pseudometric-spaces.lagda.md
@@ -0,0 +1,589 @@
+# The pseudometric completion of a pseudometric space
+
+```agda
+module metric-spaces.pseudometric-completion-of-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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
+
+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
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "pseudometric completion" Disambiguation="of a pseudometric space" Agda=pseudometric-completion-Pseudometric-Space}}
+of a [pseudometric space](metric-spaces.pseudometric-spaces.md) `M` is the
+pseudometric space of
+[Cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md)
+in `M` where two Cauchy approximations `x` and `y` are in a
+[`d`-neighborhood](metric-spaces.rational-neighborhood-relations.md) of one
+another if for all `δ ε : ℚ⁺`, `x δ` and `y ε` are in a
+`(δ + ε + d)`-neighborhood of one another in `M`.
+
+Any Cauchy approximation in the pseudometric completion has a
+[limit](metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces.md).
+
+## Definition
+
+### The pseudometric completion neighborhood relation on the type of Cauchy approximations in a pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  neighborhood-prop-pseudometric-completion-Pseudometric-Space :
+    Rational-Neighborhood-Relation l2
+      (cauchy-approximation-Pseudometric-Space M)
+  neighborhood-prop-pseudometric-completion-Pseudometric-Space
+    d x y =
+      Π-Prop
+        ( ℚ⁺)
+        ( λ δ →
+          Π-Prop
+            ( ℚ⁺)
+            ( λ ε →
+              neighborhood-prop-Pseudometric-Space
+                ( M)
+                ( δ +ℚ⁺ ε +ℚ⁺ d)
+                ( map-cauchy-approximation-Pseudometric-Space M x δ)
+                ( map-cauchy-approximation-Pseudometric-Space M y ε)))
+
+  neighborhood-pseudometric-completion-Pseudometric-Space :
+    ℚ⁺ → Relation l2 (cauchy-approximation-Pseudometric-Space M)
+  neighborhood-pseudometric-completion-Pseudometric-Space d x y =
+    type-Prop
+      ( neighborhood-prop-pseudometric-completion-Pseudometric-Space
+        ( d)
+        ( x)
+        ( y))
+```
+
+## Properties
+
+### The neighborhood relation is reflexive
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    is-reflexive-neighborhood-pseudometric-completion-Pseudometric-Space :
+      (d : ℚ⁺) (x : cauchy-approximation-Pseudometric-Space M) →
+      neighborhood-pseudometric-completion-Pseudometric-Space M d x x
+    is-reflexive-neighborhood-pseudometric-completion-Pseudometric-Space
+      d x δ ε =
+      let
+        xδ = map-cauchy-approximation-Pseudometric-Space M x δ
+        xε = map-cauchy-approximation-Pseudometric-Space M x ε
+      in
+        monotonic-neighborhood-Pseudometric-Space M xδ xε
+          ( δ +ℚ⁺ ε)
+          ( δ +ℚ⁺ ε +ℚ⁺ d)
+          ( le-right-add-rational-ℚ⁺ _ d)
+          ( is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space
+            ( M)
+            ( x)
+            ( δ)
+            ( ε))
+```
+
+### The neighborhood relation is symmetric
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+    abstract
+      is-symmetric-neighborhood-pseudometric-completion-Pseudometric-Space :
+        (d : ℚ⁺) (x y : cauchy-approximation-Pseudometric-Space M) →
+        neighborhood-pseudometric-completion-Pseudometric-Space M d x y →
+        neighborhood-pseudometric-completion-Pseudometric-Space M d y x
+      is-symmetric-neighborhood-pseudometric-completion-Pseudometric-Space
+        d x y Ndxy δ ε =
+        let
+          xε = map-cauchy-approximation-Pseudometric-Space M x ε
+          yδ = map-cauchy-approximation-Pseudometric-Space M y δ
+        in
+          tr
+            ( λ d' → neighborhood-Pseudometric-Space M d' yδ xε)
+            ( ap (_+ℚ⁺ d) (commutative-add-ℚ⁺ ε δ))
+            ( symmetric-neighborhood-Pseudometric-Space M _ xε yδ (Ndxy ε δ))
+```
+
+### The neighborhood relation is triangular
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    is-triangular-neighborhood-pseudometric-completion-Pseudometric-Space :
+      (x y z : cauchy-approximation-Pseudometric-Space M) →
+      (dxy dyz : ℚ⁺) →
+      neighborhood-pseudometric-completion-Pseudometric-Space M dyz y z →
+      neighborhood-pseudometric-completion-Pseudometric-Space M dxy x y →
+      neighborhood-pseudometric-completion-Pseudometric-Space
+        ( M)
+        ( dxy +ℚ⁺ dyz)
+        ( x)
+        ( z)
+    is-triangular-neighborhood-pseudometric-completion-Pseudometric-Space
+      x y z dxy dyz Ndyz Ndxy δ ε =
+        let
+          xδ = map-cauchy-approximation-Pseudometric-Space M x δ
+          zε = map-cauchy-approximation-Pseudometric-Space M z ε
+        in
+        saturated-neighborhood-Pseudometric-Space
+          ( M)
+          ( δ +ℚ⁺ ε +ℚ⁺ (dxy +ℚ⁺ dyz))
+          ( xδ)
+          ( zε)
+          ( λ θ →
+            let
+              (θ₂ , θ₂+θ₂<θ) = bound-double-le-ℚ⁺ θ
+              (θa , θb , θa+θb=θ₂) = split-ℚ⁺ θ₂
+              yθa = map-cauchy-approximation-Pseudometric-Space M y θa
+            in
+              monotonic-neighborhood-Pseudometric-Space
+                ( M)
+                ( xδ)
+                ( zε)
+                ( (δ +ℚ⁺ θa +ℚ⁺ dxy +ℚ⁺ θb) +ℚ⁺ (θa +ℚ⁺ ε +ℚ⁺ dyz +ℚ⁺ θb))
+                ( δ +ℚ⁺ ε +ℚ⁺ (dxy +ℚ⁺ dyz) +ℚ⁺ θ)
+                ( tr
+                  ( λ q → le-ℚ⁺ q (δ +ℚ⁺ ε +ℚ⁺ (dxy +ℚ⁺ dyz) +ℚ⁺ θ))
+                  ( equational-reasoning
+                    ((δ +ℚ⁺ ε) +ℚ⁺ (dxy +ℚ⁺ dyz)) +ℚ⁺ (θ₂ +ℚ⁺ θ₂)
+                    ＝
+                      ((δ +ℚ⁺ dxy) +ℚ⁺ (ε +ℚ⁺ dyz)) +ℚ⁺
+                      ((θa +ℚ⁺ θb) +ℚ⁺ (θa +ℚ⁺ θb))
+                      by
+                        ap-add-ℚ⁺
+                          ( interchange-law-add-add-ℚ⁺ δ ε dxy dyz)
+                          ( inv (ap-add-ℚ⁺ θa+θb=θ₂ θa+θb=θ₂))
+                    ＝
+                      ((δ +ℚ⁺ dxy) +ℚ⁺ (θa +ℚ⁺ θb)) +ℚ⁺
+                      ((ε +ℚ⁺ dyz) +ℚ⁺ (θa +ℚ⁺ θb))
+                      by interchange-law-add-add-ℚ⁺ _ _ _ _
+                    ＝
+                      ((δ +ℚ⁺ θa) +ℚ⁺ (dxy +ℚ⁺ θb)) +ℚ⁺
+                      ((ε +ℚ⁺ θa) +ℚ⁺ (dyz +ℚ⁺ θb))
+                      by
+                        ap-add-ℚ⁺
+                          ( interchange-law-add-add-ℚ⁺ _ _ _ _)
+                          ( interchange-law-add-add-ℚ⁺ _ _ _ _)
+                    ＝
+                      (δ +ℚ⁺ θa +ℚ⁺ dxy +ℚ⁺ θb) +ℚ⁺
+                      ((θa +ℚ⁺ ε) +ℚ⁺ (dyz +ℚ⁺ θb))
+                      by
+                        ap-add-ℚ⁺
+                          ( inv (associative-add-ℚ⁺ _ _ _))
+                          ( ap-add-ℚ⁺ (commutative-add-ℚ⁺ _ _) refl)
+                    ＝ (δ +ℚ⁺ θa +ℚ⁺ dxy +ℚ⁺ θb) +ℚ⁺ (θa +ℚ⁺ ε +ℚ⁺ dyz +ℚ⁺ θb)
+                      by ap-add-ℚ⁺ refl (inv (associative-add-ℚ⁺ _ _ _)))
+                  ( preserves-le-right-add-ℚ
+                    ( rational-ℚ⁺ (δ +ℚ⁺ ε +ℚ⁺ (dxy +ℚ⁺ dyz)))
+                    ( rational-ℚ⁺ (θ₂ +ℚ⁺ θ₂))
+                    ( rational-ℚ⁺ θ)
+                    ( θ₂+θ₂<θ)))
+                ( triangular-neighborhood-Pseudometric-Space M xδ yθa zε
+                  ( δ +ℚ⁺ θa +ℚ⁺ dxy +ℚ⁺ θb)
+                  ( θa +ℚ⁺ ε +ℚ⁺ dyz +ℚ⁺ θb)
+                  ( monotonic-neighborhood-Pseudometric-Space M yθa zε
+                    ( θa +ℚ⁺ ε +ℚ⁺ dyz)
+                    ( θa +ℚ⁺ ε +ℚ⁺ dyz +ℚ⁺ θb)
+                    ( le-left-add-ℚ⁺ (θa +ℚ⁺ ε +ℚ⁺ dyz) θb)
+                    ( Ndyz θa ε))
+                  ( monotonic-neighborhood-Pseudometric-Space M xδ yθa
+                    ( δ +ℚ⁺ θa +ℚ⁺ dxy)
+                    ( δ +ℚ⁺ θa +ℚ⁺ dxy +ℚ⁺ θb)
+                    ( le-left-add-ℚ⁺ (δ +ℚ⁺ θa +ℚ⁺ dxy) θb)
+                    ( Ndxy δ θa))))
+```
+
+### The neighborhood relation is saturated
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    is-saturated-neighborhood-pseudometric-completion-Pseudometric-Space :
+      ( ε : ℚ⁺) (x y : cauchy-approximation-Pseudometric-Space M) →
+      ( (δ : ℚ⁺) →
+        neighborhood-pseudometric-completion-Pseudometric-Space
+          ( M)
+          ( ε +ℚ⁺ δ)
+          ( x)
+          ( y)) →
+      neighborhood-pseudometric-completion-Pseudometric-Space M ε x y
+    is-saturated-neighborhood-pseudometric-completion-Pseudometric-Space
+      d x y H δ ε =
+        let
+          xδ = map-cauchy-approximation-Pseudometric-Space M x δ
+          yε = map-cauchy-approximation-Pseudometric-Space M y ε
+        in
+          saturated-neighborhood-Pseudometric-Space M
+            ( δ +ℚ⁺ ε +ℚ⁺ d)
+            ( xδ)
+            ( yε)
+            ( λ θ →
+              tr
+                ( λ η → neighborhood-Pseudometric-Space M η xδ yε)
+                ( inv (associative-add-ℚ⁺ _ _ _))
+                ( H θ δ ε))
+```
+
+### The pseudometric completion of a pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  pseudometric-completion-Pseudometric-Space :
+    Pseudometric-Space (l1 ⊔ l2) l2
+  pseudometric-completion-Pseudometric-Space =
+    ( cauchy-approximation-Pseudometric-Space M ,
+      neighborhood-prop-pseudometric-completion-Pseudometric-Space M ,
+      is-reflexive-neighborhood-pseudometric-completion-Pseudometric-Space M ,
+      is-symmetric-neighborhood-pseudometric-completion-Pseudometric-Space M ,
+      is-triangular-neighborhood-pseudometric-completion-Pseudometric-Space M ,
+      is-saturated-neighborhood-pseudometric-completion-Pseudometric-Space M)
+```
+
+### The isometry from a pseudometric space to its pseudometric completion
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  map-pseudometric-completion-Pseudometric-Space :
+    type-Pseudometric-Space M → cauchy-approximation-Pseudometric-Space M
+  map-pseudometric-completion-Pseudometric-Space =
+    const-cauchy-approximation-Pseudometric-Space M
+
+  abstract
+    preserves-neighborhood-map-pseudometric-completion-Pseudometric-Space :
+      (d : ℚ⁺) (x y : type-Pseudometric-Space M) →
+      neighborhood-Pseudometric-Space M d x y →
+      neighborhood-pseudometric-completion-Pseudometric-Space
+        ( M)
+        ( d)
+        ( map-pseudometric-completion-Pseudometric-Space x)
+        ( map-pseudometric-completion-Pseudometric-Space y)
+    preserves-neighborhood-map-pseudometric-completion-Pseudometric-Space
+      d x y Nxy δ ε =
+      monotonic-neighborhood-Pseudometric-Space M x y d (δ +ℚ⁺ ε +ℚ⁺ d)
+        ( le-right-add-ℚ⁺ (δ +ℚ⁺ ε) d)
+        ( Nxy)
+
+    reflects-neighborhood-map-pseudometric-completion-Pseudometric-Space :
+      (d : ℚ⁺) (x y : type-Pseudometric-Space M) →
+      neighborhood-pseudometric-completion-Pseudometric-Space
+        ( M)
+        ( d)
+        ( map-pseudometric-completion-Pseudometric-Space x)
+        ( map-pseudometric-completion-Pseudometric-Space y) →
+      neighborhood-Pseudometric-Space M d x y
+    reflects-neighborhood-map-pseudometric-completion-Pseudometric-Space
+      d x y Nxy =
+      saturated-neighborhood-Pseudometric-Space M d x y
+        ( λ δ →
+          let
+            (δ₁ , δ₂ , δ₁+δ₂=δ) = split-ℚ⁺ δ
+          in
+            tr
+              ( λ ε → neighborhood-Pseudometric-Space M ε x y)
+              ( commutative-add-ℚ⁺ _ _ ∙ ap (d +ℚ⁺_) δ₁+δ₂=δ)
+              ( Nxy δ₁ δ₂))
+
+    is-isometry-map-pseudometric-completion-Pseudometric-Space :
+      is-isometry-Pseudometric-Space
+        ( M)
+        ( pseudometric-completion-Pseudometric-Space M)
+        ( map-pseudometric-completion-Pseudometric-Space)
+    is-isometry-map-pseudometric-completion-Pseudometric-Space d x y =
+      ( ( preserves-neighborhood-map-pseudometric-completion-Pseudometric-Space
+          ( d)
+          ( x)
+          ( y)) ,
+        (reflects-neighborhood-map-pseudometric-completion-Pseudometric-Space
+          ( d)
+          ( x)
+          ( y)))
+
+  isometry-pseudometric-completion-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( M)
+      ( pseudometric-completion-Pseudometric-Space M)
+  isometry-pseudometric-completion-Pseudometric-Space =
+    ( map-pseudometric-completion-Pseudometric-Space ,
+      is-isometry-map-pseudometric-completion-Pseudometric-Space)
+```
+
+### Any Cauchy approximation in the pseudometric completion of a pseudometric space has a limit
+
+```agda
+module _
+  { l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  ( U :
+    cauchy-approximation-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space M))
+  where
+
+  map-cauchy-approximation-pseudometric-completion-Pseudometric-Space :
+    ℚ⁺ → ℚ⁺ → type-Pseudometric-Space M
+  map-cauchy-approximation-pseudometric-completion-Pseudometric-Space ε =
+    map-cauchy-approximation-Pseudometric-Space M
+      ( map-cauchy-approximation-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space M)
+        ( U)
+        ( ε))
+
+  is-cauchy-map-cauchy-approximation-pseudometric-completion-Pseudometric-Space :
+    (δ ε d₁ d₂ : ℚ⁺) →
+    neighborhood-Pseudometric-Space
+      ( M)
+      ( d₁ +ℚ⁺ d₂ +ℚ⁺ (δ +ℚ⁺ ε))
+      ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+        ( δ)
+        ( d₁))
+      ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+        ( ε)
+        ( d₂))
+  is-cauchy-map-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+    =
+    is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space M)
+      ( U)
+
+  map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space :
+    ℚ⁺ → type-Pseudometric-Space M
+  map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space d =
+    let
+      (d₁ , d₂ , _) = split-ℚ⁺ d
+    in
+      map-cauchy-approximation-pseudometric-completion-Pseudometric-Space d₂ d₁
+
+  is-cauchy-map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space :
+    is-cauchy-approximation-Pseudometric-Space
+      ( M)
+      ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space)
+  is-cauchy-map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+    δ ε =
+    let
+      (δ₁ , δ₂ , δ₁+δ₂=δ) = split-ℚ⁺ δ
+      (ε₁ , ε₂ , ε₁+ε₂=ε) = split-ℚ⁺ ε
+
+      lemma-δ+ε :
+        (δ₁ +ℚ⁺ ε₁ +ℚ⁺ (δ₂ +ℚ⁺ ε₂)) ＝ δ +ℚ⁺ ε
+      lemma-δ+ε =
+        ( interchange-law-add-add-ℚ⁺
+          ( δ₁)
+          ( ε₁)
+          ( δ₂)
+          ( ε₂)) ∙
+        ( ap-binary
+          ( add-ℚ⁺)
+          ( δ₁+δ₂=δ)
+          ( ε₁+ε₂=ε))
+    in
+      tr
+        ( is-upper-bound-dist-Pseudometric-Space
+          ( M)
+          ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( δ))
+          ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( ε)))
+        ( lemma-δ+ε)
+        ( is-cauchy-map-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+          _ _ _ _)
+
+  lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space :
+    cauchy-approximation-Pseudometric-Space M
+  lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space =
+    ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space ,
+      is-cauchy-map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space)
+
+  is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space :
+    is-limit-cauchy-approximation-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space M)
+      ( U)
+      ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space)
+  is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+    δ ε η θ =
+    let
+      (θ₁ , θ₂ , θ₁+θ₂=θ) = split-ℚ⁺ θ
+
+      lemma-η+θ+δ :
+        ( η +ℚ⁺ θ₁ +ℚ⁺ (δ +ℚ⁺ θ₂)) ＝ η +ℚ⁺ θ +ℚ⁺ δ
+      lemma-η+θ+δ =
+        ( interchange-law-add-add-ℚ⁺ η θ₁ δ θ₂) ∙
+        ( ap
+          ( add-ℚ⁺ (η +ℚ⁺ δ))
+          ( θ₁+θ₂=θ)) ∙
+        ( associative-add-ℚ⁺ η δ θ) ∙
+        ( ap
+          ( add-ℚ⁺ η)
+          ( commutative-add-ℚ⁺ δ θ)) ∙
+        ( inv (associative-add-ℚ⁺ η θ δ))
+
+      lemma-lim :
+        neighborhood-Pseudometric-Space M
+          ( η +ℚ⁺ θ +ℚ⁺ δ)
+          ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( δ)
+            ( η))
+          ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( θ₂)
+            ( θ₁))
+      lemma-lim =
+        tr
+          ( is-upper-bound-dist-Pseudometric-Space M
+            ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+              ( δ)
+              ( η))
+            ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+              ( θ)))
+          ( lemma-η+θ+δ)
+          ( is-cauchy-map-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            _ _ _ _)
+    in
+      tr
+        ( is-upper-bound-dist-Pseudometric-Space M
+          ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( δ)
+            ( η))
+          ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( θ)))
+        ( associative-add-ℚ⁺
+          ( η +ℚ⁺ θ)
+          ( δ)
+          ( ε))
+        ( monotonic-neighborhood-Pseudometric-Space M
+          ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( δ)
+            ( η))
+          ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( θ))
+          ( η +ℚ⁺ θ +ℚ⁺ δ)
+          ( η +ℚ⁺ θ +ℚ⁺ δ +ℚ⁺ ε)
+          ( le-left-add-ℚ⁺ ( η +ℚ⁺ θ +ℚ⁺ δ) ε)
+          ( lemma-lim))
+
+  has-limit-cauchy-approximation-pseudometric-completion-Pseudometric-Space :
+    Σ ( cauchy-approximation-Pseudometric-Space M)
+      ( is-limit-cauchy-approximation-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space M)
+        ( U))
+  has-limit-cauchy-approximation-pseudometric-completion-Pseudometric-Space =
+    ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space ,
+      is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space)
+```
+
+### Short maps into complete metric spaces factor through pseudometric completions
+
+```agda
+module _
+  { l1 l2 l1' l2' : Level}
+  ( A : Pseudometric-Space l1 l2)
+  ( C : Complete-Metric-Space l1' l2')
+  ( f :
+    short-function-Pseudometric-Space A (pseudometric-Complete-Metric-Space C))
+  where
+
+  map-short-function-complete-pseudometric-completion-Pseudometric-Space :
+    type-function-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space A)
+      ( pseudometric-Complete-Metric-Space C)
+  map-short-function-complete-pseudometric-completion-Pseudometric-Space =
+    ( limit-cauchy-approximation-Complete-Metric-Space C) ∘
+    ( map-short-function-cauchy-approximation-Pseudometric-Space
+      ( A)
+      ( pseudometric-Complete-Metric-Space C)
+      ( f))
+
+  htpy-comp-map-short-function-complete-pseudometric-completion-Pseudometric-Space :
+    ( map-short-function-complete-pseudometric-completion-Pseudometric-Space ∘
+      map-pseudometric-completion-Pseudometric-Space A) ~
+    ( map-short-function-Pseudometric-Space
+      ( A)
+      ( pseudometric-Complete-Metric-Space C)
+      ( f))
+  htpy-comp-map-short-function-complete-pseudometric-completion-Pseudometric-Space
+    x =
+    all-eq-is-limit-cauchy-approximation-Metric-Space
+      ( metric-Complete-Metric-Space C)
+      ( map-short-function-cauchy-approximation-Pseudometric-Space
+        ( A)
+        ( pseudometric-Complete-Metric-Space C)
+        ( f)
+        ( const-cauchy-approximation-Pseudometric-Space A x))
+      ( map-short-function-complete-pseudometric-completion-Pseudometric-Space
+        ( map-pseudometric-completion-Pseudometric-Space A x))
+      ( map-short-function-Pseudometric-Space
+        ( A)
+        ( pseudometric-Complete-Metric-Space C)
+        ( f)
+        ( x))
+      ( is-limit-limit-cauchy-approximation-Complete-Metric-Space
+        ( C)
+        ( map-short-function-cauchy-approximation-Pseudometric-Space
+          ( A)
+          ( pseudometric-Complete-Metric-Space C)
+          ( f)
+          ( const-cauchy-approximation-Pseudometric-Space A x)))
+      ( is-limit-const-cauchy-approximation-Metric-Space
+        ( metric-Complete-Metric-Space C)
+        ( map-short-function-Pseudometric-Space
+          ( A)
+          ( pseudometric-Complete-Metric-Space C)
+          ( f)
+          ( x)))
+
+  -- is-short-map-short-function-complete-pseudometric-completion-Pseudometric-Space :
+  --   is-short-function-Pseudometric-Space
+  --     ( pseudometric-completion-Pseudometric-Space A)
+  --     ( pseudometric-Complete-Metric-Space C)
+  --     ( map-short-function-complete-pseudometric-completion-Pseudometric-Space)
+  -- is-short-map-short-function-complete-pseudometric-completion-Pseudometric-Space
+  --   d x y Nxy =
+  --   {!!}
+```