diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md
index c501d3c56d..5ea0eb4f03 100644
--- a/src/metric-spaces.lagda.md
+++ b/src/metric-spaces.lagda.md
@@ -62,6 +62,7 @@ open import metric-spaces.bounded-distance-decompositions-of-metric-spaces publi
 open import metric-spaces.cartesian-products-metric-spaces public
 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-quotients-of-pseudometric-spaces public
 open import metric-spaces.cauchy-approximations-metric-spaces public
 open import metric-spaces.cauchy-approximations-pseudometric-spaces public
 open import metric-spaces.cauchy-sequences-complete-metric-spaces public
@@ -101,6 +102,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
@@ -125,6 +129,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
diff --git a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..9414e516f8
--- /dev/null
+++ b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md
@@ -0,0 +1,312 @@
+# Cauchy approximations in metric quotients of pseudometric spaces
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module metric-spaces.cauchy-approximations-metric-quotients-of-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-relations
+open import foundation.binary-transport
+open import foundation.contractible-maps
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equivalence-classes
+open import foundation.equivalences
+open import foundation.existential-quantification
+open import foundation.fibers-of-maps
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.inhabited-subtypes
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.reflecting-maps-equivalence-relations
+open import foundation.retractions
+open import foundation.sections
+open import foundation.set-quotients
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universal-property-set-quotients
+open import foundation.universe-levels
+
+open import logic.functoriality-existential-quantification
+
+open import metric-spaces.cauchy-approximations-metric-spaces
+open import metric-spaces.cauchy-approximations-pseudometric-spaces
+open import metric-spaces.convergent-cauchy-approximations-metric-spaces
+open import metric-spaces.equality-of-metric-spaces
+open import metric-spaces.extensionality-pseudometric-spaces
+open import metric-spaces.functions-metric-spaces
+open import metric-spaces.isometries-metric-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-quotients-of-pseudometric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.pseudometric-completion-of-metric-spaces
+open import metric-spaces.pseudometric-completion-of-pseudometric-spaces
+open import metric-spaces.pseudometric-spaces
+open import metric-spaces.rational-neighborhood-relations
+open import metric-spaces.short-functions-metric-spaces
+open import metric-spaces.short-functions-pseudometric-spaces
+open import metric-spaces.similarity-of-elements-pseudometric-spaces
+```
+
+</details>
+
+## Idea
+
+The pointwise [quotients](foundation.set-quotients.md) of
+[Cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md)
+by the
+[similarity relation](metric-spaces.similarity-of-elements-pseudometric-spaces.md)
+in a [pseudometric space](metric-spaces.pseudometric-spaces.md) are Cauchy
+approximations in the
+[metric quotient](metric-spaces.metric-quotients-of-pseudometric-spaces.md). A
+Cauchy approximation in a the metric quotient of a pseudometric space has a
+{{#concept "lift up to similarity" Agda=has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space}}
+if it is similar (in the
+[pseudometric completion](metric-spaces.pseudometric-completion-of-metric-spaces.md)
+of the metric quotient) to the pointwise quotient of
+[some](foundation.existential-quantification.md) Cauchy approximation in the
+pseudometric space.
+
+The pointwise quotient of Cauchy approximations preserves
+[limits](metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces.md).
+The pointwise quotient of a Cauchy approximation has a lift. A Cauchy
+approximation that admits a
+[limit](metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces.md)
+has a lift.
+
+## Definitions
+
+### The pointwise quotient Cauchy approximation of a Cauchy approximation in a pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  map-metric-quotient-cauchy-approximation-Pseudometric-Space :
+    cauchy-approximation-Pseudometric-Space M →
+    cauchy-approximation-Metric-Space
+      ( metric-quotient-Pseudometric-Space M)
+  map-metric-quotient-cauchy-approximation-Pseudometric-Space =
+    map-short-function-cauchy-approximation-Pseudometric-Space
+      ( M)
+      ( pseudometric-metric-quotient-Pseudometric-Space M)
+      ( short-map-metric-quotient-Pseudometric-Space M)
+```
+
+### Lifts of Cauchy approximations in the quotient metric space up to similarity
+
+```agda
+module _
+  { l1 l2 : Level} (A : Pseudometric-Space l1 l2)
+  ( u :
+    cauchy-approximation-Metric-Space
+      ( metric-quotient-Pseudometric-Space A))
+  ( v : cauchy-approximation-Pseudometric-Space A)
+  where
+
+  is-lift-quotient-prop-cauchy-approximation-Pseudometric-Space :
+    Prop (l1 ⊔ l2)
+  is-lift-quotient-prop-cauchy-approximation-Pseudometric-Space =
+    sim-prop-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space
+        ( pseudometric-metric-quotient-Pseudometric-Space A))
+      ( u)
+      ( map-metric-quotient-cauchy-approximation-Pseudometric-Space A v)
+
+  is-lift-quotient-cauchy-approximation-Pseudometric-Space : UU (l1 ⊔ l2)
+  is-lift-quotient-cauchy-approximation-Pseudometric-Space =
+    type-Prop is-lift-quotient-prop-cauchy-approximation-Pseudometric-Space
+
+  is-prop-is-lift-quotient-cauchy-approximation-Pseudometric-Space :
+    is-prop is-lift-quotient-cauchy-approximation-Pseudometric-Space
+  is-prop-is-lift-quotient-cauchy-approximation-Pseudometric-Space =
+    is-prop-type-Prop
+      is-lift-quotient-prop-cauchy-approximation-Pseudometric-Space
+
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
+  ( u :
+    cauchy-approximation-Metric-Space
+      ( metric-quotient-Pseudometric-Space A))
+  where
+
+  has-lift-prop-cauchy-approximation-metric-quotient-Pseudometric-Space :
+    Prop (l1 ⊔ l2)
+  has-lift-prop-cauchy-approximation-metric-quotient-Pseudometric-Space =
+    ∃ ( cauchy-approximation-Pseudometric-Space A)
+      ( is-lift-quotient-prop-cauchy-approximation-Pseudometric-Space A u)
+
+  has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space :
+    UU (l1 ⊔ l2)
+  has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space =
+    type-Prop
+      has-lift-prop-cauchy-approximation-metric-quotient-Pseudometric-Space
+
+  is-prop-has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space :
+    is-prop has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space
+  is-prop-has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space =
+    is-prop-type-Prop
+      has-lift-prop-cauchy-approximation-metric-quotient-Pseudometric-Space
+```
+
+## Properties
+
+### The pointwise quotient of Cauchy approximations in the quotient metric space preserves limits
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  (u : cauchy-approximation-Pseudometric-Space M)
+  (lim : type-Pseudometric-Space M)
+  (is-lim :
+    is-limit-cauchy-approximation-Pseudometric-Space M u lim)
+  where
+
+  preserves-limit-map-metric-quotient-cauchy-approximation-Pseudometric-Space :
+    is-limit-cauchy-approximation-Metric-Space
+      ( metric-quotient-Pseudometric-Space M)
+      ( map-metric-quotient-cauchy-approximation-Pseudometric-Space M u)
+      ( map-metric-quotient-Pseudometric-Space M lim)
+  preserves-limit-map-metric-quotient-cauchy-approximation-Pseudometric-Space
+    ε δ (x , x∈uε) (y , y∈lim) =
+    let
+      lim~y : sim-Pseudometric-Space M lim y
+      lim~y =
+        sim-is-in-equivalence-class-quotient-map-set-quotient
+          ( equivalence-relation-sim-Pseudometric-Space M)
+          ( lim)
+          ( y)
+          ( y∈lim)
+
+      uε~x :
+        sim-Pseudometric-Space M
+          ( map-cauchy-approximation-Pseudometric-Space M u ε)
+          ( x)
+      uε~x =
+        sim-is-in-equivalence-class-quotient-map-set-quotient
+          ( equivalence-relation-sim-Pseudometric-Space M)
+          ( map-cauchy-approximation-Pseudometric-Space M u ε)
+          ( x)
+          ( x∈uε)
+    in
+      preserves-neighborhood-sim-Pseudometric-Space
+        ( M)
+        ( uε~x)
+        ( lim~y)
+        ( ε +ℚ⁺ δ)
+        ( is-lim ε δ)
+```
+
+### Pointwise quotients of Cauchy approximations have lifts
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
+  (u : cauchy-approximation-Pseudometric-Space A)
+  where
+
+  has-lift-map-quotient-cauchy-approximation-metric-quotient-Pseudometric-Space :
+    has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space
+      ( A)
+      ( map-metric-quotient-cauchy-approximation-Pseudometric-Space A u)
+  has-lift-map-quotient-cauchy-approximation-metric-quotient-Pseudometric-Space =
+    unit-trunc-Prop
+      ( u ,
+        refl-sim-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space
+            ( pseudometric-metric-quotient-Pseudometric-Space A))
+          ( map-metric-quotient-cauchy-approximation-Pseudometric-Space A u))
+```
+
+### Convergent Cauchy approximations in the quotient metric space have a lift up to similarity
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
+  ( u :
+    cauchy-approximation-Metric-Space
+      ( metric-quotient-Pseudometric-Space A))
+  ( lim : type-Metric-Space (metric-quotient-Pseudometric-Space A))
+  ( is-lim :
+    is-limit-cauchy-approximation-Metric-Space
+      ( metric-quotient-Pseudometric-Space A)
+      ( u)
+      ( lim))
+  where
+
+  lemma-sim-lift-is-limit-cauchy-approximation-metric-quotient-Pseudometric-Space :
+    (x : type-Pseudometric-Space A) →
+    (is-in-class-metric-quotient-Pseudometric-Space A lim x) →
+    is-lift-quotient-cauchy-approximation-Pseudometric-Space
+      ( A)
+      ( u)
+      ( const-cauchy-approximation-Pseudometric-Space A x)
+  lemma-sim-lift-is-limit-cauchy-approximation-metric-quotient-Pseudometric-Space
+    x x∈lim =
+    transitive-sim-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space
+        ( pseudometric-metric-quotient-Pseudometric-Space A))
+      ( u)
+      ( const-cauchy-approximation-Pseudometric-Space
+        ( pseudometric-metric-quotient-Pseudometric-Space A)
+        ( lim))
+      ( const-cauchy-approximation-Pseudometric-Space
+        ( pseudometric-metric-quotient-Pseudometric-Space A)
+        ( map-metric-quotient-Pseudometric-Space A x))
+      ( λ d α β →
+        sim-eq-Pseudometric-Space
+          ( pseudometric-metric-quotient-Pseudometric-Space A)
+          ( lim)
+          ( map-metric-quotient-Pseudometric-Space A x)
+          ( inv
+            ( eq-set-quotient-equivalence-class-set-quotient
+              ( equivalence-relation-sim-Pseudometric-Space A)
+              ( lim)
+              ( x∈lim)))
+          ( α +ℚ⁺ β +ℚ⁺ d))
+      ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+        ( pseudometric-metric-quotient-Pseudometric-Space A)
+        ( u)
+        ( lim)
+        ( is-lim))
+
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
+  ( u :
+    cauchy-approximation-Metric-Space
+      ( metric-quotient-Pseudometric-Space A))
+  where
+
+  has-lift-is-convergent-cauchy-approximation-metric-quotient-Pseudometric-Space :
+    is-convergent-cauchy-approximation-Metric-Space
+      ( metric-quotient-Pseudometric-Space A)
+      ( u) →
+    has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space A u
+  has-lift-is-convergent-cauchy-approximation-metric-quotient-Pseudometric-Space
+    (lim , is-lim) =
+    map-exists
+      ( is-lift-quotient-cauchy-approximation-Pseudometric-Space A u)
+      ( const-cauchy-approximation-Pseudometric-Space A)
+      ( lemma-sim-lift-is-limit-cauchy-approximation-metric-quotient-Pseudometric-Space
+        ( A)
+        ( u)
+        ( lim)
+        ( is-lim))
+      ( is-inhabited-class-metric-quotient-Pseudometric-Space A lim)
+```
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..3d822f77fc 100644
--- a/src/metric-spaces/cauchy-sequences-complete-metric-spaces.lagda.md
+++ b/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)
 ```
diff --git a/src/metric-spaces/complete-metric-spaces.lagda.md b/src/metric-spaces/complete-metric-spaces.lagda.md
index 6b10db7b42..8f894926c8 100644
--- a/src/metric-spaces/complete-metric-spaces.lagda.md
+++ b/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
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 53b0dbe5b7..5641ecc9fb 100644
--- a/src/metric-spaces/convergent-cauchy-approximations-metric-spaces.lagda.md
+++ b/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)
+```
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 e1ecfba92e..4ba16ab30a 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
@@ -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)
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 3e6705b776..6226f7b2c9 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
@@ -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
diff --git a/src/metric-spaces/metric-pseudocompletion-of-metric-spaces.lagda.md b/src/metric-spaces/metric-pseudocompletion-of-metric-spaces.lagda.md
new file mode 100644
index 0000000000..a2bc054b60
--- /dev/null
+++ b/src/metric-spaces/metric-pseudocompletion-of-metric-spaces.lagda.md
@@ -0,0 +1,380 @@
+# The metric pseudocompletion of a metric space
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module metric-spaces.metric-pseudocompletion-of-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.isomorphisms-in-precategories
+
+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.equivalences
+open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.set-quotients
+open import foundation.sets
+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.equality-of-metric-spaces
+open import metric-spaces.functions-metric-spaces
+open import metric-spaces.functions-pseudometric-spaces
+open import metric-spaces.isometries-metric-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-pseudocompletion-of-pseudometric-spaces
+open import metric-spaces.metric-quotients-of-pseudometric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.precategory-of-metric-spaces-and-short-functions
+open import metric-spaces.pseudometric-completion-of-metric-spaces
+open import metric-spaces.pseudometric-completion-of-pseudometric-spaces
+open import metric-spaces.pseudometric-spaces
+open import metric-spaces.rational-neighborhood-relations
+open import metric-spaces.short-functions-metric-spaces
+open import metric-spaces.short-functions-pseudometric-spaces
+open import metric-spaces.similarity-of-elements-pseudometric-spaces
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "metric pseudocompletion" Disambiguation="of a metric space Agda=metric-pseudocompletion-Metric-Space}}
+of a [metric space](metric-spaces.metric-spaces.md) `M` is the
+[metric pseudocompletion](metric-spaces.metric-pseudocompletion-of-pseudometric-spaces.md)
+of its underlying [pseudometric space](metric-spaces.pseudometric-spaces.md);
+i.e. the
+[metric quotient](metric-spaces.metric-quotients-of-pseudometric-spaces.md)
+`[C M]` of its
+[pseudometric completion](metric-spaces.pseudometric-completion-of-metric-spaces.md)
+`C M`.
+
+The natural [isometry](metric-spaces.isometries-metric-spaces.md)
+
+```text
+M → [C M]
+```
+
+is an [equivalence](foundation.equivalences.md) if and only if `M` is
+[complete](metric-spaces.complete-metric-spaces.md).
+
+## Definitions
+
+### The metric pseudocompletion of a metric space
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+  metric-pseudocompletion-Metric-Space :
+    Metric-Space (l1 ⊔ l2) (l1 ⊔ l2)
+  metric-pseudocompletion-Metric-Space =
+    metric-pseudocompletion-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+
+  pseudometric-metric-pseudocompletion-Metric-Space :
+    Pseudometric-Space (l1 ⊔ l2) (l1 ⊔ l2)
+  pseudometric-metric-pseudocompletion-Metric-Space =
+    pseudometric-Metric-Space
+      metric-pseudocompletion-Metric-Space
+
+  type-metric-pseudocompletion-Metric-Space : UU (l1 ⊔ l2)
+  type-metric-pseudocompletion-Metric-Space =
+    type-Metric-Space metric-pseudocompletion-Metric-Space
+```
+
+### The isometry from the pseudometric completion of a metric space into its metric pseudocompletion
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+  isometry-metric-pseudocompletion-pseudometric-completion-Metric-Space :
+    isometry-Pseudometric-Space
+      ( pseudometric-completion-Metric-Space M)
+      ( pseudometric-metric-pseudocompletion-Metric-Space M)
+  isometry-metric-pseudocompletion-pseudometric-completion-Metric-Space =
+    isometry-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+
+  map-metric-pseudocompletion-pseudometric-completion-Metric-Space :
+    type-function-Pseudometric-Space
+      ( pseudometric-completion-Metric-Space M)
+      ( pseudometric-metric-pseudocompletion-Metric-Space M)
+  map-metric-pseudocompletion-pseudometric-completion-Metric-Space =
+    map-isometry-Pseudometric-Space
+      ( pseudometric-completion-Metric-Space M)
+      ( pseudometric-metric-pseudocompletion-Metric-Space M)
+      ( isometry-metric-pseudocompletion-pseudometric-completion-Metric-Space)
+```
+
+### The isometry from a metric space into its metric pseudocompletion
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+  isometry-metric-pseudocompletion-Metric-Space :
+    isometry-Metric-Space
+      ( M)
+      ( metric-pseudocompletion-Metric-Space M)
+  isometry-metric-pseudocompletion-Metric-Space =
+    isometry-metric-pseudocompletion-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+
+  map-metric-pseudocompletion-Metric-Space :
+    type-function-Metric-Space
+      ( M)
+      ( metric-pseudocompletion-Metric-Space M)
+  map-metric-pseudocompletion-Metric-Space =
+    map-isometry-Metric-Space
+      ( M)
+      ( metric-pseudocompletion-Metric-Space M)
+      ( isometry-metric-pseudocompletion-Metric-Space)
+
+  is-isometry-map-metric-pseudocompletion-Metric-Space :
+    is-isometry-Metric-Space
+      ( M)
+      ( metric-pseudocompletion-Metric-Space M)
+      ( map-metric-pseudocompletion-Metric-Space)
+  is-isometry-map-metric-pseudocompletion-Metric-Space =
+    is-isometry-map-isometry-Metric-Space
+      ( M)
+      ( metric-pseudocompletion-Metric-Space M)
+      ( isometry-metric-pseudocompletion-Metric-Space)
+```
+
+## Properties
+
+### The mapping from a complete metric space into its metric pseudocompletion is an isometric equivalence
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  (is-complete-M : is-complete-Metric-Space M)
+  where
+
+  short-map-lim-metric-pseudocompletion-is-complete-Metric-Space :
+    short-function-Metric-Space
+      ( metric-pseudocompletion-Metric-Space M)
+      ( M)
+  short-map-lim-metric-pseudocompletion-is-complete-Metric-Space =
+    short-map-short-function-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Metric-Space M)
+      ( M)
+      ( short-map-lim-pseudometric-completion-is-complete-Metric-Space
+        ( M)
+        ( is-complete-M))
+
+  map-lim-metric-pseudocompletion-is-complete-Metric-Space :
+    type-function-Metric-Space
+      ( metric-pseudocompletion-Metric-Space M)
+      ( M)
+  map-lim-metric-pseudocompletion-is-complete-Metric-Space =
+    map-short-function-Metric-Space
+      ( metric-pseudocompletion-Metric-Space M)
+      ( M)
+      ( short-map-lim-metric-pseudocompletion-is-complete-Metric-Space)
+
+  is-short-map-lim-metric-pseudocompletion-is-completr-Metric-Space :
+    is-short-function-Metric-Space
+      ( metric-pseudocompletion-Metric-Space M)
+      ( M)
+      ( map-lim-metric-pseudocompletion-is-complete-Metric-Space)
+  is-short-map-lim-metric-pseudocompletion-is-completr-Metric-Space =
+    is-short-map-short-function-Metric-Space
+      ( metric-pseudocompletion-Metric-Space M)
+      ( M)
+      ( short-map-lim-metric-pseudocompletion-is-complete-Metric-Space)
+
+  compute-map-lim-metric-pseudocompletion-is-complete-Metric-Space :
+    (X : type-metric-pseudocompletion-Metric-Space M) →
+    (x : cauchy-approximation-Metric-Space M) →
+    is-in-class-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Metric-Space M)
+      ( X)
+      ( x) →
+    map-lim-metric-pseudocompletion-is-complete-Metric-Space X ＝
+    limit-cauchy-approximation-Complete-Metric-Space
+      ( M , is-complete-M)
+      ( x)
+  compute-map-lim-metric-pseudocompletion-is-complete-Metric-Space =
+    compute-map-short-function-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Metric-Space M)
+      ( M)
+      ( short-map-lim-pseudometric-completion-is-complete-Metric-Space
+        ( M)
+        (is-complete-M))
+
+  is-section-map-metric-pseudocompletion-is-complete-Metric-Space :
+    ( map-metric-pseudocompletion-Metric-Space M ∘
+      map-lim-metric-pseudocompletion-is-complete-Metric-Space) ~
+    ( id)
+  is-section-map-metric-pseudocompletion-is-complete-Metric-Space U =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( Id-Prop
+              ( set-Metric-Space
+                ( metric-pseudocompletion-Metric-Space M))
+            ( map-metric-pseudocompletion-Metric-Space M
+              ( map-lim-metric-pseudocompletion-is-complete-Metric-Space U))
+            ( U))
+        in do
+          (u , u∈U) ←
+            is-inhabited-class-metric-quotient-Pseudometric-Space
+              ( pseudometric-completion-Metric-Space M)
+              ( U)
+          let
+            lim-u : type-Metric-Space M
+            lim-u =
+              limit-cauchy-approximation-Complete-Metric-Space
+                ( M , is-complete-M)
+                ( u)
+
+            compute-map-lim-U :
+              map-lim-metric-pseudocompletion-is-complete-Metric-Space U ＝ lim-u
+            compute-map-lim-U =
+              compute-map-lim-metric-pseudocompletion-is-complete-Metric-Space
+                ( U)
+                ( u)
+                ( u∈U)
+
+            sim-u-lim-u :
+              sim-Pseudometric-Space
+                ( pseudometric-completion-Metric-Space M)
+                ( u)
+                ( const-cauchy-approximation-Metric-Space
+                  ( M)
+                  ( lim-u))
+            sim-u-lim-u =
+              sim-const-is-limit-cauchy-approximation-Metric-Space
+                ( M)
+                ( u)
+                ( lim-u)
+                ( is-limit-map-lim-pseudometric-completion-is-complete-Metric-Space
+                  ( M)
+                  ( is-complete-M)
+                  ( u))
+
+            [u]=[lim-u] :
+              ( map-metric-quotient-Pseudometric-Space
+                ( pseudometric-completion-Metric-Space M)
+                ( u)) ＝
+              ( map-metric-pseudocompletion-Metric-Space M lim-u)
+            [u]=[lim-u] =
+              apply-effectiveness-quotient-map'
+                ( equivalence-relation-sim-Pseudometric-Space
+                  ( pseudometric-completion-Metric-Space M))
+                ( sim-u-lim-u)
+          ( ( ap
+              ( map-metric-pseudocompletion-Metric-Space M)
+              ( compute-map-lim-U)) ∙
+            ( inv [u]=[lim-u]) ∙
+            ( eq-set-quotient-equivalence-class-set-quotient
+              ( equivalence-relation-sim-Pseudometric-Space
+              ( pseudometric-completion-Metric-Space M))
+              ( U)
+              ( u∈U)))
+
+  is-retraction-map-metric-pseudocompletion-is-complete-Metric-Space :
+    ( map-lim-metric-pseudocompletion-is-complete-Metric-Space ∘
+      map-metric-pseudocompletion-Metric-Space M) ~
+    ( id)
+  is-retraction-map-metric-pseudocompletion-is-complete-Metric-Space x =
+    ( compute-map-lim-metric-pseudocompletion-is-complete-Metric-Space
+      ( map-metric-pseudocompletion-Metric-Space M x)
+      ( const-cauchy-approximation-Metric-Space M x)
+      ( is-in-class-map-quotient-Pseudometric-Space
+        ( pseudometric-completion-Metric-Space M)
+        ( const-cauchy-approximation-Metric-Space M x))) ∙
+    ( is-retraction-limit-cauchy-approximation-Complete-Metric-Space
+      ( M , is-complete-M)
+      ( x))
+
+  is-equiv-map-metric-pseudocompletion-is-complete-Metric-Space :
+    is-equiv
+      ( map-metric-pseudocompletion-Metric-Space M)
+  is-equiv-map-metric-pseudocompletion-is-complete-Metric-Space =
+    is-equiv-is-invertible
+      ( map-lim-metric-pseudocompletion-is-complete-Metric-Space)
+      ( is-section-map-metric-pseudocompletion-is-complete-Metric-Space)
+      ( is-retraction-map-metric-pseudocompletion-is-complete-Metric-Space)
+
+  isometric-equiv-metric-pseudocompletion-is-complete-Metric-Space' :
+    isometric-equiv-Metric-Space'
+      ( M)
+      ( metric-pseudocompletion-Metric-Space M)
+  isometric-equiv-metric-pseudocompletion-is-complete-Metric-Space' =
+    ( map-metric-pseudocompletion-Metric-Space M ,
+      is-equiv-map-metric-pseudocompletion-is-complete-Metric-Space ,
+      is-isometry-map-metric-pseudocompletion-Metric-Space M)
+```
+
+### If the mapping from a metric space into its metric pseudocompletion is an equivalence, the metric space is complete
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+  is-complete-is-equiv-map-metric-pseudocompletion-Metric-Space :
+    is-equiv (map-metric-pseudocompletion-Metric-Space M) →
+    is-complete-Metric-Space M
+  is-complete-is-equiv-map-metric-pseudocompletion-Metric-Space H u =
+    (lim-u , is-limit-lim-u)
+    where
+
+    lim-u : type-Metric-Space M
+    lim-u =
+      map-inv-is-equiv
+        ( H)
+        ( map-metric-pseudocompletion-pseudometric-completion-Metric-Space
+          ( M)
+          ( u))
+
+    is-limit-lim-u :
+      is-limit-cauchy-approximation-Metric-Space
+        ( M)
+        ( u)
+        ( lim-u)
+    is-limit-lim-u =
+      is-limit-sim-const-cauchy-approximation-Metric-Space
+        ( M)
+        ( u)
+        ( lim-u)
+        ( apply-effectiveness-quotient-map
+          ( equivalence-relation-sim-Pseudometric-Space
+            ( pseudometric-completion-Metric-Space M))
+          ( inv
+            ( is-section-map-section-is-equiv
+              ( H)
+              ( map-metric-pseudocompletion-pseudometric-completion-Metric-Space
+                ( M)
+                ( u)))))
+```
diff --git a/src/metric-spaces/metric-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-pseudocompletion-of-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..b57d473117
--- /dev/null
+++ b/src/metric-spaces/metric-pseudocompletion-of-pseudometric-spaces.lagda.md
@@ -0,0 +1,801 @@
+# The metric pseudocompletion of a pseudometric space
+
+```agda
+module metric-spaces.metric-pseudocompletion-of-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.isomorphisms-in-precategories
+
+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.equivalences
+open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.set-quotients
+open import foundation.sets
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import metric-spaces.cauchy-approximations-metric-quotients-of-pseudometric-spaces
+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.equality-of-metric-spaces
+open import metric-spaces.functions-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-quotients-of-pseudometric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.precategory-of-metric-spaces-and-short-functions
+open import metric-spaces.pseudometric-completion-of-pseudometric-spaces
+open import metric-spaces.pseudometric-spaces
+open import metric-spaces.rational-neighborhood-relations
+open import metric-spaces.short-functions-metric-spaces
+open import metric-spaces.short-functions-pseudometric-spaces
+open import metric-spaces.similarity-of-elements-pseudometric-spaces
+```
+
+</details>
+
+## Idea
+
+Let `M` be a [pseudometric space](metric-spaces.pseudometric-spaces.md) and
+`C M` denote its
+[pseudometric completion](metric-spaces.pseudometric-completion-of-pseudometric-spaces.md);
+the
+{{#concept "metric pseudocompletion" Disambiguation="of a pseudometric space" Agda=metric-pseudocompletion-Pseudometric-Space}}
+of `M` is the
+[metric quotient](metric-spaces.metric-quotients-of-pseudometric-spaces.md)
+
+```text
+[C M] = C M / ~
+```
+
+There are [isometries](metric-spaces.isometries-pseudometric-spaces.md)
+
+```text
+M → C M → [C M]
+```
+
+The metric pseudocompletion of the pseudometric completion of a pseudometric
+space is the metric pseudocompletion of the pseudometric space:
+
+```text
+[C (C M)] ＝ [C M]
+```
+
+A [Cauchy approximation](metric-spaces.cauchy-approximations-metric-spaces.md)
+in `[C M]`, `f : C [C M]` is
+[convergent](metric-spaces.convergent-cauchy-approximations-metric-spaces.md) if
+and only if it is
+[similar](metric-spaces.similarity-of-elements-pseudometric-spaces.md) in
+`C [C M]` to the
+[pointwise quotient](metric-spaces.cauchy-approximations-metric-quotients-of-pseudometric-spaces.md)
+of some
+[Cauchy approximation](metric-spaces.cauchy-approximations-pseudometric-spaces.md)
+`g : C (C M)`.
+
+## Definition
+
+### The metric pseudocompletion of a pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  metric-pseudocompletion-Pseudometric-Space :
+    Metric-Space (l1 ⊔ l2) (l1 ⊔ l2)
+  metric-pseudocompletion-Pseudometric-Space =
+    metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space P)
+
+  pseudometric-metric-pseudocompletion-Pseudometric-Space :
+    Pseudometric-Space (l1 ⊔ l2) (l1 ⊔ l2)
+  pseudometric-metric-pseudocompletion-Pseudometric-Space =
+    pseudometric-Metric-Space
+      metric-pseudocompletion-Pseudometric-Space
+
+  type-metric-pseudocompletion-Pseudometric-Space : UU (l1 ⊔ l2)
+  type-metric-pseudocompletion-Pseudometric-Space =
+    type-Metric-Space metric-pseudocompletion-Pseudometric-Space
+```
+
+### The metric pseudocompletion of the pseudometric completion of a pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  metric-pseudocompletion-pseudometric-completion-Pseudometric-Space :
+    Metric-Space (l1 ⊔ l2) (l1 ⊔ l2)
+  metric-pseudocompletion-pseudometric-completion-Pseudometric-Space =
+    metric-pseudocompletion-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space P)
+```
+
+## Properties
+
+### The isometry from the pseudometric completion of a pseudometric space into its metric pseudocompletion
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  isometry-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space P)
+      ( pseudometric-metric-pseudocompletion-Pseudometric-Space P)
+  isometry-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space =
+    isometry-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space P)
+```
+
+### The isometry from a pseudometric space into its metric pseudocompletion
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  isometry-metric-pseudocompletion-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( P)
+      ( pseudometric-metric-pseudocompletion-Pseudometric-Space P)
+  isometry-metric-pseudocompletion-Pseudometric-Space =
+    comp-isometry-Pseudometric-Space
+      ( P)
+      ( pseudometric-completion-Pseudometric-Space P)
+      ( pseudometric-metric-pseudocompletion-Pseudometric-Space P)
+      ( isometry-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+        ( P))
+      ( isometry-pseudometric-completion-Pseudometric-Space P)
+```
+
+### The isometry from the pseudometric completion of the pseudometric completion into the metric pseudocompletion
+
+```agda
+module _
+  { l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  isometry-metric-pseudocompletion-pseudometric-completion²-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P))
+      ( pseudometric-metric-pseudocompletion-Pseudometric-Space P)
+  isometry-metric-pseudocompletion-pseudometric-completion²-Pseudometric-Space =
+    comp-isometry-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P))
+      ( pseudometric-completion-Pseudometric-Space P)
+      ( pseudometric-metric-pseudocompletion-Pseudometric-Space P)
+      ( isometry-metric-quotient-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P))
+      ( isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+        ( P))
+
+  short-map-metric-pseudocompletion-pseudometric-completion²-Pseudometric-Space :
+    short-function-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P))
+      ( pseudometric-metric-pseudocompletion-Pseudometric-Space P)
+  short-map-metric-pseudocompletion-pseudometric-completion²-Pseudometric-Space =
+    short-isometry-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P))
+      ( pseudometric-metric-pseudocompletion-Pseudometric-Space P)
+      ( isometry-metric-pseudocompletion-pseudometric-completion²-Pseudometric-Space)
+```
+
+### The short isomorphism from the metric pseudocompletion of the pseudometric completion of a pseudometric space into its metric pseudocompletion
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  short-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space :
+    short-function-Metric-Space
+      ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P)
+      ( metric-pseudocompletion-Pseudometric-Space P)
+  short-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space =
+    short-map-short-function-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P))
+      ( metric-pseudocompletion-Pseudometric-Space P)
+      ( short-map-metric-pseudocompletion-pseudometric-completion²-Pseudometric-Space
+        ( P))
+
+  map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space :
+    type-function-Metric-Space
+      ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P)
+      ( metric-pseudocompletion-Pseudometric-Space P)
+  map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space =
+    map-short-function-Metric-Space
+      ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P)
+      ( metric-pseudocompletion-Pseudometric-Space P)
+      ( short-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space)
+
+  compute-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space :
+    ( X :
+      type-metric-pseudocompletion-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P)) →
+    ( x :
+      cauchy-approximation-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space P)) →
+    is-in-class-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P))
+      ( X)
+      ( x) →
+    map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space X ＝
+    map-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space P)
+      ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+        ( P)
+        ( x))
+  compute-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+    =
+    compute-map-short-function-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P))
+      ( metric-pseudocompletion-Pseudometric-Space P)
+      ( short-map-metric-pseudocompletion-pseudometric-completion²-Pseudometric-Space
+        ( P))
+
+  short-map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space :
+    short-function-Metric-Space
+      ( metric-pseudocompletion-Pseudometric-Space P)
+      ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P)
+  short-map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space =
+    short-map-short-function-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space P)
+      ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P)
+      ( comp-short-function-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P)
+        ( pseudometric-completion-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space P))
+        ( pseudometric-metric-pseudocompletion-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space P))
+        ( short-map-metric-quotient-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space P)))
+        ( short-map-pseudometric-completion-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space P)))
+
+  map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space :
+    type-function-Metric-Space
+      ( metric-pseudocompletion-Pseudometric-Space P)
+      ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P)
+  map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space =
+    map-short-function-Metric-Space
+      ( metric-pseudocompletion-Pseudometric-Space P)
+      ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P)
+      ( short-map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space)
+
+  compute-map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space :
+    (X : type-metric-pseudocompletion-Pseudometric-Space P) →
+    (x : cauchy-approximation-Pseudometric-Space P) →
+    is-in-class-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space P)
+      ( X)
+      ( x) →
+    map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+      ( X) ＝
+    map-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P))
+      ( map-pseudometric-completion-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P)
+        ( x))
+  compute-map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+    =
+    compute-map-short-function-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space P)
+      ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P)
+      ( comp-short-function-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P)
+        ( pseudometric-completion-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space P))
+        ( pseudometric-metric-pseudocompletion-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space P))
+        ( short-map-metric-quotient-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space P)))
+        ( short-map-pseudometric-completion-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space P)))
+
+  is-section-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space :
+    ( map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space ∘
+      map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space) ~
+    id
+  is-section-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+    X =
+    let
+      open
+        do-syntax-trunc-Prop
+          ( Id-Prop
+            ( set-Metric-Space
+              ( metric-pseudocompletion-Pseudometric-Space P))
+            ( map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+              ( map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+                ( X)))
+            ( X))
+    in do
+      ( x , x∈X) ←
+        is-inhabited-class-metric-quotient-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space P)
+          ( X)
+      let
+        map-inv-X =
+          map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+            ( X)
+
+        compute-map-inv-X :
+          map-inv-X ＝
+          map-metric-quotient-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P))
+            ( map-pseudometric-completion-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P)
+              ( x))
+        compute-map-inv-X =
+          compute-map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+            ( X)
+            ( x)
+            ( x∈X)
+
+        is-in-class-x :
+          is-in-class-metric-quotient-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P))
+            ( map-inv-X)
+            ( map-pseudometric-completion-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P)
+              ( x))
+        is-in-class-x =
+          inv-tr
+            ( λ Y →
+              is-in-class-metric-quotient-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space
+                  ( pseudometric-completion-Pseudometric-Space P))
+                ( Y)
+                ( map-pseudometric-completion-Pseudometric-Space
+                  ( pseudometric-completion-Pseudometric-Space P)
+                  ( x)))
+            ( compute-map-inv-X)
+            ( is-in-class-map-quotient-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space P))
+              ( map-pseudometric-completion-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space P)
+                ( x)))
+
+        compute-map :
+          map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+            ( map-inv-X) ＝
+          map-metric-quotient-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space P)
+            ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+              ( P)
+              ( map-pseudometric-completion-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space P)
+                ( x)))
+        compute-map =
+          compute-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+            ( map-inv-X)
+            ( map-pseudometric-completion-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P)
+              ( x))
+            ( is-in-class-x)
+
+        compute-quotient-lim :
+          map-metric-quotient-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space P)
+            ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+              ( P)
+              ( map-pseudometric-completion-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space P)
+                ( x))) ＝
+          map-metric-quotient-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space P)
+            ( x)
+        compute-quotient-lim =
+          apply-effectiveness-quotient-map'
+            ( equivalence-relation-sim-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P))
+            ( all-sim-is-limit-cauchy-approximation-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P)
+              ( map-pseudometric-completion-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space P)
+                ( x))
+              ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                ( P)
+                ( map-pseudometric-completion-Pseudometric-Space
+                  ( pseudometric-completion-Pseudometric-Space P)
+                  ( x)))
+              ( x)
+              ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                ( P)
+                ( map-pseudometric-completion-Pseudometric-Space
+                  ( pseudometric-completion-Pseudometric-Space P)
+                  ( x)))
+              ( is-limit-const-cauchy-approximation-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space P)
+                ( x)))
+
+        compute-quotient-x :
+          map-metric-quotient-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space P)
+            ( x) ＝ X
+        compute-quotient-x =
+          eq-set-quotient-equivalence-class-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P))
+            ( X)
+            ( x∈X)
+
+      ( compute-map ∙
+        compute-quotient-lim ∙
+        compute-quotient-x)
+
+  is-retraction-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space :
+    ( map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space ∘
+      map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space)
+      ~
+    id
+  is-retraction-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+    X =
+    let
+      open
+        do-syntax-trunc-Prop
+          ( Id-Prop
+            ( set-Metric-Space
+              ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+                ( P)))
+            ( map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+              ( map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+                ( X)))
+            ( X))
+
+    in do
+      ( x , x∈X) ←
+        is-inhabited-class-metric-quotient-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space P))
+          ( X)
+      let
+        map-X =
+          map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+            ( X)
+
+        compute-map-X :
+          map-X ＝
+          map-metric-quotient-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space P)
+            ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+              ( P)
+              ( x))
+        compute-map-X =
+          compute-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+            ( X)
+            ( x)
+            ( x∈X)
+
+        is-in-class-map-X :
+          is-in-class-metric-quotient-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space P)
+            ( map-X)
+            ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+              ( P)
+              ( x))
+        is-in-class-map-X =
+          inv-tr
+            ( λ Y →
+              is-in-class-metric-quotient-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space P)
+                ( Y)
+                ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                  ( P)
+                  ( x)))
+            ( compute-map-X)
+            ( is-in-class-map-quotient-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P)
+              ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                ( P)
+                ( x)))
+
+        compute-map-inv :
+          map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+            ( map-X) ＝
+          map-metric-quotient-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P))
+            ( map-pseudometric-completion-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P)
+              ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                ( P)
+                ( x)))
+        compute-map-inv =
+          compute-map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+            ( map-X)
+            ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+              ( P)
+              ( x))
+            ( is-in-class-map-X)
+
+        compute-map-quotient-lim :
+          map-metric-quotient-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P))
+            ( map-pseudometric-completion-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P)
+              ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                ( P)
+                ( x))) ＝
+          map-metric-quotient-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P))
+            ( x)
+        compute-map-quotient-lim =
+          apply-effectiveness-quotient-map'
+            ( equivalence-relation-sim-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space P)))
+            ( symmetric-sim-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space P))
+              ( x)
+              ( map-pseudometric-completion-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space P)
+                ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                  ( P)
+                  ( x)))
+              ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space P)
+                ( x)
+                ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                  ( P)
+                  ( x))
+                ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                  ( P)
+                  ( x))))
+
+        compute-quotient-x :
+          map-metric-quotient-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P))
+            ( x) ＝
+          X
+        compute-quotient-x =
+          eq-set-quotient-equivalence-class-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space P)))
+            ( X)
+            ( x∈X)
+
+      ( compute-map-inv ∙
+        compute-map-quotient-lim ∙
+        compute-quotient-x)
+
+  is-iso-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space :
+    is-iso-Precategory
+      precategory-short-function-Metric-Space
+      { metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P}
+      { metric-pseudocompletion-Pseudometric-Space P}
+      short-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+  pr1
+    is-iso-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+    =
+    short-map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+  pr2
+    is-iso-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+    =
+    ( ( eq-htpy-map-short-function-Metric-Space
+        ( metric-pseudocompletion-Pseudometric-Space P)
+        ( metric-pseudocompletion-Pseudometric-Space P)
+        ( comp-short-function-Metric-Space
+          ( metric-pseudocompletion-Pseudometric-Space P)
+          ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+            ( P))
+          ( metric-pseudocompletion-Pseudometric-Space P)
+          ( short-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space)
+          ( short-map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space))
+        ( short-id-Metric-Space
+          ( metric-pseudocompletion-Pseudometric-Space P))
+        ( is-section-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space)) ,
+      ( eq-htpy-map-short-function-Metric-Space
+        ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P)
+        ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P)
+        ( comp-short-function-Metric-Space
+          ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+            ( P))
+          ( metric-pseudocompletion-Pseudometric-Space P)
+            ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+              ( P))
+          ( short-map-inv-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space)
+          ( short-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space))
+        ( short-id-Metric-Space
+          ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space
+            ( P)))
+        ( is-retraction-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space)))
+
+  iso-metric-pseudocompeletion-pseudometric-completion-Pseudometric-Space :
+    iso-Precategory
+      ( precategory-short-function-Metric-Space)
+      ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P)
+      ( metric-pseudocompletion-Pseudometric-Space P)
+  iso-metric-pseudocompeletion-pseudometric-completion-Pseudometric-Space =
+    ( short-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space ,
+      is-iso-map-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space)
+```
+
+### The equality between the metric pseudocompletion of the pseudometric completion of a pseudometric space and its metric pseudocompletion
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  eq-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space :
+    ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P) ＝
+    ( metric-pseudocompletion-Pseudometric-Space P)
+  eq-metric-pseudocompletion-pseudometric-completion-Pseudometric-Space =
+    eq-isometric-equiv-Metric-Space'
+      ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P)
+      ( metric-pseudocompletion-Pseudometric-Space P)
+      ( map-equiv-isometric-equiv-iso-short-function-Metric-Space'
+        ( metric-pseudocompletion-pseudometric-completion-Pseudometric-Space P)
+        ( metric-pseudocompletion-Pseudometric-Space P)
+        ( iso-metric-pseudocompeletion-pseudometric-completion-Pseudometric-Space
+          ( P)))
+```
+
+### Cauchy approximations similar to pointwise quotient of Cauchy approximations in the pseudometric completion are convergent
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  ( u :
+    cauchy-approximation-Metric-Space
+      ( metric-pseudocompletion-Pseudometric-Space P))
+  where
+
+  is-convergent-has-lift-cauchy-approximation-metric-pseudocompletion-Pseudometric-Space :
+    has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space P)
+      ( u) →
+    is-convergent-cauchy-approximation-Metric-Space
+      ( metric-pseudocompletion-Pseudometric-Space P)
+      ( u)
+  is-convergent-has-lift-cauchy-approximation-metric-pseudocompletion-Pseudometric-Space
+    sim-lift =
+    let
+      open
+        do-syntax-trunc-Prop
+          ( is-convergent-prop-cauchy-approximation-Metric-Space
+            ( metric-pseudocompletion-Pseudometric-Space P)
+            ( u))
+    in do
+      ( v , u~[v]) ← sim-lift
+      let
+        ( lim-v , is-lim-v) =
+          has-limit-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( P)
+            ( v)
+
+        lim-u =
+          map-metric-quotient-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space P)
+            ( lim-v)
+
+        is-lim[v]-lim-u :
+          is-limit-cauchy-approximation-Metric-Space
+            ( metric-quotient-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P))
+            ( map-metric-quotient-cauchy-approximation-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P)
+              ( v))
+            ( lim-u)
+        is-lim[v]-lim-u =
+          preserves-limit-map-metric-quotient-cauchy-approximation-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space P)
+            ( v)
+            ( lim-v)
+            ( is-lim-v)
+
+        [lim-u] =
+          const-cauchy-approximation-Metric-Space
+            ( metric-pseudocompletion-Pseudometric-Space P)
+            ( lim-u)
+
+        u~[lim-u] :
+          sim-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space
+              ( pseudometric-metric-pseudocompletion-Pseudometric-Space P))
+            ( u)
+            ( [lim-u])
+        u~[lim-u] =
+          transitive-sim-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space
+              ( pseudometric-metric-pseudocompletion-Pseudometric-Space P))
+            ( u)
+            ( map-metric-quotient-cauchy-approximation-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space P)
+              ( v))
+            ( [lim-u])
+            ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+              ( pseudometric-metric-pseudocompletion-Pseudometric-Space P)
+              ( map-metric-quotient-cauchy-approximation-Pseudometric-Space
+                ( pseudometric-completion-Pseudometric-Space P)
+                ( v))
+              ( lim-u)
+              ( is-lim[v]-lim-u))
+            ( u~[v])
+      ( ( lim-u) ,
+        ( is-limit-sim-const-cauchy-approximation-Pseudometric-Space
+          ( pseudometric-metric-pseudocompletion-Pseudometric-Space P)
+          ( u)
+          ( lim-u)
+          ( u~[lim-u])))
+
+  iff-has-lift-is-convergent-cauchy-approximation-metric-pseudocompletion-Pseudometric-Space :
+    is-convergent-cauchy-approximation-Metric-Space
+      ( metric-pseudocompletion-Pseudometric-Space P)
+      ( u) ↔
+    has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space P)
+      ( u)
+  pr1
+    iff-has-lift-is-convergent-cauchy-approximation-metric-pseudocompletion-Pseudometric-Space
+    =
+    has-lift-is-convergent-cauchy-approximation-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space P)
+      ( u)
+  pr2
+    iff-has-lift-is-convergent-cauchy-approximation-metric-pseudocompletion-Pseudometric-Space
+    =
+    is-convergent-has-lift-cauchy-approximation-metric-pseudocompletion-Pseudometric-Space
+
+  equiv-has-lift-is-convergent-cauchy-approximation-metric-pseudocompletion-Pseudometric-Space :
+    is-convergent-cauchy-approximation-Metric-Space
+      ( metric-pseudocompletion-Pseudometric-Space P)
+      ( u) ≃
+    has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space P)
+      ( u)
+  equiv-has-lift-is-convergent-cauchy-approximation-metric-pseudocompletion-Pseudometric-Space
+    =
+    equiv-iff
+      ( is-convergent-prop-cauchy-approximation-Metric-Space
+        ( metric-pseudocompletion-Pseudometric-Space P)
+        ( u))
+      ( has-lift-prop-cauchy-approximation-metric-quotient-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P)
+        ( u))
+      ( has-lift-is-convergent-cauchy-approximation-metric-quotient-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space P)
+        ( u))
+      ( is-convergent-has-lift-cauchy-approximation-metric-pseudocompletion-Pseudometric-Space)
+```
diff --git a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..f0d82da780
--- /dev/null
+++ b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md
@@ -0,0 +1,836 @@
+# Metric quotients of pseudometric spaces
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module metric-spaces.metric-quotients-of-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-relations
+open import foundation.binary-transport
+open import foundation.contractible-maps
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equivalence-classes
+open import foundation.equivalences
+open import foundation.existential-quantification
+open import foundation.fibers-of-maps
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.inhabited-subtypes
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.reflecting-maps-equivalence-relations
+open import foundation.retractions
+open import foundation.sections
+open import foundation.set-quotients
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universal-property-set-quotients
+open import foundation.universe-levels
+
+open import logic.functoriality-existential-quantification
+
+open import metric-spaces.cauchy-approximations-metric-spaces
+open import metric-spaces.cauchy-approximations-pseudometric-spaces
+open import metric-spaces.convergent-cauchy-approximations-metric-spaces
+open import metric-spaces.equality-of-metric-spaces
+open import metric-spaces.extensionality-pseudometric-spaces
+open import metric-spaces.functions-metric-spaces
+open import metric-spaces.isometries-metric-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-completion-of-pseudometric-spaces
+open import metric-spaces.pseudometric-spaces
+open import metric-spaces.rational-neighborhood-relations
+open import metric-spaces.short-functions-metric-spaces
+open import metric-spaces.short-functions-pseudometric-spaces
+open import metric-spaces.similarity-of-elements-pseudometric-spaces
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "metric quotient" Disambiguation="of a pseudometric space" Agda=metric-quotient-Pseudometric-Space}}
+of a [pseudometric space](metric-spaces.pseudometric-spaces.md) is the
+[metric space](metric-spaces.metric-spaces.md) whose points are
+[quotient classes](foundation.set-quotients.md) of `M` by the
+[similarity relation](metric-spaces.similarity-of-elements-pseudometric-spaces.md)
+and [neighborhoods](metric-spaces.rational-neighborhood-relations.md) given by
+neighborhoods of inhabitants of the quotient classes: two quotient classes `X`,
+`Y` are in a `d`-neighborhood if for all `x ∈ X` and `y ∈ Y`, `x` and `y` are
+`d`-neighbors in the pseudometric space.
+
+Any pseudometric space `M` has an
+[isometry](metric-spaces.isometries-pseudometric-spaces.md) into its metric
+quotient; if `M` is a metric space, this is an
+[isometric equivalence](metric-spaces.equality-of-metric-spaces.md).
+
+Any [short map](metric-spaces.short-functions-pseudometric-spaces.md) (resp.
+isometry) from a pseudometric space to a metric space factors through the metric
+quotient of its domain.
+
+## Definitions
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  set-metric-quotient-Pseudometric-Space : Set (l1 ⊔ l2)
+  set-metric-quotient-Pseudometric-Space =
+    quotient-Set (equivalence-relation-sim-Pseudometric-Space M)
+
+  type-metric-quotient-Pseudometric-Space : UU (l1 ⊔ l2)
+  type-metric-quotient-Pseudometric-Space =
+    type-Set set-metric-quotient-Pseudometric-Space
+
+  subtype-class-metric-quotient-Pseudometric-Space :
+    (X : type-metric-quotient-Pseudometric-Space) →
+    subtype l2 (type-Pseudometric-Space M)
+  subtype-class-metric-quotient-Pseudometric-Space =
+    subtype-set-quotient
+      ( equivalence-relation-sim-Pseudometric-Space M)
+
+  is-in-class-metric-quotient-Pseudometric-Space :
+    (X : type-metric-quotient-Pseudometric-Space) →
+    type-Pseudometric-Space M →
+    UU l2
+  is-in-class-metric-quotient-Pseudometric-Space =
+    is-in-equivalence-class-set-quotient
+      ( equivalence-relation-sim-Pseudometric-Space M)
+
+  type-subtype-metric-quotient-Pseudometric-Space :
+    (X : type-metric-quotient-Pseudometric-Space) → UU (l1 ⊔ l2)
+  type-subtype-metric-quotient-Pseudometric-Space X =
+    type-subtype
+      ( subtype-class-metric-quotient-Pseudometric-Space X)
+
+  neighborhood-prop-metric-quotient-Pseudometric-Space :
+    Rational-Neighborhood-Relation
+      ( l1 ⊔ l2)
+      ( type-metric-quotient-Pseudometric-Space)
+  neighborhood-prop-metric-quotient-Pseudometric-Space ε X Y =
+    Π-Prop
+      ( type-subtype-metric-quotient-Pseudometric-Space X)
+      ( λ (x , x∈X) →
+        Π-Prop
+          ( type-subtype-metric-quotient-Pseudometric-Space Y)
+          ( λ (y , y∈Y) → neighborhood-prop-Pseudometric-Space M ε x y))
+
+  neighborhood-metric-quotient-Pseudometric-Space :
+    ℚ⁺ → Relation (l1 ⊔ l2) type-metric-quotient-Pseudometric-Space
+  neighborhood-metric-quotient-Pseudometric-Space ε X Y =
+    type-Prop (neighborhood-prop-metric-quotient-Pseudometric-Space ε X Y)
+```
+
+## Properties
+
+### All quotient classes are inhabited
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
+  (x : type-metric-quotient-Pseudometric-Space A)
+  where
+
+  is-inhabited-class-metric-quotient-Pseudometric-Space :
+    is-inhabited-subtype
+      ( subtype-class-metric-quotient-Pseudometric-Space A x)
+  is-inhabited-class-metric-quotient-Pseudometric-Space =
+    is-inhabited-subtype-set-quotient
+      ( equivalence-relation-sim-Pseudometric-Space A)
+      ( x)
+```
+
+### The quotient neighborhood relation is reflexive
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    is-reflexive-neighborhood-metric-quotient-Pseudometric-Space :
+      (d : ℚ⁺) (X : type-metric-quotient-Pseudometric-Space M) →
+      neighborhood-metric-quotient-Pseudometric-Space M d X X
+    is-reflexive-neighborhood-metric-quotient-Pseudometric-Space
+      d X (x , x∈X) (y , y∈X) =
+      apply-effectiveness-quotient-map
+        ( equivalence-relation-sim-Pseudometric-Space M)
+        ( ( eq-set-quotient-equivalence-class-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space M)
+            ( X)
+            ( x∈X)) ∙
+          ( inv
+            ( eq-set-quotient-equivalence-class-set-quotient
+              ( equivalence-relation-sim-Pseudometric-Space M)
+              ( X)
+              ( y∈X))))
+        ( d)
+```
+
+### The quotient neighborhood relation is symmetric
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    is-symmetric-neighborhood-metric-quotient-Pseudometric-Space :
+      (d : ℚ⁺) (x y : type-metric-quotient-Pseudometric-Space M) →
+      neighborhood-metric-quotient-Pseudometric-Space M d x y →
+      neighborhood-metric-quotient-Pseudometric-Space M d y x
+    is-symmetric-neighborhood-metric-quotient-Pseudometric-Space
+      d X Y d⟨X,Y⟩ (y , y∈Y) (x , x∈X) =
+      symmetric-neighborhood-Pseudometric-Space
+        ( M)
+        ( d)
+        ( x)
+        ( y)
+        ( d⟨X,Y⟩ (x , x∈X) (y , y∈Y))
+```
+
+### The quotient neighborhood relation is triangular
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  (X Y Z : type-metric-quotient-Pseudometric-Space M)
+  (d₁ d₂ : ℚ⁺)
+  where
+
+  abstract
+    is-triangular-neighborhood-metric-quotient-Pseudometric-Space :
+      neighborhood-metric-quotient-Pseudometric-Space M d₂ Y Z →
+      neighborhood-metric-quotient-Pseudometric-Space M d₁ X Y →
+      neighborhood-metric-quotient-Pseudometric-Space M (d₁ +ℚ⁺ d₂) X Z
+    is-triangular-neighborhood-metric-quotient-Pseudometric-Space
+      d₂⟨Y,Z⟩ d₁⟨X,Y⟩ (x , x∈X) (z , z∈Z) =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( neighborhood-prop-Pseudometric-Space M (d₁ +ℚ⁺ d₂) x z)
+      in do
+        (y , y∈Y) ←
+          is-inhabited-subtype-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space M)
+            ( Y)
+        triangular-neighborhood-Pseudometric-Space
+          ( M)
+          ( x)
+          ( y)
+          ( z)
+          ( d₁)
+          ( d₂)
+          ( d₂⟨Y,Z⟩ (y , y∈Y) (z , z∈Z))
+          ( d₁⟨X,Y⟩ (x , x∈X) (y , y∈Y))
+```
+
+### The quotient neighborhood relation is saturated
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    is-saturated-neighborhood-metric-quotient-Pseudometric-Space :
+      (ε : ℚ⁺) (X Y : type-metric-quotient-Pseudometric-Space M) →
+      ((δ : ℚ⁺) →
+        neighborhood-metric-quotient-Pseudometric-Space M (ε +ℚ⁺ δ) X Y) →
+      neighborhood-metric-quotient-Pseudometric-Space M ε X Y
+    is-saturated-neighborhood-metric-quotient-Pseudometric-Space
+      ε X Y H (x , x∈X) (y , y∈Y) =
+      saturated-neighborhood-Pseudometric-Space M ε x y
+        ( λ δ → H δ (x , x∈X) (y , y∈Y))
+```
+
+### The quotient pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  pseudometric-metric-quotient-Pseudometric-Space :
+    Pseudometric-Space (l1 ⊔ l2) (l1 ⊔ l2)
+  pseudometric-metric-quotient-Pseudometric-Space =
+    ( type-metric-quotient-Pseudometric-Space M ,
+      neighborhood-prop-metric-quotient-Pseudometric-Space M ,
+      is-reflexive-neighborhood-metric-quotient-Pseudometric-Space M ,
+      is-symmetric-neighborhood-metric-quotient-Pseudometric-Space M ,
+      is-triangular-neighborhood-metric-quotient-Pseudometric-Space M ,
+      is-saturated-neighborhood-metric-quotient-Pseudometric-Space M)
+```
+
+### The quotient pseudometric space is tight and extensional
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    is-tight-pseudometric-metric-quotient-Pseudometric-Space :
+      is-tight-Pseudometric-Space
+        (pseudometric-metric-quotient-Pseudometric-Space M)
+    is-tight-pseudometric-metric-quotient-Pseudometric-Space X Y X~Y =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( Id-Prop
+              ( set-metric-quotient-Pseudometric-Space M)
+              ( X)
+              ( Y))
+      in do
+        ( x , x∈X) ←
+          is-inhabited-subtype-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space M)
+            ( X)
+
+        ( y , y∈Y) ←
+          is-inhabited-subtype-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space M)
+            ( Y)
+
+        eq-set-quotient-sim-element-set-quotient
+          ( equivalence-relation-sim-Pseudometric-Space M)
+          ( X)
+          ( Y)
+          ( x∈X)
+          ( y∈Y)
+          ( λ d → X~Y d (x , x∈X) (y , y∈Y))
+
+    is-extensional-pseudometric-metric-quotient-Pseudometric-Space :
+      is-extensional-Pseudometric-Space
+        ( pseudometric-metric-quotient-Pseudometric-Space M)
+    is-extensional-pseudometric-metric-quotient-Pseudometric-Space =
+      is-extensional-is-tight-Pseudometric-Space
+        ( pseudometric-metric-quotient-Pseudometric-Space M)
+        ( is-tight-pseudometric-metric-quotient-Pseudometric-Space)
+```
+
+### The quotient metric space of a pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  metric-quotient-Pseudometric-Space : Metric-Space (l1 ⊔ l2) (l1 ⊔ l2)
+  metric-quotient-Pseudometric-Space =
+    make-Metric-Space
+      ( type-metric-quotient-Pseudometric-Space M)
+      ( neighborhood-prop-metric-quotient-Pseudometric-Space M)
+      ( is-reflexive-neighborhood-metric-quotient-Pseudometric-Space M)
+      ( is-symmetric-neighborhood-metric-quotient-Pseudometric-Space M)
+      ( is-triangular-neighborhood-metric-quotient-Pseudometric-Space M)
+      ( is-saturated-neighborhood-metric-quotient-Pseudometric-Space M)
+      ( is-extensional-pseudometric-metric-quotient-Pseudometric-Space M)
+```
+
+### The mapping from a pseudometric space to its quotient metric space
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  map-metric-quotient-Pseudometric-Space :
+    type-Pseudometric-Space M → type-metric-quotient-Pseudometric-Space M
+  map-metric-quotient-Pseudometric-Space =
+    quotient-map (equivalence-relation-sim-Pseudometric-Space M)
+
+  is-in-class-map-quotient-Pseudometric-Space :
+    (x : type-Pseudometric-Space M) →
+    is-in-class-metric-quotient-Pseudometric-Space
+      ( M)
+      ( map-metric-quotient-Pseudometric-Space x)
+      ( x)
+  is-in-class-map-quotient-Pseudometric-Space =
+    is-in-equivalence-class-quotient-map-set-quotient
+      ( equivalence-relation-sim-Pseudometric-Space M)
+
+  map-subtype-metric-quotient-Pseudometric-Space :
+    (x : type-Pseudometric-Space M) →
+    type-subtype-metric-quotient-Pseudometric-Space M
+      ( map-metric-quotient-Pseudometric-Space x)
+  map-subtype-metric-quotient-Pseudometric-Space =
+    inhabitant-equivalence-class-quotient-map-set-quotient
+      ( equivalence-relation-sim-Pseudometric-Space M)
+```
+
+### The mapping from a pseudometric space its quotient metric space is an isometry
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    preserves-neighborhood-map-metric-quotient-Pseudometric-Space :
+      (d : ℚ⁺) (x y : type-Pseudometric-Space M) →
+      neighborhood-Pseudometric-Space M d x y →
+      neighborhood-metric-quotient-Pseudometric-Space
+        ( M)
+        ( d)
+        ( map-metric-quotient-Pseudometric-Space M x)
+        ( map-metric-quotient-Pseudometric-Space M y)
+    preserves-neighborhood-map-metric-quotient-Pseudometric-Space
+      d x y d⟨x,y⟩ (x' , x≈x') (y' , y≈y') =
+      let
+        x~x' =
+          sim-is-in-equivalence-class-quotient-map-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space M)
+            ( x)
+            ( x')
+            ( x≈x')
+
+        y~y' =
+          sim-is-in-equivalence-class-quotient-map-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space M)
+            ( y)
+            ( y')
+            ( y≈y')
+
+      in
+        preserves-neighborhood-right-sim-Pseudometric-Space M y~y' d x'
+          ( preserves-neighborhood-left-sim-Pseudometric-Space
+            ( M)
+            ( x~x')
+            ( d)
+            ( y)
+            ( d⟨x,y⟩))
+
+    reflects-neighborhood-map-metric-quotient-Pseudometric-Space :
+      (d : ℚ⁺) (x y : type-Pseudometric-Space M) →
+      neighborhood-metric-quotient-Pseudometric-Space
+        ( M)
+        ( d)
+        ( map-metric-quotient-Pseudometric-Space M x)
+        ( map-metric-quotient-Pseudometric-Space M y) →
+      neighborhood-Pseudometric-Space M d x y
+    reflects-neighborhood-map-metric-quotient-Pseudometric-Space
+      d x y Nxy =
+        Nxy
+          ( map-subtype-metric-quotient-Pseudometric-Space M x)
+          ( map-subtype-metric-quotient-Pseudometric-Space M y)
+
+  is-isometry-map-metric-quotient-Pseudometric-Space :
+    is-isometry-Pseudometric-Space
+      ( M)
+      ( pseudometric-metric-quotient-Pseudometric-Space M)
+      ( map-metric-quotient-Pseudometric-Space M)
+  is-isometry-map-metric-quotient-Pseudometric-Space d x y =
+    ( preserves-neighborhood-map-metric-quotient-Pseudometric-Space d x y ,
+      reflects-neighborhood-map-metric-quotient-Pseudometric-Space d x y)
+```
+
+### The isometry from a pseudometric space to its quotient metric space
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  isometry-metric-quotient-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( M)
+      ( pseudometric-metric-quotient-Pseudometric-Space M)
+  isometry-metric-quotient-Pseudometric-Space =
+    ( map-metric-quotient-Pseudometric-Space M ,
+      is-isometry-map-metric-quotient-Pseudometric-Space M)
+```
+
+### The short map from a pseudometric space to its quotient metric space
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  short-map-metric-quotient-Pseudometric-Space :
+    short-function-Pseudometric-Space
+      ( M)
+      ( pseudometric-metric-quotient-Pseudometric-Space M)
+  short-map-metric-quotient-Pseudometric-Space =
+    short-isometry-Pseudometric-Space
+      ( M)
+      ( pseudometric-metric-quotient-Pseudometric-Space M)
+      ( isometry-metric-quotient-Pseudometric-Space M)
+```
+
+### The isometric equivalence between a metric space and the quotient metric space of its pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Metric-Space l1 l2)
+  where
+
+  map-metric-quotient-Metric-Space :
+    type-Metric-Space M →
+    type-metric-quotient-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+  map-metric-quotient-Metric-Space =
+    map-metric-quotient-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+
+  abstract
+    is-contr-map-metric-quotient-Metric-Space :
+      is-contr-map map-metric-quotient-Metric-Space
+    is-contr-map-metric-quotient-Metric-Space X =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( is-contr-Prop
+              ( fiber map-metric-quotient-Metric-Space X))
+        in do
+          ( x , x∈X) ←
+            is-inhabited-subtype-set-quotient
+              ( equivalence-relation-sim-Metric-Space M)
+              ( X)
+
+          ( ( x ,
+              eq-set-quotient-equivalence-class-set-quotient
+                ( equivalence-relation-sim-Metric-Space M)
+                ( X)
+                ( x∈X)) ,
+            ( λ (y , Y＝X) →
+              eq-type-subtype
+                ( λ z →
+                  Id-Prop
+                    ( set-metric-quotient-Pseudometric-Space
+                      ( pseudometric-Metric-Space M))
+                      ( map-metric-quotient-Metric-Space z)
+                      ( X))
+                ( eq-sim-Metric-Space
+                  ( M)
+                  ( x)
+                  ( y)
+                  ( apply-effectiveness-quotient-map
+                    ( equivalence-relation-sim-Metric-Space M)
+                    ( ( eq-set-quotient-equivalence-class-set-quotient
+                        ( equivalence-relation-sim-Metric-Space M)
+                        ( X)
+                        ( x∈X)) ∙
+                      ( inv Y＝X))))))
+
+    is-equiv-map-metric-quotient-Metric-Space :
+      is-equiv map-metric-quotient-Metric-Space
+    is-equiv-map-metric-quotient-Metric-Space =
+      is-equiv-is-contr-map
+        ( is-contr-map-metric-quotient-Metric-Space)
+
+    is-isometry-map-metric-quotient-Metric-Space :
+      is-isometry-Metric-Space
+        ( M)
+        ( metric-quotient-Pseudometric-Space
+          ( pseudometric-Metric-Space M))
+        ( map-metric-quotient-Metric-Space)
+    is-isometry-map-metric-quotient-Metric-Space =
+      is-isometry-map-metric-quotient-Pseudometric-Space
+        ( pseudometric-Metric-Space M)
+
+  isometric-equiv-metric-quotient-Metric-Space' :
+    isometric-equiv-Metric-Space'
+      ( M)
+      ( metric-quotient-Pseudometric-Space
+        ( pseudometric-Metric-Space M))
+  isometric-equiv-metric-quotient-Metric-Space' =
+    ( map-metric-quotient-Metric-Space ,
+      is-equiv-map-metric-quotient-Metric-Space ,
+      is-isometry-map-metric-quotient-Metric-Space)
+```
+
+### The construction of the quotient metric space of a pseudometric space is idempotent
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  is-idempotent-metric-quotient-Pseudometric-Space :
+    metric-quotient-Pseudometric-Space
+      ( pseudometric-Metric-Space
+        ( metric-quotient-Pseudometric-Space M)) ＝
+    metric-quotient-Pseudometric-Space M
+  is-idempotent-metric-quotient-Pseudometric-Space =
+    inv
+      ( eq-isometric-equiv-Metric-Space'
+        ( metric-quotient-Pseudometric-Space M)
+        ( metric-quotient-Pseudometric-Space
+          ( pseudometric-Metric-Space
+            ( metric-quotient-Pseudometric-Space M)))
+        ( isometric-equiv-metric-quotient-Metric-Space'
+          ( metric-quotient-Pseudometric-Space M)))
+```
+
+### Induced short function from the quotient metric space into a metric space
+
+```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
+
+  map-short-function-metric-quotient-Pseudometric-space :
+    type-function-Metric-Space
+      ( metric-quotient-Pseudometric-Space A)
+      ( B)
+  map-short-function-metric-quotient-Pseudometric-space =
+    inv-precomp-set-quotient
+      ( equivalence-relation-sim-Pseudometric-Space A)
+      ( set-Metric-Space B)
+      ( reflecting-map-short-function-metric-space-Pseudometric-Space A B f)
+
+  htpy-map-short-function-metric-quotient-Pseudometric-Space :
+    ( ( map-short-function-metric-quotient-Pseudometric-space) ∘
+      ( map-metric-quotient-Pseudometric-Space A)) ~
+    ( map-short-function-Pseudometric-Space A (pseudometric-Metric-Space B) f)
+  htpy-map-short-function-metric-quotient-Pseudometric-Space =
+    is-section-inv-precomp-set-quotient
+      ( equivalence-relation-sim-Pseudometric-Space A)
+      ( set-Metric-Space B)
+      ( reflecting-map-short-function-metric-space-Pseudometric-Space A B f)
+
+  compute-map-short-function-metric-quotient-Pseudometric-Space :
+    (X : type-metric-quotient-Pseudometric-Space A) →
+    (x : type-Pseudometric-Space A) →
+    is-in-class-metric-quotient-Pseudometric-Space A X x →
+    map-short-function-metric-quotient-Pseudometric-space X ＝
+    map-short-function-Pseudometric-Space A (pseudometric-Metric-Space B) f x
+  compute-map-short-function-metric-quotient-Pseudometric-Space X x x∈X =
+    tr
+      ( λ Y →
+        map-short-function-metric-quotient-Pseudometric-space Y ＝
+        map-short-function-Pseudometric-Space
+          ( A)
+          ( pseudometric-Metric-Space B)
+          ( f)
+          ( x))
+      ( eq-set-quotient-equivalence-class-set-quotient
+        ( equivalence-relation-sim-Pseudometric-Space A)
+        ( X)
+        ( x∈X))
+      ( htpy-map-short-function-metric-quotient-Pseudometric-Space x)
+
+  abstract
+    is-short-map-short-function-metric-quotient-Pseudometric-Space :
+      is-short-function-Metric-Space
+        ( metric-quotient-Pseudometric-Space A)
+        ( B)
+        ( map-short-function-metric-quotient-Pseudometric-space)
+    is-short-map-short-function-metric-quotient-Pseudometric-Space
+      d X Y N⟨X,Y⟩ =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( neighborhood-prop-Metric-Space
+              ( B)
+              ( d)
+              ( map-short-function-metric-quotient-Pseudometric-space X)
+              ( map-short-function-metric-quotient-Pseudometric-space Y))
+        in do
+          ( x , x∈X) ←
+            is-inhabited-subtype-set-quotient
+              ( equivalence-relation-sim-Pseudometric-Space A)
+              ( X)
+          ( y , y∈Y) ←
+            is-inhabited-subtype-set-quotient
+              ( equivalence-relation-sim-Pseudometric-Space A)
+              ( Y)
+
+          binary-tr
+            ( neighborhood-Metric-Space B d)
+            ( inv
+              ( compute-map-short-function-metric-quotient-Pseudometric-Space
+                ( X)
+                ( x)
+                ( x∈X)))
+            ( inv
+              ( compute-map-short-function-metric-quotient-Pseudometric-Space
+                ( Y)
+                ( y)
+                ( y∈Y)))
+            ( is-short-map-short-function-Pseudometric-Space
+              ( A)
+              ( pseudometric-Metric-Space B)
+              ( f)
+              ( d)
+              ( x)
+              ( y)
+              ( N⟨X,Y⟩ (x , x∈X) (y , y∈Y)))
+
+  short-map-short-function-metric-quotient-Pseudometric-Space :
+    short-function-Metric-Space
+      ( metric-quotient-Pseudometric-Space A)
+      ( B)
+  short-map-short-function-metric-quotient-Pseudometric-Space =
+    ( map-short-function-metric-quotient-Pseudometric-space ,
+      is-short-map-short-function-metric-quotient-Pseudometric-Space)
+```
+
+### Induced isometry from the quotient metric space into a metric space
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2)
+  (B : Metric-Space l1' l2')
+  (f : isometry-Pseudometric-Space A (pseudometric-Metric-Space B))
+  where
+
+  map-isometry-metric-quotient-Pseudometric-Space :
+    type-function-Metric-Space
+      ( metric-quotient-Pseudometric-Space A)
+      ( B)
+  map-isometry-metric-quotient-Pseudometric-Space =
+    map-short-function-metric-quotient-Pseudometric-space
+      ( A)
+      ( B)
+      ( short-isometry-Pseudometric-Space
+        ( A)
+        ( pseudometric-Metric-Space B)
+        ( f))
+
+  htpy-map-isometry-metric-quotient-Pseudometric-Space :
+    ( ( map-isometry-metric-quotient-Pseudometric-Space) ∘
+      ( map-metric-quotient-Pseudometric-Space A)) ~
+    ( map-isometry-Pseudometric-Space A (pseudometric-Metric-Space B) f)
+  htpy-map-isometry-metric-quotient-Pseudometric-Space =
+    htpy-map-short-function-metric-quotient-Pseudometric-Space
+      ( A)
+      ( B)
+      ( short-isometry-Pseudometric-Space
+        ( A)
+        ( pseudometric-Metric-Space B)
+        ( f))
+
+  compute-map-isometry-metric-quotient-Pseudometric-Space :
+    (X : type-metric-quotient-Pseudometric-Space A) →
+    (x : type-Pseudometric-Space A) →
+    is-in-class-metric-quotient-Pseudometric-Space A X x →
+    map-isometry-metric-quotient-Pseudometric-Space X ＝
+    map-isometry-Pseudometric-Space
+      ( A)
+      ( pseudometric-Metric-Space B)
+      ( f)
+      ( x)
+  compute-map-isometry-metric-quotient-Pseudometric-Space =
+    compute-map-short-function-metric-quotient-Pseudometric-Space
+      ( A)
+      ( B)
+      ( short-isometry-Pseudometric-Space
+        ( A)
+        ( pseudometric-Metric-Space B)
+        ( f))
+
+  abstract
+    preserves-neighborhood-map-isometry-metric-quotient-Pseudometric-Space :
+      (d : ℚ⁺) →
+      (x y : type-metric-quotient-Pseudometric-Space A) →
+      neighborhood-metric-quotient-Pseudometric-Space
+        ( A)
+        ( d)
+        ( x)
+        ( y) →
+      neighborhood-Metric-Space
+        ( B)
+        ( d)
+        ( map-isometry-metric-quotient-Pseudometric-Space x)
+        ( map-isometry-metric-quotient-Pseudometric-Space y)
+    preserves-neighborhood-map-isometry-metric-quotient-Pseudometric-Space =
+      is-short-map-short-function-metric-quotient-Pseudometric-Space
+        ( A)
+        ( B)
+        ( short-isometry-Pseudometric-Space
+          ( A)
+          ( pseudometric-Metric-Space B)
+          ( f))
+
+    reflects-neighborhood-map-isometry-metric-quotient-Pseudometric-Space :
+      (d : ℚ⁺) →
+      (x y : type-metric-quotient-Pseudometric-Space A) →
+      neighborhood-Metric-Space
+        ( B)
+        ( d)
+        ( map-isometry-metric-quotient-Pseudometric-Space x)
+        ( map-isometry-metric-quotient-Pseudometric-Space y) →
+      neighborhood-metric-quotient-Pseudometric-Space
+        ( A)
+        ( d)
+        ( x)
+        ( y)
+    reflects-neighborhood-map-isometry-metric-quotient-Pseudometric-Space
+      d X Y N⟨fX,fY⟩ (x , x∈X) (y , y∈Y) =
+      reflects-neighborhood-map-isometry-Pseudometric-Space
+        ( A)
+        ( pseudometric-Metric-Space B)
+        ( f)
+        ( d)
+        ( x)
+        ( y)
+        ( binary-tr
+          ( neighborhood-Metric-Space B d)
+          ( compute-map-isometry-metric-quotient-Pseudometric-Space X x x∈X)
+          ( compute-map-isometry-metric-quotient-Pseudometric-Space Y y y∈Y)
+          ( N⟨fX,fY⟩))
+
+    is-isometry-map-isometry-metric-quotient-Pseudometric-Space :
+      is-isometry-Metric-Space
+        ( metric-quotient-Pseudometric-Space A)
+        ( B)
+        ( map-isometry-metric-quotient-Pseudometric-Space)
+    is-isometry-map-isometry-metric-quotient-Pseudometric-Space d x y =
+      ( preserves-neighborhood-map-isometry-metric-quotient-Pseudometric-Space
+        ( d)
+        ( x)
+        ( y) ,
+        reflects-neighborhood-map-isometry-metric-quotient-Pseudometric-Space
+          ( d)
+          ( x)
+          ( y))
+
+  isometry-map-isometry-metric-quotient-Pseudometric-Space :
+    isometry-Metric-Space
+      ( metric-quotient-Pseudometric-Space A)
+      ( B)
+  isometry-map-isometry-metric-quotient-Pseudometric-Space =
+    ( map-isometry-metric-quotient-Pseudometric-Space ,
+      is-isometry-map-isometry-metric-quotient-Pseudometric-Space)
+```
+
+## External links
+
+- [Metric identification](https://en.wikipedia.org/wiki/Pseudometric_space#Metric_identification)
+  on pseudometric spaces at Wikipedia
diff --git a/src/metric-spaces/metric-spaces.lagda.md b/src/metric-spaces/metric-spaces.lagda.md
index c507203765..25fbe2e982 100644
--- a/src/metric-spaces/metric-spaces.lagda.md
+++ b/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
diff --git a/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md b/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md
index 564a2b9385..6d3251395d 100644
--- a/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md
+++ b/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md
@@ -232,6 +232,7 @@ 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
@@ -239,6 +240,13 @@ module _
     ( 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
diff --git a/src/metric-spaces/pseudometric-completion-of-metric-spaces.lagda.md b/src/metric-spaces/pseudometric-completion-of-metric-spaces.lagda.md
new file mode 100644
index 0000000000..57328439f2
--- /dev/null
+++ b/src/metric-spaces/pseudometric-completion-of-metric-spaces.lagda.md
@@ -0,0 +1,437 @@
+# The pseudometric completion of a metric space
+
+```agda
+module metric-spaces.pseudometric-completion-of-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+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-completion-of-pseudometric-spaces
+open import metric-spaces.pseudometric-spaces
+open import metric-spaces.rational-neighborhood-relations
+open import metric-spaces.short-functions-pseudometric-spaces
+open import metric-spaces.similarity-of-elements-pseudometric-spaces
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "pseudometric completion" Disambiguation="of a metric space" Agda=pseudometric-completion-Metric-Space}}
+of a [metric space](metric-spaces.metric-spaces.md) `M` is the
+[pseudometric completion](metric-spaces.pseudometric-completion-of-pseudometric-spaces.md)
+of its underlying [pseudometric space](metric-spaces.pseudometric-spaces.md):
+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).
+If the metric space is [complete](metric-spaces.complete-metric-spaces.md), it
+is a [retract](foundation.retracts-of-types.md) of its pseudometric completion.
+
+## Definition
+
+### The pseudometric completion of a metric space
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+  pseudometric-completion-Metric-Space :
+    Pseudometric-Space (l1 ⊔ l2) l2
+  pseudometric-completion-Metric-Space =
+    pseudometric-completion-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+```
+
+### The pseudometric completion neighborhood relation on the type of Cauchy approximations in a pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+  neighborhood-prop-pseudometric-completion-Metric-Space :
+    Rational-Neighborhood-Relation l2
+      (cauchy-approximation-Metric-Space M)
+  neighborhood-prop-pseudometric-completion-Metric-Space =
+    neighborhood-prop-pseudometric-completion-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+
+  neighborhood-pseudometric-completion-Metric-Space :
+    ℚ⁺ → Relation l2 (cauchy-approximation-Metric-Space M)
+  neighborhood-pseudometric-completion-Metric-Space =
+    neighborhood-pseudometric-completion-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+```
+
+## Properties
+
+### The neighborhood relation is reflexive
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+  abstract
+    is-reflexive-neighborhood-pseudometric-completion-Metric-Space :
+      (d : ℚ⁺) (x : cauchy-approximation-Metric-Space M) →
+      neighborhood-pseudometric-completion-Metric-Space M d x x
+    is-reflexive-neighborhood-pseudometric-completion-Metric-Space =
+      is-reflexive-neighborhood-pseudometric-completion-Pseudometric-Space
+        ( pseudometric-Metric-Space M)
+```
+
+### The neighborhood relation is symmetric
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+    abstract
+      is-symmetric-neighborhood-pseudometric-completion-Metric-Space :
+        (d : ℚ⁺) (x y : cauchy-approximation-Metric-Space M) →
+        neighborhood-pseudometric-completion-Metric-Space M d x y →
+        neighborhood-pseudometric-completion-Metric-Space M d y x
+      is-symmetric-neighborhood-pseudometric-completion-Metric-Space =
+        is-symmetric-neighborhood-pseudometric-completion-Pseudometric-Space
+          ( pseudometric-Metric-Space M)
+```
+
+### The neighborhood relation is triangular
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+  abstract
+    is-triangular-neighborhood-pseudometric-completion-Metric-Space :
+      (x y z : cauchy-approximation-Metric-Space M) →
+      (dxy dyz : ℚ⁺) →
+      neighborhood-pseudometric-completion-Metric-Space M dyz y z →
+      neighborhood-pseudometric-completion-Metric-Space M dxy x y →
+      neighborhood-pseudometric-completion-Metric-Space
+        ( M)
+        ( dxy +ℚ⁺ dyz)
+        ( x)
+        ( z)
+    is-triangular-neighborhood-pseudometric-completion-Metric-Space =
+      is-triangular-neighborhood-pseudometric-completion-Pseudometric-Space
+        ( pseudometric-Metric-Space M)
+```
+
+### The neighborhood relation is saturated
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+  abstract
+    is-saturated-neighborhood-pseudometric-completion-Metric-Space :
+      ( ε : ℚ⁺) (x y : cauchy-approximation-Metric-Space M) →
+      ( (δ : ℚ⁺) →
+        neighborhood-pseudometric-completion-Metric-Space
+          ( M)
+          ( ε +ℚ⁺ δ)
+          ( x)
+          ( y)) →
+      neighborhood-pseudometric-completion-Metric-Space M ε x y
+    is-saturated-neighborhood-pseudometric-completion-Metric-Space =
+      is-saturated-neighborhood-pseudometric-completion-Pseudometric-Space
+        ( pseudometric-Metric-Space M)
+```
+
+### The isometry from a metric space to its pseudometric completion
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+  isometry-pseudometric-completion-Metric-Space :
+    isometry-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+      ( pseudometric-completion-Metric-Space M)
+  isometry-pseudometric-completion-Metric-Space =
+    isometry-pseudometric-completion-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+
+  map-pseudometric-completion-Metric-Space :
+    type-Metric-Space M → cauchy-approximation-Metric-Space M
+  map-pseudometric-completion-Metric-Space =
+    map-isometry-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+      ( pseudometric-completion-Metric-Space M)
+      ( isometry-pseudometric-completion-Metric-Space)
+
+  abstract
+    is-isometry-map-pseudometric-completion-Metric-Space :
+      is-isometry-Pseudometric-Space
+        ( pseudometric-Metric-Space M)
+        ( pseudometric-completion-Metric-Space M)
+        ( map-pseudometric-completion-Metric-Space)
+    is-isometry-map-pseudometric-completion-Metric-Space =
+      is-isometry-map-isometry-Pseudometric-Space
+        ( pseudometric-Metric-Space M)
+        ( pseudometric-completion-Metric-Space M)
+        ( isometry-pseudometric-completion-Metric-Space)
+```
+
+### Convergent Cauchy approximations are similar to constant Cauchy approximations in the pseudometric completion
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  (u : cauchy-approximation-Metric-Space M)
+  (x : type-Metric-Space M)
+  where
+
+  abstract
+    sim-const-is-limit-cauchy-approximation-Metric-Space :
+      is-limit-cauchy-approximation-Metric-Space M u x →
+      sim-Pseudometric-Space
+        ( pseudometric-completion-Metric-Space M)
+        ( u)
+        ( const-cauchy-approximation-Metric-Space M x)
+    sim-const-is-limit-cauchy-approximation-Metric-Space H d α β =
+      monotonic-neighborhood-Metric-Space
+        ( M)
+        ( map-cauchy-approximation-Metric-Space M u α)
+        ( x)
+        ( α +ℚ⁺ β)
+        ( α +ℚ⁺ β +ℚ⁺ d)
+        ( le-left-add-ℚ⁺ (α +ℚ⁺ β) d)
+        ( H α β)
+
+    is-limit-sim-const-cauchy-approximation-Metric-Space :
+      sim-Pseudometric-Space
+        ( pseudometric-completion-Metric-Space M)
+        ( u)
+        ( const-cauchy-approximation-Metric-Space M x) →
+      is-limit-cauchy-approximation-Metric-Space M u x
+    is-limit-sim-const-cauchy-approximation-Metric-Space H α β =
+      saturated-neighborhood-Metric-Space
+        ( M)
+        ( α +ℚ⁺ β)
+        ( map-cauchy-approximation-Metric-Space M u α)
+        ( x)
+        ( λ d → H d α β)
+```
+
+### Any Cauchy approximation in the pseudometric completion of a metric space has a limit
+
+```agda
+module _
+  { l1 l2 : Level} (M : Metric-Space l1 l2)
+  ( U :
+    cauchy-approximation-Pseudometric-Space
+      ( pseudometric-completion-Metric-Space M))
+  where
+
+  has-limit-cauchy-approximation-pseudometric-completion-Metric-Space :
+    Σ ( cauchy-approximation-Metric-Space M)
+      ( is-limit-cauchy-approximation-Pseudometric-Space
+        ( pseudometric-completion-Metric-Space M)
+        ( U))
+  has-limit-cauchy-approximation-pseudometric-completion-Metric-Space =
+    has-limit-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+      ( U)
+
+  lim-cauchy-approximation-pseudometric-completion-Metric-Space :
+    cauchy-approximation-Metric-Space M
+  lim-cauchy-approximation-pseudometric-completion-Metric-Space =
+    pr1 has-limit-cauchy-approximation-pseudometric-completion-Metric-Space
+
+  is-limit-lim-cauchy-approximation-pseudometric-completion-Metric-Space :
+    is-limit-cauchy-approximation-Pseudometric-Space
+      ( pseudometric-completion-Metric-Space M)
+      ( U)
+      ( lim-cauchy-approximation-pseudometric-completion-Metric-Space)
+  is-limit-lim-cauchy-approximation-pseudometric-completion-Metric-Space =
+    pr2 has-limit-cauchy-approximation-pseudometric-completion-Metric-Space
+```
+
+### The isometry from a Cauchy approximation in the pseudometric completion to its limit
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+  isometry-lim-cauchy-approximation-pseudometric-completion-Metric-Space :
+    isometry-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space
+        ( pseudometric-completion-Metric-Space M))
+      ( pseudometric-completion-Metric-Space M)
+  isometry-lim-cauchy-approximation-pseudometric-completion-Metric-Space =
+    isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+```
+
+### Any complete metric space is a short retract of its pseudometric completion
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  (is-complete-M : is-complete-Metric-Space M)
+  where
+
+  map-lim-pseudometric-completion-is-complete-Metric-Space :
+    type-function-Pseudometric-Space
+      ( pseudometric-completion-Metric-Space M)
+      ( pseudometric-Metric-Space M)
+  map-lim-pseudometric-completion-is-complete-Metric-Space =
+    limit-cauchy-approximation-Complete-Metric-Space
+      ( M , is-complete-M)
+
+  is-limit-map-lim-pseudometric-completion-is-complete-Metric-Space :
+    (u : cauchy-approximation-Metric-Space M) →
+    is-limit-cauchy-approximation-Metric-Space
+      ( M)
+      ( u)
+      ( map-lim-pseudometric-completion-is-complete-Metric-Space u)
+  is-limit-map-lim-pseudometric-completion-is-complete-Metric-Space =
+    is-limit-limit-cauchy-approximation-Complete-Metric-Space
+      ( M , is-complete-M)
+
+  sim-const-map-lim-pseudometric-completion-is-complete-Metric-Space :
+    (u : cauchy-approximation-Metric-Space M) →
+    sim-Pseudometric-Space
+      ( pseudometric-completion-Metric-Space M)
+      ( u)
+      ( const-cauchy-approximation-Metric-Space
+        ( M)
+        ( map-lim-pseudometric-completion-is-complete-Metric-Space u))
+  sim-const-map-lim-pseudometric-completion-is-complete-Metric-Space u =
+    sim-const-is-limit-cauchy-approximation-Metric-Space
+      ( M)
+      ( u)
+      ( map-lim-pseudometric-completion-is-complete-Metric-Space u)
+      ( is-limit-map-lim-pseudometric-completion-is-complete-Metric-Space u)
+
+  is-short-map-lim-pseudometric-completion-is-complete-Metric-Space :
+    is-short-function-Pseudometric-Space
+      ( pseudometric-completion-Metric-Space M)
+      ( pseudometric-Metric-Space M)
+      ( map-lim-pseudometric-completion-is-complete-Metric-Space)
+  is-short-map-lim-pseudometric-completion-is-complete-Metric-Space d x y Nxy =
+    saturated-neighborhood-Metric-Space
+      ( M)
+      ( d)
+      ( map-lim-pseudometric-completion-is-complete-Metric-Space x)
+      ( map-lim-pseudometric-completion-is-complete-Metric-Space y)
+      ( lemma-saturated-neighborhood-map-lim)
+    where
+
+      neighborhood-const-lim-x-y :
+        neighborhood-Pseudometric-Space
+          ( pseudometric-completion-Metric-Space M)
+          ( d)
+          ( const-cauchy-approximation-Metric-Space M
+            ( map-lim-pseudometric-completion-is-complete-Metric-Space x))
+          ( const-cauchy-approximation-Metric-Space M
+            ( map-lim-pseudometric-completion-is-complete-Metric-Space y))
+      neighborhood-const-lim-x-y =
+        preserves-neighborhood-sim-Pseudometric-Space
+          ( pseudometric-completion-Metric-Space M)
+          { x}
+          { const-cauchy-approximation-Metric-Space
+            ( M)
+            ( map-lim-pseudometric-completion-is-complete-Metric-Space x)}
+          { y}
+          { const-cauchy-approximation-Metric-Space
+            ( M)
+            ( map-lim-pseudometric-completion-is-complete-Metric-Space y)}
+          ( sim-const-map-lim-pseudometric-completion-is-complete-Metric-Space
+            ( x))
+          ( sim-const-map-lim-pseudometric-completion-is-complete-Metric-Space
+            ( y))
+          ( d)
+          ( Nxy)
+
+      lemma-saturated-neighborhood-map-lim :
+        (δ : ℚ⁺) →
+        neighborhood-Metric-Space
+          ( M)
+          ( d +ℚ⁺ δ)
+          ( map-lim-pseudometric-completion-is-complete-Metric-Space x)
+          ( map-lim-pseudometric-completion-is-complete-Metric-Space y)
+      lemma-saturated-neighborhood-map-lim δ =
+        tr
+          ( is-upper-bound-dist-Metric-Space
+            ( M)
+            ( map-lim-pseudometric-completion-is-complete-Metric-Space x)
+            ( map-lim-pseudometric-completion-is-complete-Metric-Space y))
+          ( ap (add-ℚ⁺' d) (eq-add-split-ℚ⁺ δ) ∙ commutative-add-ℚ⁺ δ d)
+          ( neighborhood-const-lim-x-y
+            ( left-summand-split-ℚ⁺ δ)
+            ( right-summand-split-ℚ⁺ δ))
+
+  short-map-lim-pseudometric-completion-is-complete-Metric-Space :
+    short-function-Pseudometric-Space
+      ( pseudometric-completion-Metric-Space M)
+      ( pseudometric-Metric-Space M)
+  short-map-lim-pseudometric-completion-is-complete-Metric-Space =
+    ( map-lim-pseudometric-completion-is-complete-Metric-Space ,
+      is-short-map-lim-pseudometric-completion-is-complete-Metric-Space)
+
+  is-retraction-map-pseudometric-completion-is-complete-Metric-Space :
+    ( map-lim-pseudometric-completion-is-complete-Metric-Space ∘
+      map-pseudometric-completion-Metric-Space M) ~
+    ( id)
+  is-retraction-map-pseudometric-completion-is-complete-Metric-Space =
+    is-retraction-limit-cauchy-approximation-Complete-Metric-Space
+      ( M , is-complete-M)
+
+  sim-map-lim-pseudometric-completion-is-complete-Metric-Space :
+    (u : cauchy-approximation-Metric-Space M) →
+    sim-Pseudometric-Space
+      ( pseudometric-completion-Metric-Space M)
+      ( u)
+      ( map-pseudometric-completion-Metric-Space
+        ( M)
+        ( map-lim-pseudometric-completion-is-complete-Metric-Space u))
+  sim-map-lim-pseudometric-completion-is-complete-Metric-Space u =
+    sim-const-is-limit-cauchy-approximation-Metric-Space
+      ( M)
+      ( u)
+      ( map-lim-pseudometric-completion-is-complete-Metric-Space u)
+      ( is-limit-map-lim-pseudometric-completion-is-complete-Metric-Space 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..e7489c92e2
--- /dev/null
+++ b/src/metric-spaces/pseudometric-completion-of-pseudometric-spaces.lagda.md
@@ -0,0 +1,766 @@
+# The pseudometric completion of a pseudometric space
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module metric-spaces.pseudometric-completion-of-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.strict-inequality-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
+open import metric-spaces.similarity-of-elements-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)
+
+  short-map-pseudometric-completion-Pseudometric-Space :
+    short-function-Pseudometric-Space
+      ( M)
+      ( pseudometric-completion-Pseudometric-Space M)
+  short-map-pseudometric-completion-Pseudometric-Space =
+    short-isometry-Pseudometric-Space
+      ( M)
+      ( pseudometric-completion-Pseudometric-Space M)
+      ( isometry-pseudometric-completion-Pseudometric-Space)
+```
+
+### Convergent Cauchy approximations are similar to constant Cauchy approximations in the pseudometric completion
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  (u : cauchy-approximation-Pseudometric-Space M)
+  (x : type-Pseudometric-Space M)
+  where
+
+  abstract
+    sim-const-is-limit-cauchy-approximation-Pseudometric-Space :
+      is-limit-cauchy-approximation-Pseudometric-Space M u x →
+      sim-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space M)
+        ( u)
+        ( const-cauchy-approximation-Pseudometric-Space M x)
+    sim-const-is-limit-cauchy-approximation-Pseudometric-Space H d α β =
+      monotonic-neighborhood-Pseudometric-Space
+        ( M)
+        ( map-cauchy-approximation-Pseudometric-Space M u α)
+        ( x)
+        ( α +ℚ⁺ β)
+        ( α +ℚ⁺ β +ℚ⁺ d)
+        ( le-left-add-ℚ⁺ (α +ℚ⁺ β) d)
+        ( H α β)
+
+    is-limit-sim-const-cauchy-approximation-Pseudometric-Space :
+      sim-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space M)
+        ( u)
+        ( const-cauchy-approximation-Pseudometric-Space M x) →
+      is-limit-cauchy-approximation-Pseudometric-Space M u x
+    is-limit-sim-const-cauchy-approximation-Pseudometric-Space H α β =
+      saturated-neighborhood-Pseudometric-Space
+        ( M)
+        ( α +ℚ⁺ β)
+        ( map-cauchy-approximation-Pseudometric-Space M u α)
+        ( x)
+        ( λ d → H d α β)
+```
+
+### 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)
+```
+
+### The map from a Cauchy approximation in the pseudometric completion to its limit is an isometry
+
+```agda
+module _
+  { l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  ( d : ℚ⁺)
+  ( u v :
+    cauchy-approximation-Pseudometric-Space
+    ( pseudometric-completion-Pseudometric-Space M))
+  where
+
+  abstract
+    preserves-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space :
+      neighborhood-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space M))
+        ( d)
+        ( u)
+        ( v) →
+      neighborhood-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space M)
+        ( d)
+        ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+          ( M)
+          ( u))
+        ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+          ( M)
+          ( v))
+    preserves-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+      Nuv =
+      let
+        neighborhood-const-lim :
+          neighborhood-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space M))
+            ( d)
+            ( const-cauchy-approximation-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space M)
+              ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                ( M)
+                ( u)))
+            ( const-cauchy-approximation-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space M)
+              ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                ( M)
+                ( v)))
+        neighborhood-const-lim =
+          preserves-neighborhood-sim-Pseudometric-Space
+            ( pseudometric-completion-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space M))
+            { u}
+            { const-cauchy-approximation-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space M)
+              ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                ( M)
+                ( u))}
+            { v}
+            { const-cauchy-approximation-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space M)
+              ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                ( M)
+                ( v))}
+            ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space M)
+              ( u)
+              ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                ( M)
+                ( u))
+              ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                ( M)
+                ( u)))
+            ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+              ( pseudometric-completion-Pseudometric-Space M)
+              ( v)
+              ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                ( M)
+                ( v))
+              ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+                ( M)
+                ( v)))
+            ( d)
+            ( Nuv)
+      in
+        reflects-neighborhood-map-pseudometric-completion-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space M)
+          ( d)
+          ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( M)
+            ( u))
+          ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( M)
+            ( v))
+          ( neighborhood-const-lim)
+
+    reflects-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space :
+      neighborhood-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space M)
+        ( d)
+        ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+          ( M)
+          ( u))
+        ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+          ( M)
+          ( v)) →
+      neighborhood-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space M))
+        ( d)
+        ( u)
+        ( v)
+    reflects-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+      N-lim =
+      reflects-neighborhood-sim-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space M))
+        { u}
+        { const-cauchy-approximation-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space M)
+          ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( M)
+            ( u))}
+        { v}
+        { const-cauchy-approximation-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space M)
+          ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( M)
+            ( v))}
+        ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space M)
+            ( u)
+            ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+              ( M)
+              ( u))
+            ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+              ( M)
+              ( u)))
+        ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space M)
+            ( v)
+            ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+              ( M)
+              ( v))
+            ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+              ( M)
+              ( v)))
+        ( d)
+        ( preserves-neighborhood-map-pseudometric-completion-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space M)
+          ( d)
+          ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( M)
+            ( u))
+          ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+            ( M)
+            ( v))
+          ( N-lim))
+
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    is-isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space :
+      is-isometry-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space
+          ( pseudometric-completion-Pseudometric-Space M))
+        ( pseudometric-completion-Pseudometric-Space M)
+        ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space M)
+    is-isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+      d x y =
+      ( ( preserves-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+          ( M)
+          ( d)
+          ( x)
+          ( y)) ,
+        ( reflects-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space
+          ( M)
+          ( d)
+          ( x)
+          ( y)))
+
+  isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( pseudometric-completion-Pseudometric-Space
+        ( pseudometric-completion-Pseudometric-Space M))
+      ( pseudometric-completion-Pseudometric-Space M)
+  isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space =
+    ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space M ,
+      is-isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space)
+```
diff --git a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md
index 289635cb19..763b86217f 100644
--- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md
+++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md
@@ -24,6 +24,7 @@ open import foundation.universe-levels
 
 open import metric-spaces.pseudometric-spaces
 open import metric-spaces.rational-neighborhood-relations
+open import metric-spaces.short-functions-pseudometric-spaces
 ```
 
 </details>
@@ -170,54 +171,98 @@ module _
   {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
   where
 
-  preserves-neighborhood-sim-Pseudometric-Space :
-    { x y : type-Pseudometric-Space A} →
-    ( sim-Pseudometric-Space A x y) →
-    ( d : ℚ⁺) (z : type-Pseudometric-Space A) →
-    neighborhood-Pseudometric-Space A d x z →
-    neighborhood-Pseudometric-Space A d y z
-  preserves-neighborhood-sim-Pseudometric-Space {x} {y} x≍y d z Nxz =
-    saturated-neighborhood-Pseudometric-Space
-      ( A)
-      ( d)
-      ( y)
-      ( z)
-      ( λ δ →
-        tr
-          ( is-upper-bound-dist-Pseudometric-Space A y z)
-          ( commutative-add-ℚ⁺ δ d)
-          ( triangular-neighborhood-Pseudometric-Space
-            ( A)
-            ( y)
-            ( x)
-            ( z)
-            ( δ)
-            ( d)
-            ( Nxz)
-            ( symmetric-neighborhood-Pseudometric-Space
+  abstract
+    preserves-neighborhood-left-sim-Pseudometric-Space :
+      { x y : type-Pseudometric-Space A} →
+      ( sim-Pseudometric-Space A x y) →
+      ( d : ℚ⁺) (z : type-Pseudometric-Space A) →
+      neighborhood-Pseudometric-Space A d x z →
+      neighborhood-Pseudometric-Space A d y z
+    preserves-neighborhood-left-sim-Pseudometric-Space {x} {y} x≍y d z Nxz =
+      saturated-neighborhood-Pseudometric-Space
+        ( A)
+        ( d)
+        ( y)
+        ( z)
+        ( λ δ →
+          tr
+            ( is-upper-bound-dist-Pseudometric-Space A y z)
+            ( commutative-add-ℚ⁺ δ d)
+            ( triangular-neighborhood-Pseudometric-Space
               ( A)
-              ( δ)
-              ( x)
               ( y)
-              ( x≍y δ))))
-
-  iff-same-neighbors-sim-Pseudometric-Space :
-    { x y : type-Pseudometric-Space A} →
-    ( sim-Pseudometric-Space A x y) ↔
-    ( (d : ℚ⁺) (z : type-Pseudometric-Space A) →
-      neighborhood-Pseudometric-Space A d x z ↔
-      neighborhood-Pseudometric-Space A d y z)
-  iff-same-neighbors-sim-Pseudometric-Space =
-    ( λ x≍y d z →
-      ( preserves-neighborhood-sim-Pseudometric-Space x≍y d z) ,
-      ( preserves-neighborhood-sim-Pseudometric-Space
-        ( inv-sim-Pseudometric-Space A x≍y)
+              ( x)
+              ( z)
+              ( δ)
+              ( d)
+              ( Nxz)
+              ( symmetric-neighborhood-Pseudometric-Space
+                ( A)
+                ( δ)
+                ( x)
+                ( y)
+                ( x≍y δ))))
+
+    preserves-neighborhood-right-sim-Pseudometric-Space :
+      { x y : type-Pseudometric-Space A} →
+      ( sim-Pseudometric-Space A x y) →
+      ( d : ℚ⁺) (z : type-Pseudometric-Space A) →
+      neighborhood-Pseudometric-Space A d z x →
+      neighborhood-Pseudometric-Space A d z y
+    preserves-neighborhood-right-sim-Pseudometric-Space {x} {y} x≍y d z Nzx =
+      symmetric-neighborhood-Pseudometric-Space A d y z
+        ( preserves-neighborhood-left-sim-Pseudometric-Space x≍y d z
+          ( symmetric-neighborhood-Pseudometric-Space A d z x Nzx))
+
+    preserves-neighborhood-sim-Pseudometric-Space :
+      {x x' y y' : type-Pseudometric-Space A} →
+      sim-Pseudometric-Space A x x' →
+      sim-Pseudometric-Space A y y' →
+      (d : ℚ⁺) →
+      neighborhood-Pseudometric-Space A d x y →
+      neighborhood-Pseudometric-Space A d x' y'
+    preserves-neighborhood-sim-Pseudometric-Space
+      {x} {x'} {y} {y'} x~x' y~y' d Nxy =
+      preserves-neighborhood-left-sim-Pseudometric-Space
+        ( x~x')
         ( d)
-        ( z))) ,
-    ( λ same-neighbors d →
-      backward-implication
-        ( same-neighbors d _)
-        ( refl-sim-Pseudometric-Space A _ d))
+        ( y')
+        ( preserves-neighborhood-right-sim-Pseudometric-Space
+          ( y~y')
+          ( d)
+          ( x)
+          ( Nxy))
+
+    reflects-neighborhood-sim-Pseudometric-Space :
+      {x x' y y' : type-Pseudometric-Space A} →
+      sim-Pseudometric-Space A x x' →
+      sim-Pseudometric-Space A y y' →
+      (d : ℚ⁺) →
+      neighborhood-Pseudometric-Space A d x' y' →
+      neighborhood-Pseudometric-Space A d x y
+    reflects-neighborhood-sim-Pseudometric-Space
+      {x} {x'} {y} {y'} x~x' y~y' =
+      preserves-neighborhood-sim-Pseudometric-Space
+        ( inv-sim-Pseudometric-Space A x~x')
+        ( inv-sim-Pseudometric-Space A y~y')
+
+    iff-same-neighbors-sim-Pseudometric-Space :
+      { x y : type-Pseudometric-Space A} →
+      ( sim-Pseudometric-Space A x y) ↔
+      ( (d : ℚ⁺) (z : type-Pseudometric-Space A) →
+        neighborhood-Pseudometric-Space A d x z ↔
+        neighborhood-Pseudometric-Space A d y z)
+    iff-same-neighbors-sim-Pseudometric-Space =
+      ( λ x≍y d z →
+        ( preserves-neighborhood-left-sim-Pseudometric-Space x≍y d z) ,
+        ( preserves-neighborhood-left-sim-Pseudometric-Space
+          ( inv-sim-Pseudometric-Space A x≍y)
+          ( d)
+          ( z))) ,
+      ( λ same-neighbors d →
+        backward-implication
+          ( same-neighbors d _)
+          ( refl-sim-Pseudometric-Space A _ d))
 ```
 
 ### Similar elements are elements similar w.r.t the underlying rational neighborhood relation
@@ -227,35 +272,57 @@ module _
   {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
   where
 
-  iff-same-neighbors-same-neighborhood-Pseudometric-Space :
-    {x y : type-Pseudometric-Space A} →
-    ( (d : ℚ⁺) (z : type-Pseudometric-Space A) →
-      neighborhood-Pseudometric-Space A d x z ↔
-      neighborhood-Pseudometric-Space A d y z) ↔
-    ( sim-Rational-Neighborhood-Relation
-      ( neighborhood-prop-Pseudometric-Space A)
-      ( x)
-      ( y))
-  iff-same-neighbors-same-neighborhood-Pseudometric-Space =
-    ( λ H d z →
-      ( H d z) ,
-      ( inv-neighborhood-Pseudometric-Space A ∘
-        pr1 (H d z) ∘
-        inv-neighborhood-Pseudometric-Space A) ,
-      ( inv-neighborhood-Pseudometric-Space A ∘
-        pr2 (H d z) ∘
-        inv-neighborhood-Pseudometric-Space A)) ,
-    ( iff-left-neighbor-sim-Rational-Neighborhood-Relation
-      ( neighborhood-prop-Pseudometric-Space A))
-
-  iff-same-neighborhood-sim-Pseudometric-Space :
-    { x y : type-Pseudometric-Space A} →
-    ( sim-Pseudometric-Space A x y) ↔
-    ( sim-Rational-Neighborhood-Relation
-      ( neighborhood-prop-Pseudometric-Space A)
-      ( x)
-      ( y))
-  iff-same-neighborhood-sim-Pseudometric-Space =
-    ( iff-same-neighbors-same-neighborhood-Pseudometric-Space) ∘iff
-    ( iff-same-neighbors-sim-Pseudometric-Space A)
+  abstract
+    iff-same-neighbors-same-neighborhood-Pseudometric-Space :
+      {x y : type-Pseudometric-Space A} →
+      ( (d : ℚ⁺) (z : type-Pseudometric-Space A) →
+        neighborhood-Pseudometric-Space A d x z ↔
+        neighborhood-Pseudometric-Space A d y z) ↔
+      ( sim-Rational-Neighborhood-Relation
+        ( neighborhood-prop-Pseudometric-Space A)
+        ( x)
+        ( y))
+    iff-same-neighbors-same-neighborhood-Pseudometric-Space =
+      ( λ H d z →
+        ( H d z) ,
+        ( inv-neighborhood-Pseudometric-Space A ∘
+          pr1 (H d z) ∘
+          inv-neighborhood-Pseudometric-Space A) ,
+        ( inv-neighborhood-Pseudometric-Space A ∘
+          pr2 (H d z) ∘
+          inv-neighborhood-Pseudometric-Space A)) ,
+      ( iff-left-neighbor-sim-Rational-Neighborhood-Relation
+        ( neighborhood-prop-Pseudometric-Space A))
+
+    iff-same-neighborhood-sim-Pseudometric-Space :
+      { x y : type-Pseudometric-Space A} →
+      ( sim-Pseudometric-Space A x y) ↔
+      ( sim-Rational-Neighborhood-Relation
+        ( neighborhood-prop-Pseudometric-Space A)
+        ( x)
+        ( y))
+    iff-same-neighborhood-sim-Pseudometric-Space =
+      ( iff-same-neighbors-same-neighborhood-Pseudometric-Space) ∘iff
+      ( iff-same-neighbors-sim-Pseudometric-Space A)
+```
+
+### Short maps between pseudometric spaces preserves similarity
+
+```agda
+module _
+  { l1 l2 l1' l2' : Level}
+  ( A : Pseudometric-Space l1 l2)
+  ( B : Pseudometric-Space l1' l2')
+  ( f : short-function-Pseudometric-Space A B)
+  where
+
+  abstract
+    preserves-sim-map-short-function-Pseudometric-Space :
+      ( x y : type-Pseudometric-Space A) →
+      ( sim-Pseudometric-Space A x y) →
+      ( sim-Pseudometric-Space B
+        ( map-short-function-Pseudometric-Space A B f x)
+        ( map-short-function-Pseudometric-Space A B f y))
+    preserves-sim-map-short-function-Pseudometric-Space x y x~y d =
+      is-short-map-short-function-Pseudometric-Space A B f d x y (x~y d)
 ```