diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md
index bc48c2ee7e..6b8a2c6213 100644
--- a/src/metric-spaces.lagda.md
+++ b/src/metric-spaces.lagda.md
@@ -67,6 +67,8 @@ 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-dense-metric-extensions-of-pseudometric-spaces public
+open import metric-spaces.cauchy-precompletion-of-pseudometric-spaces public
 open import metric-spaces.cauchy-pseudocompletion-of-metric-spaces public
 open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces public
 open import metric-spaces.cauchy-sequences-complete-metric-spaces public
@@ -75,6 +77,7 @@ open import metric-spaces.closed-subsets-located-metric-spaces public
 open import metric-spaces.closed-subsets-metric-spaces public
 open import metric-spaces.closure-subsets-metric-spaces public
 open import metric-spaces.compact-metric-spaces public
+open import metric-spaces.complete-metric-extensions-of-pseudometric-spaces public
 open import metric-spaces.complete-metric-spaces public
 open import metric-spaces.continuous-functions-metric-spaces public
 open import metric-spaces.convergent-cauchy-approximations-metric-spaces public
@@ -106,6 +109,7 @@ 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-extensions-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
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
index 9184f29af6..4c46e7a886 100644
--- 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
@@ -107,7 +107,7 @@ module _
       ( cauchy-pseudocompletion-Metric-Space
         ( metric-quotient-Pseudometric-Space M))
   short-map-metric-quotient-cauchy-apprtoximation-Pseudometric-Space =
-    short-map-short-function-cauchy-approximation-Pseudometric-Space
+    short-map-cauchy-approximation-short-function-Pseudometric-Space
       ( M)
       ( pseudometric-metric-quotient-Pseudometric-Space M)
       ( short-map-metric-quotient-Pseudometric-Space M)
diff --git a/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md
index caf5ee3d31..d8bf919a55 100644
--- a/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md
+++ b/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md
@@ -123,7 +123,7 @@ module _
     cauchy-approximation-Metric-Space A →
     cauchy-approximation-Metric-Space B
   map-short-function-cauchy-approximation-Metric-Space =
-    map-short-function-cauchy-approximation-Pseudometric-Space
+    map-cauchy-approximation-short-function-Pseudometric-Space
       ( pseudometric-Metric-Space A)
       ( pseudometric-Metric-Space B)
       ( f)
diff --git a/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md
index 3f7b863d42..b6b0b62a39 100644
--- a/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md
+++ b/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md
@@ -19,6 +19,7 @@ open import foundation.propositions
 open import foundation.subtypes
 open import foundation.universe-levels
 
+open import metric-spaces.isometries-pseudometric-spaces
 open import metric-spaces.pseudometric-spaces
 open import metric-spaces.short-functions-pseudometric-spaces
 ```
@@ -112,10 +113,10 @@ module _
   (f : short-function-Pseudometric-Space A B)
   where
 
-  map-short-function-cauchy-approximation-Pseudometric-Space :
+  map-cauchy-approximation-short-function-Pseudometric-Space :
     cauchy-approximation-Pseudometric-Space A →
     cauchy-approximation-Pseudometric-Space B
-  map-short-function-cauchy-approximation-Pseudometric-Space (u , H) =
+  map-cauchy-approximation-short-function-Pseudometric-Space (u , H) =
     ( map-short-function-Pseudometric-Space A B f ∘ u ,
       λ ε δ →
         is-short-map-short-function-Pseudometric-Space
@@ -128,6 +129,25 @@ module _
           ( H ε δ))
 ```
 
+### The action of isometries on Cauchy approximations
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
+  (f : isometry-Pseudometric-Space A B)
+  where
+
+  map-cauchy-approximation-isometry-Pseudometric-Space :
+    cauchy-approximation-Pseudometric-Space A →
+    cauchy-approximation-Pseudometric-Space B
+  map-cauchy-approximation-isometry-Pseudometric-Space =
+    map-cauchy-approximation-short-function-Pseudometric-Space
+      ( A)
+      ( B)
+      ( short-isometry-Pseudometric-Space A B f)
+```
+
 ### Homotopic Cauchy approximations are equal
 
 ```agda
diff --git a/src/metric-spaces/cauchy-dense-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-dense-metric-extensions-of-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..f47fed160e
--- /dev/null
+++ b/src/metric-spaces/cauchy-dense-metric-extensions-of-pseudometric-spaces.lagda.md
@@ -0,0 +1,497 @@
+# Cauchy dense metric extensions of pseudometric spaces
+
+```agda
+module metric-spaces.cauchy-dense-metric-extensions-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.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.subtypes
+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.cauchy-precompletion-of-pseudometric-spaces
+open import metric-spaces.cauchy-pseudocompletion-of-metric-spaces
+open import metric-spaces.cauchy-pseudocompletion-of-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-extensions-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-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
+
+A [metric extension](metric-spaces.metric-extensions-of-pseudometric-spaces.md)
+of a [pseudometric space](metric-spaces.pseudometric-spaces.md) is called
+{{#concept "Cauchy dense" Disambiguation="metric extension of a pseudometric space" Agda=is-cauchy-dense-Metric-Extension}}
+if all the points of the target [metric space](metric-spaces.metric-spaces.md)
+are [limits](metric-spaces.limits-of-cauchy-approximations-metric-spaces.md) of
+images of
+[cauchy approximations](metric-spaces.cauchy-approximations-metric-spaces.md) in
+the pseudometric space.
+
+## Definitions
+
+### The property of being a limit point of the Cauchy precompletion
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Pseudometric-Space l1 l2)
+  (M : Metric-Extension l3 l4 P)
+  (X : type-cauchy-precompletion-Pseudometric-Space P)
+  (y : type-metric-space-Metric-Extension P M)
+  where
+
+  is-limit-cauchy-precompletion-prop-point-Metric-Extension :
+    Prop (l1 ⊔ l2 ⊔ l4)
+  is-limit-cauchy-precompletion-prop-point-Metric-Extension =
+    Π-Prop
+      ( cauchy-approximation-Pseudometric-Space P)
+      ( λ x →
+        Π-Prop
+          ( is-in-class-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P)
+            ( X)
+            ( x))
+          ( λ x∈X →
+            is-limit-map-metric-extension-prop-cauchy-approximation-Pseudometric-Space
+              ( P)
+              ( M)
+              ( x)
+              ( y)))
+
+  is-limit-cauchy-precompletion-point-Metric-Extension : UU (l1 ⊔ l2 ⊔ l4)
+  is-limit-cauchy-precompletion-point-Metric-Extension =
+    type-Prop is-limit-cauchy-precompletion-prop-point-Metric-Extension
+```
+
+### Adherent points of a metric extension
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Pseudometric-Space l1 l2)
+  (M : Metric-Extension l3 l4 P)
+  (y : type-metric-space-Metric-Extension P M)
+  where
+
+  is-adherent-point-Metric-Extension : UU (l1 ⊔ l2 ⊔ l4)
+  is-adherent-point-Metric-Extension =
+    Σ ( type-cauchy-precompletion-Pseudometric-Space P)
+      ( λ X →
+        is-limit-cauchy-precompletion-point-Metric-Extension P M X y)
+
+  all-eq-is-adherent-point-Metric-Extension :
+    (X X' : is-adherent-point-Metric-Extension) → X ＝ X'
+  all-eq-is-adherent-point-Metric-Extension (X , lim-X) (X' , lim-X') =
+    eq-type-subtype
+      ( λ Y → is-limit-cauchy-precompletion-prop-point-Metric-Extension P M Y y)
+      ( X＝X')
+      where
+        X＝X' : X ＝ X'
+        X＝X' =
+          let
+            open
+              do-syntax-trunc-Prop
+                ( Id-Prop
+                  ( set-Metric-Space
+                    ( cauchy-precompletion-Pseudometric-Space P))
+                  ( X)
+                  ( X'))
+          in do
+            (x , x∈X) ←
+              is-inhabited-class-metric-quotient-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P)
+                ( X)
+            (x' , x'∈X') ←
+              is-inhabited-class-metric-quotient-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P)
+                ( X')
+            eq-set-quotient-sim-element-set-quotient
+              ( equivalence-relation-sim-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P))
+              ( X)
+              ( X')
+              ( x∈X)
+              ( x'∈X')
+              ( lemma-sim-is-limit-map-metric-extension-cauchy-approximation-Pseudometric-Space
+                ( P)
+                ( M)
+                ( y)
+                ( x)
+                ( x')
+                ( lim-X x x∈X)
+                ( lim-X' x' x'∈X'))
+
+  is-prop-is-adherent-point-Metric-Extension :
+    is-prop is-adherent-point-Metric-Extension
+  is-prop-is-adherent-point-Metric-Extension =
+    is-prop-all-elements-equal all-eq-is-adherent-point-Metric-Extension
+
+  is-adherent-prop-point-Metric-Extension : Prop (l1 ⊔ l2 ⊔ l4)
+  is-adherent-prop-point-Metric-Extension =
+    ( is-adherent-point-Metric-Extension ,
+      is-prop-is-adherent-point-Metric-Extension)
+```
+
+### The property of being a Cauchy dense metric extensions
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Pseudometric-Space l1 l2)
+  (M : Metric-Extension l3 l4 P)
+  where
+
+  is-cauchy-dense-prop-Metric-Extension : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-cauchy-dense-prop-Metric-Extension =
+    Π-Prop
+      ( type-metric-space-Metric-Extension P M)
+      ( is-adherent-prop-point-Metric-Extension P M)
+
+  is-cauchy-dense-Metric-Extension : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-cauchy-dense-Metric-Extension =
+    type-Prop is-cauchy-dense-prop-Metric-Extension
+
+  is-prop-is-cauchy-dense-Metric-Extension :
+    is-prop is-cauchy-dense-Metric-Extension
+  is-prop-is-cauchy-dense-Metric-Extension =
+    is-prop-type-Prop is-cauchy-dense-prop-Metric-Extension
+```
+
+## Properties
+
+### The map from the target metric space of a Cauchy dense extension into the Cauchy precompletion is an isometry
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Pseudometric-Space l1 l2)
+  (M : Metric-Extension l3 l4 P)
+  (dense-M : is-cauchy-dense-Metric-Extension P M)
+  where
+
+  map-cauchy-precompletion-is-cauchy-dense-Metric-Extension :
+    type-metric-space-Metric-Extension P M →
+    type-cauchy-precompletion-Pseudometric-Space P
+  map-cauchy-precompletion-is-cauchy-dense-Metric-Extension y =
+    pr1 (dense-M y)
+
+  is-limit-map-cauchy-precompletion-is-cauchy-dense-Metric-Extension :
+    (y : type-metric-space-Metric-Extension P M) →
+    is-limit-cauchy-precompletion-point-Metric-Extension
+      ( P)
+      ( M)
+      ( map-cauchy-precompletion-is-cauchy-dense-Metric-Extension y)
+      ( y)
+  is-limit-map-cauchy-precompletion-is-cauchy-dense-Metric-Extension y =
+    pr2 (dense-M y)
+
+  sim-const-is-in-class-map-cauchy-precompletion-is-cauchy-dense-Metric-Extension :
+    (y : type-metric-space-Metric-Extension P M) →
+    (x : cauchy-approximation-Pseudometric-Space P) →
+    is-in-class-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( map-cauchy-precompletion-is-cauchy-dense-Metric-Extension y)
+      ( x) →
+    sim-Pseudometric-Space
+      ( cauchy-pseudocompletion-Metric-Space
+        ( metric-space-Metric-Extension P M))
+      ( map-metric-extension-cauchy-approximation-Pseudometric-Space
+        ( P)
+        ( M)
+        ( x))
+      ( const-cauchy-approximation-Metric-Space
+        ( metric-space-Metric-Extension P M)
+        ( y))
+  sim-const-is-in-class-map-cauchy-precompletion-is-cauchy-dense-Metric-Extension
+    y x x∈X =
+    sim-const-is-limit-cauchy-approximation-Metric-Space
+      ( metric-space-Metric-Extension P M)
+      ( map-metric-extension-cauchy-approximation-Pseudometric-Space P M x)
+      ( y)
+      ( is-limit-map-cauchy-precompletion-is-cauchy-dense-Metric-Extension
+        ( y)
+        ( x)
+        ( x∈X))
+
+  preserves-neighborhood-map-cauchy-precompletion-is-dense-Metric-Extension :
+    is-short-function-Metric-Space
+      ( metric-space-Metric-Extension P M)
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( map-cauchy-precompletion-is-cauchy-dense-Metric-Extension)
+  preserves-neighborhood-map-cauchy-precompletion-is-dense-Metric-Extension
+    d X Y NXY (x , x∈fX) (y , y∈fY) =
+    reflects-neighborhood-map-isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-pseudocompletion-Metric-Space
+        ( metric-space-Metric-Extension P M))
+      ( isometry-metric-extension-cauchy-approximation-Pseudometric-Space P M)
+      ( d)
+      ( x)
+      ( y)
+      ( Nxy)
+    where
+
+    fx~X :
+      sim-Pseudometric-Space
+        ( cauchy-pseudocompletion-Metric-Space
+          ( metric-space-Metric-Extension P M))
+        ( map-metric-extension-cauchy-approximation-Pseudometric-Space P M x)
+        ( const-cauchy-approximation-Metric-Space
+          ( metric-space-Metric-Extension P M)
+          ( X))
+    fx~X =
+      sim-const-is-in-class-map-cauchy-precompletion-is-cauchy-dense-Metric-Extension
+        ( X)
+        ( x)
+        ( x∈fX)
+
+    fy~Y :
+      sim-Pseudometric-Space
+        ( cauchy-pseudocompletion-Metric-Space
+          ( metric-space-Metric-Extension P M))
+        ( map-metric-extension-cauchy-approximation-Pseudometric-Space P M y)
+        ( const-cauchy-approximation-Metric-Space
+          ( metric-space-Metric-Extension P M)
+          ( Y))
+    fy~Y =
+      sim-const-is-in-class-map-cauchy-precompletion-is-cauchy-dense-Metric-Extension
+        ( Y)
+        ( y)
+        ( y∈fY)
+
+    Nxy :
+      neighborhood-Pseudometric-Space
+        ( cauchy-pseudocompletion-Metric-Space
+          ( metric-space-Metric-Extension P M))
+        ( d)
+        ( map-metric-extension-cauchy-approximation-Pseudometric-Space P M x)
+        ( map-metric-extension-cauchy-approximation-Pseudometric-Space P M y)
+    Nxy =
+      reflects-neighborhood-sim-Pseudometric-Space
+        ( cauchy-pseudocompletion-Metric-Space
+          ( metric-space-Metric-Extension P M))
+        { map-metric-extension-cauchy-approximation-Pseudometric-Space P M x}
+        { const-cauchy-approximation-Metric-Space
+          ( metric-space-Metric-Extension P M)
+          ( X)}
+        { map-metric-extension-cauchy-approximation-Pseudometric-Space P M y}
+        { const-cauchy-approximation-Metric-Space
+          ( metric-space-Metric-Extension P M)
+          ( Y)}
+        ( fx~X)
+        ( fy~Y)
+        ( d)
+        ( preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space
+          ( pseudometric-space-Metric-Extension P M)
+          ( d)
+          ( X)
+          ( Y)
+          ( NXY))
+
+  reflects-neighborhood-map-cauchy-precompletion-is-dense-Metric-Extension :
+    ( d : ℚ⁺) →
+    ( X Y : type-metric-space-Metric-Extension P M) →
+    neighborhood-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( d)
+      ( map-cauchy-precompletion-is-cauchy-dense-Metric-Extension X)
+      ( map-cauchy-precompletion-is-cauchy-dense-Metric-Extension Y) →
+    neighborhood-Metric-Space
+      ( metric-space-Metric-Extension P M)
+      ( d)
+      ( X)
+      ( Y)
+  reflects-neighborhood-map-cauchy-precompletion-is-dense-Metric-Extension
+    d X Y NXY =
+    let
+      open
+        do-syntax-trunc-Prop
+          ( neighborhood-prop-Metric-Space
+            ( metric-space-Metric-Extension P M)
+            ( d)
+            ( X)
+            ( Y))
+      in do
+        ( u , lim-u) ←
+          is-inhabited-class-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P)
+            ( map-cauchy-precompletion-is-cauchy-dense-Metric-Extension X)
+
+        ( v , lim-v) ←
+          is-inhabited-class-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P)
+            ( map-cauchy-precompletion-is-cauchy-dense-Metric-Extension Y)
+        let
+          fu~X :
+            sim-Pseudometric-Space
+              ( cauchy-pseudocompletion-Metric-Space
+                ( metric-space-Metric-Extension P M))
+              ( map-metric-extension-cauchy-approximation-Pseudometric-Space
+                ( P)
+                ( M)
+                ( u))
+              ( const-cauchy-approximation-Metric-Space
+                ( metric-space-Metric-Extension P M)
+                ( X))
+          fu~X =
+            sim-const-is-in-class-map-cauchy-precompletion-is-cauchy-dense-Metric-Extension
+              ( X)
+              ( u)
+              ( lim-u)
+
+          fv~Y :
+            sim-Pseudometric-Space
+              ( cauchy-pseudocompletion-Metric-Space
+                ( metric-space-Metric-Extension P M))
+              ( map-metric-extension-cauchy-approximation-Pseudometric-Space
+                ( P)
+                ( M)
+                ( v))
+              ( const-cauchy-approximation-Metric-Space
+                ( metric-space-Metric-Extension P M)
+                ( Y))
+          fv~Y =
+            sim-const-is-in-class-map-cauchy-precompletion-is-cauchy-dense-Metric-Extension
+              ( Y)
+              ( v)
+              ( lim-v)
+
+          Nuv :
+            neighborhood-Pseudometric-Space
+              ( cauchy-pseudocompletion-Metric-Space
+                ( metric-space-Metric-Extension P M))
+              ( d)
+              ( map-metric-extension-cauchy-approximation-Pseudometric-Space
+                ( P)
+                ( M)
+                ( u))
+              ( map-metric-extension-cauchy-approximation-Pseudometric-Space
+                ( P)
+                ( M)
+                ( v))
+          Nuv =
+            preserves-neighborhood-map-isometry-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P)
+              ( cauchy-pseudocompletion-Metric-Space
+                ( metric-space-Metric-Extension P M))
+              ( isometry-metric-extension-cauchy-approximation-Pseudometric-Space
+                ( P)
+                ( M))
+              ( d)
+              ( u)
+              ( v)
+              ( NXY (u , lim-u) (v , lim-v))
+
+        reflects-neighborhood-map-isometry-Pseudometric-Space
+          ( pseudometric-space-Metric-Extension P M)
+          ( cauchy-pseudocompletion-Metric-Space
+            ( metric-space-Metric-Extension P M))
+          ( isometry-cauchy-pseudocompletion-Metric-Space
+            ( metric-space-Metric-Extension P M))
+          ( d)
+          ( X)
+          ( Y)
+          ( preserves-neighborhood-sim-Pseudometric-Space
+            ( cauchy-pseudocompletion-Metric-Space
+              ( metric-space-Metric-Extension P M))
+            { map-metric-extension-cauchy-approximation-Pseudometric-Space
+              ( P)
+              ( M)
+              ( u)}
+            { const-cauchy-approximation-Metric-Space
+              ( metric-space-Metric-Extension P M)
+              ( X)}
+            { map-metric-extension-cauchy-approximation-Pseudometric-Space
+              ( P)
+              ( M)
+              ( v)}
+            { const-cauchy-approximation-Metric-Space
+              ( metric-space-Metric-Extension P M)
+              ( Y)}
+            ( fu~X)
+            ( fv~Y)
+            ( d)
+            ( Nuv))
+
+  is-isometry-map-cauchy-precompletion-is-dense-Metric-Extension :
+    is-isometry-Metric-Space
+      ( metric-space-Metric-Extension P M)
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( map-cauchy-precompletion-is-cauchy-dense-Metric-Extension)
+  is-isometry-map-cauchy-precompletion-is-dense-Metric-Extension d x y =
+    ( ( preserves-neighborhood-map-cauchy-precompletion-is-dense-Metric-Extension
+        ( d)
+        ( x)
+        ( y)) ,
+      ( reflects-neighborhood-map-cauchy-precompletion-is-dense-Metric-Extension
+        ( d)
+        ( x)
+        ( y)))
+
+  isometry-map-cauchy-precompletion-is-dense-Metric-Extension :
+    isometry-Metric-Space
+      ( metric-space-Metric-Extension P M)
+      ( cauchy-precompletion-Pseudometric-Space P)
+  isometry-map-cauchy-precompletion-is-dense-Metric-Extension =
+    ( map-cauchy-precompletion-is-cauchy-dense-Metric-Extension ,
+      is-isometry-map-cauchy-precompletion-is-dense-Metric-Extension)
+```
+
+### The Cauchy precompletion of a pseudometric space is Cauchy dense
+
+```agda
+module _
+  {l1 l2 : Level}
+  (P : Pseudometric-Space l1 l2)
+  where
+
+  is-cauchy-dense-metric-extension-cauchy-precompletion-Pseudometric-Space :
+    is-cauchy-dense-Metric-Extension
+      ( P)
+      ( metric-extension-cauchy-precompletion-Pseudometric-Space P)
+  is-cauchy-dense-metric-extension-cauchy-precompletion-Pseudometric-Space X =
+    ( X , is-limit-is-in-class-cauchy-precompletion-Pseudometric-Space P X)
+```
diff --git a/src/metric-spaces/cauchy-precompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-precompletion-of-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..604ca15726
--- /dev/null
+++ b/src/metric-spaces/cauchy-precompletion-of-pseudometric-spaces.lagda.md
@@ -0,0 +1,1151 @@
+# The Cauchy precompletion of a pseudometric space
+
+```agda
+module metric-spaces.cauchy-precompletion-of-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.isomorphisms-in-precategories
+
+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.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.cauchy-pseudocompletion-of-metric-spaces
+open import metric-spaces.cauchy-pseudocompletion-of-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-extensions-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-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
+[Cauchy pseudocompletion](metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces.md);
+the
+{{#concept "Cauchy precompletion" Disambiguation="of a pseudometric space" Agda=cauchy-precompletion-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 Cauchy precompletion of the Cauchy pseudocompletion of a pseudometric space
+is the Cauchy precompletion 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)`. So the Cauchy precompletion of a pseudometric space is
+[complete](metric-spaces.complete-metric-spaces.md) if and only if all its
+Cauchy approximations have a lift up to similarity in its Cauchy
+pseudocompletion.
+
+Any [short map](metric-spaces.short-functions-pseudometric-spaces.md) (resp.
+isometry) from a pseudometric space in a complete metric space factors as a
+short map (resp. isometry) through the Cauchy precompletion of its domain. This
+is the
+{{#concept "universal property" Disambiguation="of the Cauchy precompletion of a pseudometric space"}}
+of the Cauchy precompletion.
+
+## Definition
+
+### The Cauchy precompletion of a pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  cauchy-precompletion-Pseudometric-Space :
+    Metric-Space (l1 ⊔ l2) (l1 ⊔ l2)
+  cauchy-precompletion-Pseudometric-Space =
+    metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+
+  pseudometric-cauchy-precompletion-Pseudometric-Space :
+    Pseudometric-Space (l1 ⊔ l2) (l1 ⊔ l2)
+  pseudometric-cauchy-precompletion-Pseudometric-Space =
+    pseudometric-Metric-Space
+      cauchy-precompletion-Pseudometric-Space
+
+  type-cauchy-precompletion-Pseudometric-Space : UU (l1 ⊔ l2)
+  type-cauchy-precompletion-Pseudometric-Space =
+    type-Metric-Space cauchy-precompletion-Pseudometric-Space
+```
+
+### The Cauchy precompletion of the Cauchy pseudocompletion of a pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space :
+    Metric-Space (l1 ⊔ l2) (l1 ⊔ l2)
+  cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space =
+    cauchy-precompletion-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+```
+
+## Properties
+
+### The isometry from the Cauchy pseudocompletion of a pseudometric space into its Cauchy precompletion
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  isometry-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+  isometry-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space =
+    isometry-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+```
+
+### The isometry from a pseudometric space into its Cauchy precompletion
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  isometry-cauchy-precompletion-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( P)
+      ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+  isometry-cauchy-precompletion-Pseudometric-Space =
+    comp-isometry-Pseudometric-Space
+      ( P)
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+      ( isometry-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+        ( P))
+      ( isometry-cauchy-pseudocompletion-Pseudometric-Space P)
+
+  metric-extension-cauchy-precompletion-Pseudometric-Space :
+    Metric-Extension (l1 ⊔ l2) (l1 ⊔ l2) P
+  metric-extension-cauchy-precompletion-Pseudometric-Space =
+    ( ( cauchy-precompletion-Pseudometric-Space P) ,
+      ( isometry-cauchy-precompletion-Pseudometric-Space))
+```
+
+### The isometry from the Cauchy pseudocompletion of the Cauchy pseudocompletion into the Cauchy precompletion
+
+```agda
+module _
+  { l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  isometry-cauchy-precompletion-cauchy-pseudocompletion²-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P))
+      ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+  isometry-cauchy-precompletion-cauchy-pseudocompletion²-Pseudometric-Space =
+    comp-isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P))
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+      ( isometry-metric-quotient-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P))
+      ( isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+        ( P))
+
+  short-map-cauchy-precompletion-cauchy-pseudocompletion²-Pseudometric-Space :
+    short-function-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P))
+      ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+  short-map-cauchy-precompletion-cauchy-pseudocompletion²-Pseudometric-Space =
+    short-isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P))
+      ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+      ( isometry-cauchy-precompletion-cauchy-pseudocompletion²-Pseudometric-Space)
+```
+
+### The short isomorphism from the Cauchy precompletion of the Cauchy pseudocompletion of a pseudometric space into its Cauchy precompletion
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  short-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space :
+    short-function-Metric-Space
+      ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-precompletion-Pseudometric-Space P)
+  short-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space =
+    short-map-short-function-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P))
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( short-map-cauchy-precompletion-cauchy-pseudocompletion²-Pseudometric-Space
+        ( P))
+
+  map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space :
+    type-function-Metric-Space
+      ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-precompletion-Pseudometric-Space P)
+  map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space =
+    map-short-function-Metric-Space
+      ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( short-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space)
+
+  compute-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space :
+    ( X :
+      type-cauchy-precompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)) →
+    ( x :
+      cauchy-approximation-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)) →
+    is-in-class-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P))
+      ( X)
+      ( x) →
+    map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space X ＝
+    map-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+        ( P)
+        ( x))
+  compute-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+    =
+    compute-map-short-function-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P))
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( short-map-cauchy-precompletion-cauchy-pseudocompletion²-Pseudometric-Space
+        ( P))
+
+  short-map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space :
+    short-function-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P)
+  short-map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space =
+    short-map-short-function-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P)
+      ( comp-short-function-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( cauchy-pseudocompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space P))
+        ( pseudometric-cauchy-precompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space P))
+        ( short-map-metric-quotient-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P)))
+        ( short-map-cauchy-pseudocompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space P)))
+
+  map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space :
+    type-function-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P)
+  map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space =
+    map-short-function-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P)
+      ( short-map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space)
+
+  compute-map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space :
+    (X : type-cauchy-precompletion-Pseudometric-Space P) →
+    (x : cauchy-approximation-Pseudometric-Space P) →
+    is-in-class-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( X)
+      ( x) →
+    map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+      ( X) ＝
+    map-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P))
+      ( map-cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( x))
+  compute-map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+    =
+    compute-map-short-function-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P)
+      ( comp-short-function-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( cauchy-pseudocompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space P))
+        ( pseudometric-cauchy-precompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space P))
+        ( short-map-metric-quotient-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P)))
+        ( short-map-cauchy-pseudocompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space P)))
+
+  is-section-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space :
+    ( map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space ∘
+      map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space) ~
+    id
+  is-section-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+    X =
+    let
+      open
+        do-syntax-trunc-Prop
+          ( Id-Prop
+            ( set-Metric-Space
+              ( cauchy-precompletion-Pseudometric-Space P))
+            ( map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+              ( map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+                ( X)))
+            ( X))
+    in do
+      ( x , x∈X) ←
+        is-inhabited-class-metric-quotient-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space P)
+          ( X)
+      let
+        map-inv-X =
+          map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+            ( X)
+
+        compute-map-inv-X :
+          map-inv-X ＝
+          map-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P))
+            ( map-cauchy-pseudocompletion-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P)
+              ( x))
+        compute-map-inv-X =
+          compute-map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+            ( X)
+            ( x)
+            ( x∈X)
+
+        is-in-class-x :
+          is-in-class-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P))
+            ( map-inv-X)
+            ( map-cauchy-pseudocompletion-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P)
+              ( x))
+        is-in-class-x =
+          inv-tr
+            ( λ Y →
+              is-in-class-metric-quotient-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space
+                  ( cauchy-pseudocompletion-Pseudometric-Space P))
+                ( Y)
+                ( map-cauchy-pseudocompletion-Pseudometric-Space
+                  ( cauchy-pseudocompletion-Pseudometric-Space P)
+                  ( x)))
+            ( compute-map-inv-X)
+            ( is-in-class-map-quotient-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P))
+              ( map-cauchy-pseudocompletion-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P)
+                ( x)))
+
+        compute-map :
+          map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+            ( map-inv-X) ＝
+          map-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P)
+            ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              ( P)
+              ( map-cauchy-pseudocompletion-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P)
+                ( x)))
+        compute-map =
+          compute-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+            ( map-inv-X)
+            ( map-cauchy-pseudocompletion-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P)
+              ( x))
+            ( is-in-class-x)
+
+        compute-quotient-lim :
+          map-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P)
+            ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              ( P)
+              ( map-cauchy-pseudocompletion-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P)
+                ( x))) ＝
+          map-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P)
+            ( x)
+        compute-quotient-lim =
+          apply-effectiveness-quotient-map'
+            ( equivalence-relation-sim-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P))
+            ( all-sim-is-limit-cauchy-approximation-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P)
+              ( map-cauchy-pseudocompletion-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P)
+                ( x))
+              ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+                ( P)
+                ( map-cauchy-pseudocompletion-Pseudometric-Space
+                  ( cauchy-pseudocompletion-Pseudometric-Space P)
+                  ( x)))
+              ( x)
+              ( is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+                ( P)
+                ( map-cauchy-pseudocompletion-Pseudometric-Space
+                  ( cauchy-pseudocompletion-Pseudometric-Space P)
+                  ( x)))
+              ( is-limit-const-cauchy-approximation-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P)
+                ( x)))
+
+        compute-quotient-x :
+          map-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P)
+            ( x) ＝ X
+        compute-quotient-x =
+          eq-set-quotient-equivalence-class-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P))
+            ( X)
+            ( x∈X)
+
+      ( compute-map ∙
+        compute-quotient-lim ∙
+        compute-quotient-x)
+
+  is-retraction-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space :
+    ( map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space ∘
+      map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space)
+      ~
+    id
+  is-retraction-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+    X =
+    let
+      open
+        do-syntax-trunc-Prop
+          ( Id-Prop
+            ( set-Metric-Space
+              ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+                ( P)))
+            ( map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+              ( map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+                ( X)))
+            ( X))
+
+    in do
+      ( x , x∈X) ←
+        is-inhabited-class-metric-quotient-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P))
+          ( X)
+      let
+        map-X =
+          map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+            ( X)
+
+        compute-map-X :
+          map-X ＝
+          map-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P)
+            ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              ( P)
+              ( x))
+        compute-map-X =
+          compute-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+            ( X)
+            ( x)
+            ( x∈X)
+
+        is-in-class-map-X :
+          is-in-class-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P)
+            ( map-X)
+            ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              ( P)
+              ( x))
+        is-in-class-map-X =
+          inv-tr
+            ( λ Y →
+              is-in-class-metric-quotient-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P)
+                ( Y)
+                ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+                  ( P)
+                  ( x)))
+            ( compute-map-X)
+            ( is-in-class-map-quotient-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P)
+              ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+                ( P)
+                ( x)))
+
+        compute-map-inv :
+          map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+            ( map-X) ＝
+          map-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P))
+            ( map-cauchy-pseudocompletion-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P)
+              ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+                ( P)
+                ( x)))
+        compute-map-inv =
+          compute-map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+            ( map-X)
+            ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              ( P)
+              ( x))
+            ( is-in-class-map-X)
+
+        compute-map-quotient-lim :
+          map-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P))
+            ( map-cauchy-pseudocompletion-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P)
+              ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+                ( P)
+                ( x))) ＝
+          map-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P))
+            ( x)
+        compute-map-quotient-lim =
+          apply-effectiveness-quotient-map'
+            ( equivalence-relation-sim-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P)))
+            ( symmetric-sim-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P))
+              ( x)
+              ( map-cauchy-pseudocompletion-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P)
+                ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+                  ( P)
+                  ( x)))
+              ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P)
+                ( x)
+                ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+                  ( P)
+                  ( x))
+                ( is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+                  ( P)
+                  ( x))))
+
+        compute-quotient-x :
+          map-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P))
+            ( x) ＝
+          X
+        compute-quotient-x =
+          eq-set-quotient-equivalence-class-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P)))
+            ( X)
+            ( x∈X)
+
+      ( compute-map-inv ∙
+        compute-map-quotient-lim ∙
+        compute-quotient-x)
+
+  is-iso-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space :
+    is-iso-Precategory
+      precategory-short-function-Metric-Space
+      { cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P}
+      { cauchy-precompletion-Pseudometric-Space P}
+      short-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+  pr1
+    is-iso-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+    =
+    short-map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+  pr2
+    is-iso-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+    =
+    ( ( eq-htpy-map-short-function-Metric-Space
+        ( cauchy-precompletion-Pseudometric-Space P)
+        ( cauchy-precompletion-Pseudometric-Space P)
+        ( comp-short-function-Metric-Space
+          ( cauchy-precompletion-Pseudometric-Space P)
+          ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+            ( P))
+          ( cauchy-precompletion-Pseudometric-Space P)
+          ( short-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space)
+          ( short-map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space))
+        ( short-id-Metric-Space
+          ( cauchy-precompletion-Pseudometric-Space P))
+        ( is-section-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space)) ,
+      ( eq-htpy-map-short-function-Metric-Space
+        ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P)
+        ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P)
+        ( comp-short-function-Metric-Space
+          ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+            ( P))
+          ( cauchy-precompletion-Pseudometric-Space P)
+            ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+              ( P))
+          ( short-map-inv-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space)
+          ( short-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space))
+        ( short-id-Metric-Space
+          ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+            ( P)))
+        ( is-retraction-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space)))
+
+  iso-metric-pseudocompeletion-cauchy-pseudocompletion-Pseudometric-Space :
+    iso-Precategory
+      ( precategory-short-function-Metric-Space)
+      ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-precompletion-Pseudometric-Space P)
+  iso-metric-pseudocompeletion-cauchy-pseudocompletion-Pseudometric-Space =
+    ( short-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space ,
+      is-iso-map-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space)
+```
+
+### The equality between the Cauchy precompletion of the Cauchy pseudocompletion of a pseudometric space and its Cauchy precompletion
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  eq-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space :
+    ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P) ＝
+    ( cauchy-precompletion-Pseudometric-Space P)
+  eq-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space =
+    eq-isometric-equiv-Metric-Space'
+      ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( map-equiv-isometric-equiv-iso-short-function-Metric-Space'
+        ( cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space P)
+        ( cauchy-precompletion-Pseudometric-Space P)
+        ( iso-metric-pseudocompeletion-cauchy-pseudocompletion-Pseudometric-Space
+          ( P)))
+```
+
+### A Cauchy approximation in the Cauchy precompletion of a pseudometric space is convergent if and only if it has a lift its Cauchy pseudocompletion
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  ( u :
+    cauchy-approximation-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P))
+  where
+
+  is-convergent-has-lift-cauchy-approximation-cauchy-precompletion-Pseudometric-Space :
+    has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( u) →
+    is-convergent-cauchy-approximation-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( u)
+  is-convergent-has-lift-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+    sim-lift =
+    let
+      open
+        do-syntax-trunc-Prop
+          ( is-convergent-prop-cauchy-approximation-Metric-Space
+            ( cauchy-precompletion-Pseudometric-Space P)
+            ( u))
+    in do
+      ( v , u~[v]) ← sim-lift
+      let
+        ( lim-v , is-lim-v) =
+          has-limit-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+            ( P)
+            ( v)
+
+        lim-u =
+          map-metric-quotient-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P)
+            ( lim-v)
+
+        is-lim[v]-lim-u :
+          is-limit-cauchy-approximation-Metric-Space
+            ( metric-quotient-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P))
+            ( map-metric-quotient-cauchy-approximation-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P)
+              ( v))
+            ( lim-u)
+        is-lim[v]-lim-u =
+          preserves-limits-map-metric-quotient-cauchy-approximation-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space P)
+            ( v)
+            ( lim-v)
+            ( is-lim-v)
+
+        [lim-u] =
+          const-cauchy-approximation-Metric-Space
+            ( cauchy-precompletion-Pseudometric-Space P)
+            ( lim-u)
+
+        u~[lim-u] :
+          sim-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space
+              ( pseudometric-cauchy-precompletion-Pseudometric-Space P))
+            ( u)
+            ( [lim-u])
+        u~[lim-u] =
+          transitive-sim-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space
+              ( pseudometric-cauchy-precompletion-Pseudometric-Space P))
+            ( u)
+            ( map-metric-quotient-cauchy-approximation-Pseudometric-Space
+              ( cauchy-pseudocompletion-Pseudometric-Space P)
+              ( v))
+            ( [lim-u])
+            ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+              ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+              ( map-metric-quotient-cauchy-approximation-Pseudometric-Space
+                ( cauchy-pseudocompletion-Pseudometric-Space P)
+                ( v))
+              ( lim-u)
+              ( is-lim[v]-lim-u))
+            ( u~[v])
+      ( ( lim-u) ,
+        ( is-limit-sim-const-cauchy-approximation-Pseudometric-Space
+          ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+          ( u)
+          ( lim-u)
+          ( u~[lim-u])))
+
+  iff-has-lift-is-convergent-cauchy-approximation-cauchy-precompletion-Pseudometric-Space :
+    is-convergent-cauchy-approximation-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( u) ↔
+    has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( u)
+  pr1
+    iff-has-lift-is-convergent-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+    =
+    has-lift-is-convergent-cauchy-approximation-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( u)
+  pr2
+    iff-has-lift-is-convergent-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+    =
+    is-convergent-has-lift-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+
+  equiv-has-lift-is-convergent-cauchy-approximation-cauchy-precompletion-Pseudometric-Space :
+    is-convergent-cauchy-approximation-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( u) ≃
+    has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( u)
+  equiv-has-lift-is-convergent-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+    =
+    equiv-iff
+      ( is-convergent-prop-cauchy-approximation-Metric-Space
+        ( cauchy-precompletion-Pseudometric-Space P)
+        ( u))
+      ( has-lift-prop-cauchy-approximation-metric-quotient-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( u))
+      ( has-lift-is-convergent-cauchy-approximation-metric-quotient-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( u))
+      ( is-convergent-has-lift-cauchy-approximation-cauchy-precompletion-Pseudometric-Space)
+```
+
+### Images of Cauchy approximations in a pseudometric space converge in its Cauchy precompletion
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  (u : cauchy-approximation-Pseudometric-Space P)
+  where
+
+  is-convergent-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space :
+    is-convergent-cauchy-approximation-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space
+        ( P)
+        ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+        ( isometry-cauchy-precompletion-Pseudometric-Space P)
+        ( u))
+  is-convergent-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+    =
+    is-convergent-has-lift-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+      ( P)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space
+        ( P)
+        ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+        ( isometry-cauchy-precompletion-Pseudometric-Space P)
+        ( u))
+      ( has-lift-map-quotient-cauchy-approximation-metric-quotient-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( map-cauchy-approximation-isometry-Pseudometric-Space
+          ( P)
+          ( cauchy-pseudocompletion-Pseudometric-Space P)
+          ( isometry-cauchy-pseudocompletion-Pseudometric-Space P)
+          ( u)))
+
+  lim-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space :
+    type-cauchy-precompletion-Pseudometric-Space P
+  lim-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space =
+    pr1
+      is-convergent-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+
+  is-limit-lim-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space :
+    is-limit-cauchy-approximation-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space
+        ( P)
+        ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+        ( isometry-cauchy-precompletion-Pseudometric-Space P)
+        ( u))
+      ( lim-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space)
+  is-limit-lim-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+    =
+    pr2
+      is-convergent-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+```
+
+### The Cauchy precompletion of a pseudometric space is complete if and only if all its Cauchy approximations have a lift in its Cauchy pseudocompletion
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  iff-all-has-lift-is-complete-cauchy-precompletion-Pseudometric-Space :
+    is-complete-Metric-Space (cauchy-precompletion-Pseudometric-Space P) ↔
+    ( ( u : cauchy-approximation-Metric-Space
+        ( cauchy-precompletion-Pseudometric-Space P)) →
+      has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( u))
+  pr1 iff-all-has-lift-is-complete-cauchy-precompletion-Pseudometric-Space H u =
+    has-lift-is-convergent-cauchy-approximation-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( u)
+      ( H u)
+  pr2 iff-all-has-lift-is-complete-cauchy-precompletion-Pseudometric-Space K u =
+    is-convergent-has-lift-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+      ( P)
+      ( u)
+      ( K u)
+```
+
+### Induced short map from the Cauchy precompletion to a complete metric space
+
+```agda
+module _
+  { l1 l2 l3 l4 : Level} (P : Pseudometric-Space l1 l2)
+  ( C : Complete-Metric-Space l3 l4)
+  where
+
+  short-map-short-function-complete-metric-space-cauchy-precompletion-Pseudometric-Space :
+    short-function-Pseudometric-Space
+      ( P)
+      ( pseudometric-space-Complete-Metric-Space C) →
+    short-function-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+        ( metric-space-Complete-Metric-Space C)
+  short-map-short-function-complete-metric-space-cauchy-precompletion-Pseudometric-Space
+    f =
+    short-map-short-function-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( metric-space-Complete-Metric-Space C)
+      ( comp-short-function-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( cauchy-pseudocompletion-Metric-Space
+          ( metric-space-Complete-Metric-Space C))
+        ( pseudometric-space-Complete-Metric-Space C)
+        ( short-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( metric-space-Complete-Metric-Space C)
+          ( is-complete-metric-space-Complete-Metric-Space C))
+        ( short-map-cauchy-approximation-short-function-Pseudometric-Space
+          ( P)
+          ( pseudometric-space-Complete-Metric-Space C)
+          ( f)))
+```
+
+### Induced isometry from the Cauchy precompletion into a complete metric space
+
+```agda
+module _
+  { l1 l2 l3 l4 : Level} (P : Pseudometric-Space l1 l2)
+  ( C : Complete-Metric-Space l3 l4)
+  where
+
+  isometry-map-isometry-complete-metric-space-cauchy-precompletion-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( P)
+      ( pseudometric-space-Complete-Metric-Space C) →
+    isometry-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( metric-space-Complete-Metric-Space C)
+  isometry-map-isometry-complete-metric-space-cauchy-precompletion-Pseudometric-Space
+    f =
+    isometry-map-isometry-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( metric-space-Complete-Metric-Space C)
+      ( comp-isometry-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( cauchy-pseudocompletion-Metric-Space
+          ( metric-space-Complete-Metric-Space C))
+        ( pseudometric-space-Complete-Metric-Space C)
+        ( isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( metric-space-Complete-Metric-Space C)
+          ( is-complete-metric-space-Complete-Metric-Space C))
+        ( isometry-map-cauchy-approximation-isometry-Pseudometric-Space
+          ( P)
+          ( pseudometric-space-Complete-Metric-Space C)
+          ( f)))
+```
+
+### The image of a Cauchy approximation in the Cauchy precompletion converges to its image by the quotient map
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  (u : cauchy-approximation-Pseudometric-Space P)
+  where
+
+  sim-const-map-isometry-cauchy-precompletion-Pseudometric-Space :
+    sim-Pseudometric-Space
+      ( cauchy-pseudocompletion-Metric-Space
+        ( cauchy-precompletion-Pseudometric-Space P))
+      ( map-cauchy-approximation-isometry-Pseudometric-Space
+        ( P)
+        ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+        ( isometry-cauchy-precompletion-Pseudometric-Space P)
+        ( u))
+      ( const-cauchy-approximation-Metric-Space
+        ( cauchy-precompletion-Pseudometric-Space P)
+        ( map-metric-quotient-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space P)
+          ( u)))
+  sim-const-map-isometry-cauchy-precompletion-Pseudometric-Space d α β =
+    preserves-neighborhood-map-isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+      ( isometry-metric-quotient-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P))
+      ( α +ℚ⁺ β +ℚ⁺ d)
+      ( const-cauchy-approximation-Pseudometric-Space
+        ( P)
+        ( map-cauchy-approximation-Pseudometric-Space P u α))
+      ( u)
+      ( λ ε δ →
+        monotonic-neighborhood-Pseudometric-Space
+          ( P)
+          ( map-cauchy-approximation-Pseudometric-Space P u α)
+          ( map-cauchy-approximation-Pseudometric-Space P u δ)
+          ( α +ℚ⁺ δ)
+          ( ( ε +ℚ⁺ δ) +ℚ⁺ (α +ℚ⁺ β +ℚ⁺ d))
+          ( lemma-le α δ ε β d)
+          ( is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space
+            ( P)
+            ( u)
+            ( α)
+            ( δ)))
+      where
+
+      lemma-le :
+        (a b c d e : ℚ⁺) →
+        le-ℚ⁺
+          ( a +ℚ⁺ b)
+          ( (c +ℚ⁺ b) +ℚ⁺ (a +ℚ⁺ d +ℚ⁺ e))
+      lemma-le a b c d e =
+        tr
+          ( λ u → le-ℚ⁺ u ((c +ℚ⁺ b) +ℚ⁺ (a +ℚ⁺ d +ℚ⁺ e)))
+          ( commutative-add-ℚ⁺ b a)
+          ( preserves-le-add-ℚ
+            { rational-ℚ⁺ b}
+            { rational-ℚ⁺ (c +ℚ⁺ b)}
+            { rational-ℚ⁺ a}
+            { rational-ℚ⁺ (a +ℚ⁺ d +ℚ⁺ e)}
+            ( le-right-add-ℚ⁺ c b)
+            ( transitive-le-ℚ⁺
+              ( a)
+              ( a +ℚ⁺ d)
+              ( a +ℚ⁺ d +ℚ⁺ e)
+              ( le-left-add-ℚ⁺ (a +ℚ⁺ d) e)
+              ( le-left-add-ℚ⁺ a d)))
+
+  is-limit-map-isometry-cauchy-pseudocompletion-cauchy-precompletion-Pseudometric-Space :
+    is-limit-cauchy-approximation-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space
+        ( P)
+        ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+        ( isometry-cauchy-precompletion-Pseudometric-Space P)
+        ( u))
+      ( map-metric-quotient-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( u))
+  is-limit-map-isometry-cauchy-pseudocompletion-cauchy-precompletion-Pseudometric-Space
+    =
+    is-limit-sim-const-cauchy-approximation-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space
+        ( P)
+        ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+        ( isometry-cauchy-precompletion-Pseudometric-Space P)
+        ( u))
+      ( map-isometry-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+        ( isometry-cauchy-precompletion-cauchy-pseudocompletion-Pseudometric-Space
+          ( P))
+        ( u))
+      ( sim-const-map-isometry-cauchy-precompletion-Pseudometric-Space)
+```
+
+### Any point of the Cauchy precompletion is the limit of the image of a Cauchy approximation
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  where
+
+  is-limit-is-in-class-cauchy-precompletion-Pseudometric-Space :
+    (X : type-cauchy-precompletion-Pseudometric-Space P) →
+    (x : cauchy-approximation-Pseudometric-Space P) →
+    is-in-class-metric-quotient-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( X)
+      ( x) →
+    is-limit-cauchy-approximation-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space
+        ( P)
+        ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+        ( isometry-cauchy-precompletion-Pseudometric-Space P)
+        ( x))
+      ( X)
+  is-limit-is-in-class-cauchy-precompletion-Pseudometric-Space X x x∈X =
+    tr
+      ( is-limit-cauchy-approximation-Metric-Space
+        ( cauchy-precompletion-Pseudometric-Space P)
+        ( map-cauchy-approximation-isometry-Pseudometric-Space
+          ( P)
+          ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+          ( isometry-cauchy-precompletion-Pseudometric-Space P)
+          ( x)))
+      ( eq-map-is-in-class-metric-quotient-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( X)
+        ( x∈X))
+      ( is-limit-map-isometry-cauchy-pseudocompletion-cauchy-precompletion-Pseudometric-Space
+        ( P)
+        ( x))
+```
+
+### The limit in the Cauchy precompletion of a Cauchy approximation in a Pseudometric space is its quotient
+
+```agda
+module _
+  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
+  (u : cauchy-approximation-Pseudometric-Space P)
+  where
+
+  eq-map-quotient-lim-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space :
+    ( lim-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+      ( P)
+      ( u)) ＝
+    ( map-metric-quotient-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( u))
+  eq-map-quotient-lim-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+    =
+    all-eq-is-limit-cauchy-approximation-Metric-Space
+      ( cauchy-precompletion-Pseudometric-Space P)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space
+        ( P)
+        ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+        ( isometry-cauchy-precompletion-Pseudometric-Space P)
+        ( u))
+      ( lim-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+        ( P)
+        ( u))
+      ( map-metric-quotient-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( u))
+      ( is-limit-lim-map-isometry-cauchy-approximation-cauchy-precompletion-Pseudometric-Space
+        ( P)
+        ( u))
+      ( is-limit-map-isometry-cauchy-pseudocompletion-cauchy-precompletion-Pseudometric-Space
+        ( P)
+        ( u))
+```
+
+-- TODO
+
+-- ### If ACC holds then cauchy precompletions are complete
diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md
index 9dad3ad654..2cdba77681 100644
--- a/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md
+++ b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md
@@ -437,3 +437,103 @@ module _
       ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u)
       ( is-limit-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u)
 ```
+
+### The isometry from the Cauchy pseudocompletion of a complete metric space to its limit
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  (is-complete-M : is-complete-Metric-Space M)
+  where
+
+  abstract
+    reflects-neighborhood-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space :
+      (δ : ℚ⁺) →
+      (u v : cauchy-approximation-Metric-Space M) →
+      neighborhood-Metric-Space
+        ( M)
+        ( δ)
+        ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( M)
+          ( is-complete-M)
+          ( u))
+        ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( M)
+          ( is-complete-M)
+          ( v)) →
+      neighborhood-Pseudometric-Space
+        ( cauchy-pseudocompletion-Metric-Space M)
+        ( δ)
+        ( u)
+        ( v)
+    reflects-neighborhood-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+      δ x y Nδ =
+      reflects-neighborhood-sim-Pseudometric-Space
+        ( cauchy-pseudocompletion-Metric-Space M)
+          { x}
+          { const-cauchy-approximation-Metric-Space
+            ( M)
+            ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+              ( M)
+              ( is-complete-M)
+              ( x))}
+          { y}
+          { const-cauchy-approximation-Metric-Space
+            ( M)
+            ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+              ( M)
+              ( is-complete-M)
+              ( y))}
+        ( sim-const-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( M)
+          ( is-complete-M)
+          ( x))
+        ( sim-const-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( M)
+          ( is-complete-M)
+          ( y))
+        ( δ)
+        ( preserves-neighborhood-map-isometry-Pseudometric-Space
+          ( pseudometric-Metric-Space M)
+          ( cauchy-pseudocompletion-Metric-Space M)
+          ( isometry-cauchy-pseudocompletion-Metric-Space M)
+          ( δ)
+          ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+            ( M)
+            ( is-complete-M)
+            ( x))
+          ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+            ( M)
+            ( is-complete-M)
+            ( y))
+          ( Nδ))
+
+    is-isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space :
+      is-isometry-Pseudometric-Space
+        ( cauchy-pseudocompletion-Metric-Space M)
+        ( pseudometric-Metric-Space M)
+        ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( M)
+          ( is-complete-M))
+    is-isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space d x y =
+      ( ( is-short-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( M)
+          ( is-complete-M)
+          ( d)
+          ( x)
+          ( y)) ,
+        ( reflects-neighborhood-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( d)
+          ( x)
+          ( y)))
+
+  isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space :
+    isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Metric-Space M)
+      ( pseudometric-Metric-Space M)
+  isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space =
+    ( ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+        ( M)
+        ( is-complete-M)) ,
+      ( is-isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space))
+```
diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md
index 5bc301fcc1..d4b849e877 100644
--- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md
+++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md
@@ -412,6 +412,64 @@ module _
         ( λ d → H d α β)
 ```
 
+### Similarity in the Cauchy pseudocompletion preserves and reflects limits
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  (u v : cauchy-approximation-Pseudometric-Space M)
+  (x : type-Pseudometric-Space M)
+  where
+
+  has-same-limit-sim-cauchy-approximation-Pseudometric-Space :
+    sim-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space M)
+      ( u)
+      ( v) →
+    is-limit-cauchy-approximation-Pseudometric-Space M u x →
+    is-limit-cauchy-approximation-Pseudometric-Space M v x
+  has-same-limit-sim-cauchy-approximation-Pseudometric-Space u~v lim-u =
+    is-limit-sim-const-cauchy-approximation-Pseudometric-Space
+      ( M)
+      ( v)
+      ( x)
+      ( transitive-sim-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( v)
+        ( u)
+        ( const-cauchy-approximation-Pseudometric-Space M x)
+        ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+          ( M)
+          ( u)
+          ( x)
+          ( lim-u))
+        ( inv-sim-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M)
+          ( u~v)))
+
+  sim-has-same-limit-cauchy-approximation-Pseudometric-Space :
+    is-limit-cauchy-approximation-Pseudometric-Space M u x →
+    is-limit-cauchy-approximation-Pseudometric-Space M v x →
+    sim-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space M)
+      ( u)
+      ( v)
+  sim-has-same-limit-cauchy-approximation-Pseudometric-Space lim-u lim-v =
+    transitive-sim-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space M)
+      ( u)
+      ( const-cauchy-approximation-Pseudometric-Space M x)
+      ( v)
+      ( inv-sim-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+          ( M)
+          ( v)
+          ( x)
+          ( lim-v)))
+      ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space M u x lim-u)
+```
+
 ### Any Cauchy approximation in the Cauchy pseudocompletion of a pseudometric space has a limit
 
 ```agda
@@ -772,12 +830,12 @@ module _
   (f : short-function-Pseudometric-Space A B)
   where
 
-  is-short-map-short-function-cauchy-approximation-Pseudometric-Space :
+  is-short-map-cauchy-approximation-short-function-Pseudometric-Space :
     is-short-function-Pseudometric-Space
       ( cauchy-pseudocompletion-Pseudometric-Space A)
       ( cauchy-pseudocompletion-Pseudometric-Space B)
-      ( map-short-function-cauchy-approximation-Pseudometric-Space A B f)
-  is-short-map-short-function-cauchy-approximation-Pseudometric-Space
+      ( map-cauchy-approximation-short-function-Pseudometric-Space A B f)
+  is-short-map-cauchy-approximation-short-function-Pseudometric-Space
     d x y Nxy α β =
     is-short-map-short-function-Pseudometric-Space A B f
       ( α +ℚ⁺ β +ℚ⁺ d)
@@ -785,13 +843,95 @@ module _
       ( map-cauchy-approximation-Pseudometric-Space A y β)
       ( Nxy α β)
 
-  short-map-short-function-cauchy-approximation-Pseudometric-Space :
+  short-map-cauchy-approximation-short-function-Pseudometric-Space :
     short-function-Pseudometric-Space
       ( cauchy-pseudocompletion-Pseudometric-Space A)
       ( cauchy-pseudocompletion-Pseudometric-Space B)
-  short-map-short-function-cauchy-approximation-Pseudometric-Space =
-    ( map-short-function-cauchy-approximation-Pseudometric-Space A B f ,
-      is-short-map-short-function-cauchy-approximation-Pseudometric-Space)
+  short-map-cauchy-approximation-short-function-Pseudometric-Space =
+    ( map-cauchy-approximation-short-function-Pseudometric-Space A B f ,
+      is-short-map-cauchy-approximation-short-function-Pseudometric-Space)
+```
+
+### The action of isometries on Cauchy approximations is an isometry
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
+  (f : isometry-Pseudometric-Space A B)
+  where abstract
+
+  preserves-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space :
+    (d : ℚ⁺) →
+    (x y : cauchy-approximation-Pseudometric-Space A) →
+    neighborhood-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space A)
+      ( d)
+      ( x)
+      ( y) →
+    neighborhood-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space B)
+      ( d)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space A B f x)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space A B f y)
+  preserves-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space =
+    is-short-map-cauchy-approximation-short-function-Pseudometric-Space
+      ( A)
+      ( B)
+      ( short-isometry-Pseudometric-Space A B f)
+
+  reflects-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space :
+    (d : ℚ⁺) →
+    (x y : cauchy-approximation-Pseudometric-Space A) →
+    neighborhood-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space B)
+      ( d)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space A B f x)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space A B f y) →
+    neighborhood-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space A)
+      ( d)
+      ( x)
+      ( y)
+  reflects-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space
+    d x y Nxy α β =
+    reflects-neighborhood-map-isometry-Pseudometric-Space
+      ( A)
+      ( B)
+      ( f)
+      ( α +ℚ⁺ β +ℚ⁺ d)
+      ( map-cauchy-approximation-Pseudometric-Space A x α)
+      ( map-cauchy-approximation-Pseudometric-Space A y β)
+      ( Nxy α β)
+
+  is-isometry-map-cauchy-approximation-isometry-Pseudometric-Space :
+    is-isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space A)
+      ( cauchy-pseudocompletion-Pseudometric-Space B)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space A B f)
+  is-isometry-map-cauchy-approximation-isometry-Pseudometric-Space d x y =
+    ( ( preserves-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space
+        ( d)
+        ( x)
+        ( y)) ,
+      ( reflects-neighborhood-map-cauchy-approximation-isometry-Pseudometric-Space
+        ( d)
+        ( x)
+        ( y)))
+
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
+  (f : isometry-Pseudometric-Space A B)
+  where
+
+  isometry-map-cauchy-approximation-isometry-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space A)
+      ( cauchy-pseudocompletion-Pseudometric-Space B)
+  isometry-map-cauchy-approximation-isometry-Pseudometric-Space =
+    ( map-cauchy-approximation-isometry-Pseudometric-Space A B f ,
+      is-isometry-map-cauchy-approximation-isometry-Pseudometric-Space A B f)
 ```
 
 ### The image of a Cauchy approximation in the Cauchy pseudocompletion is convergent
@@ -805,7 +945,7 @@ module _
   is-limit-map-cauchy-approximation-cauchy-pseudocompletion-Ppseudometric-Space :
     is-limit-cauchy-approximation-Pseudometric-Space
       ( cauchy-pseudocompletion-Pseudometric-Space M)
-      ( map-short-function-cauchy-approximation-Pseudometric-Space
+      ( map-cauchy-approximation-short-function-Pseudometric-Space
         ( M)
         ( cauchy-pseudocompletion-Pseudometric-Space M)
         ( short-map-cauchy-pseudocompletion-Pseudometric-Space M)
@@ -839,7 +979,7 @@ module _
     sim-Pseudometric-Space
       ( cauchy-pseudocompletion-Pseudometric-Space
         ( cauchy-pseudocompletion-Pseudometric-Space M))
-      ( map-short-function-cauchy-approximation-Pseudometric-Space
+      ( map-cauchy-approximation-short-function-Pseudometric-Space
         ( M)
         ( cauchy-pseudocompletion-Pseudometric-Space M)
         ( short-map-cauchy-pseudocompletion-Pseudometric-Space M)
@@ -850,7 +990,7 @@ module _
   sim-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space =
     sim-const-is-limit-cauchy-approximation-Pseudometric-Space
       ( cauchy-pseudocompletion-Pseudometric-Space M)
-      ( map-short-function-cauchy-approximation-Pseudometric-Space
+      ( map-cauchy-approximation-short-function-Pseudometric-Space
         ( M)
         ( cauchy-pseudocompletion-Pseudometric-Space M)
         ( short-map-cauchy-pseudocompletion-Pseudometric-Space M)
diff --git a/src/metric-spaces/complete-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/complete-metric-extensions-of-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..12f8df9499
--- /dev/null
+++ b/src/metric-spaces/complete-metric-extensions-of-pseudometric-spaces.lagda.md
@@ -0,0 +1,164 @@
+# Complete metric extensions of pseudometric spaces
+
+```agda
+module metric-spaces.complete-metric-extensions-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.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.cauchy-precompletion-of-pseudometric-spaces
+open import metric-spaces.cauchy-pseudocompletion-of-metric-spaces
+open import metric-spaces.cauchy-pseudocompletion-of-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-extensions-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-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
+
+A [metric extension](metric-spaces.metric-extensions-of-pseudometric-spaces.md)
+is
+{{#concept "complete" Disambiguation="metric extension of a pseudometric space Agda=Complete-Metric-Extension}}
+if its target [metric space](metric-spaces.metric-spaces.md) is
+[complete](metric-spaces.complete-metric-spaces.md).
+
+## Definition
+
+### The property of being a complete metric extension
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (P : Pseudometric-Space l1 l2)
+  (M : Metric-Extension l3 l4 P)
+  where
+
+  is-complete-prop-Metric-Extension : Prop (l3 ⊔ l4)
+  is-complete-prop-Metric-Extension =
+    is-complete-prop-Metric-Space (metric-space-Metric-Extension P M)
+
+  is-complete-Metric-Extension : UU (l3 ⊔ l4)
+  is-complete-Metric-Extension =
+    type-Prop is-complete-prop-Metric-Extension
+
+  is-prop-is-complete-Metric-Extension : is-prop is-complete-Metric-Extension
+  is-prop-is-complete-Metric-Extension =
+    is-prop-type-Prop is-complete-prop-Metric-Extension
+```
+
+### The type of complete metric extensions of a pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level}
+  (l3 l4 : Level)
+  (P : Pseudometric-Space l1 l2)
+  where
+
+  Complete-Metric-Extension : UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4)
+  Complete-Metric-Extension =
+    Σ ( Metric-Extension l3 l4 P)
+      ( is-complete-Metric-Extension P)
+
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Pseudometric-Space l1 l2)
+  (M : Complete-Metric-Extension l3 l4 P)
+  where
+
+  metric-extension-Complete-Meric-Extension : Metric-Extension l3 l4 P
+  metric-extension-Complete-Meric-Extension = pr1 M
+
+  metric-space-Complete-Metric-Extension : Metric-Space l3 l4
+  metric-space-Complete-Metric-Extension =
+    metric-space-Metric-Extension P metric-extension-Complete-Meric-Extension
+
+  type-metric-space-Complete-Metric-Extension : UU l3
+  type-metric-space-Complete-Metric-Extension =
+    type-metric-space-Metric-Extension
+      ( P)
+      ( metric-extension-Complete-Meric-Extension)
+
+  is-complete-metric-space-Complete-Metric-Extension :
+    is-complete-Metric-Space metric-space-Complete-Metric-Extension
+  is-complete-metric-space-Complete-Metric-Extension = pr2 M
+
+  complete-metric-space-Complete-Metric-Extension : Complete-Metric-Space l3 l4
+  complete-metric-space-Complete-Metric-Extension =
+    ( metric-space-Complete-Metric-Extension ,
+      is-complete-metric-space-Complete-Metric-Extension)
+
+  isometry-Complete-Metric-Extension :
+    isometry-Pseudometric-Space
+      ( P)
+      ( pseudometric-Metric-Space metric-space-Complete-Metric-Extension)
+  isometry-Complete-Metric-Extension =
+    isometry-Metric-Extension P metric-extension-Complete-Meric-Extension
+```
+
+## Properties
+
+### A complete metric extension of a pseudometric space induces a complete metric extension of its Cauchy precompletion
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Pseudometric-Space l1 l2)
+  (M : Complete-Metric-Extension l3 l4 P)
+  where
+
+  map-complete-metric-extension-cauchy-precompletion-Pseudometric-Space :
+    Complete-Metric-Extension l3 l4
+      ( pseudometric-cauchy-precompletion-Pseudometric-Space P)
+  pr1 map-complete-metric-extension-cauchy-precompletion-Pseudometric-Space =
+    ( ( metric-space-Complete-Metric-Extension P M) ,
+      ( isometry-map-isometry-complete-metric-space-cauchy-precompletion-Pseudometric-Space
+        ( P)
+        ( complete-metric-space-Complete-Metric-Extension P M)
+        ( isometry-Complete-Metric-Extension P M)))
+  pr2 map-complete-metric-extension-cauchy-precompletion-Pseudometric-Space =
+    is-complete-metric-space-Complete-Metric-Extension P M
+```
diff --git a/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..b0dc1d57f3
--- /dev/null
+++ b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md
@@ -0,0 +1,238 @@
+# Metric extensions of pseudometric spaces
+
+```agda
+module metric-spaces.metric-extensions-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.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.cauchy-pseudocompletion-of-metric-spaces
+open import metric-spaces.cauchy-pseudocompletion-of-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-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-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
+
+A
+{{#concept "metric extension" Disambiguation="of a pseudometric space" Agda=Metric-Extension}}
+of a [pseudometric space](metric-spaces.pseudometric-spaces.md) `P` is a
+[metric space](metric-spaces.metric-spaces.md) `M` together with an
+[isometry](metric-spaces.isometries-pseudometric-spaces.md) `f : P → M`.
+
+## Definition
+
+### Metric extensions of pseudometric spaces
+
+```agda
+module _
+  {l1 l2 : Level} (l3 l4 : Level) (P : Pseudometric-Space l1 l2)
+  where
+
+  Metric-Extension : UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4)
+  Metric-Extension =
+    Σ ( Metric-Space l3 l4)
+      ( isometry-Pseudometric-Space P ∘ pseudometric-Metric-Space)
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (P : Pseudometric-Space l1 l2)
+  (M : Metric-Extension l3 l4 P)
+  where
+
+  metric-space-Metric-Extension : Metric-Space l3 l4
+  metric-space-Metric-Extension = pr1 M
+
+  pseudometric-space-Metric-Extension : Pseudometric-Space l3 l4
+  pseudometric-space-Metric-Extension =
+    pseudometric-Metric-Space metric-space-Metric-Extension
+
+  type-metric-space-Metric-Extension : UU l3
+  type-metric-space-Metric-Extension =
+    type-Metric-Space metric-space-Metric-Extension
+
+  isometry-Metric-Extension :
+    isometry-Pseudometric-Space P pseudometric-space-Metric-Extension
+  isometry-Metric-Extension = pr2 M
+```
+
+## Properties
+
+### Action of metric extensions on Cauchy approximations
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (P : Pseudometric-Space l1 l2)
+  (M : Metric-Extension l3 l4 P)
+  where
+
+  isometry-metric-extension-cauchy-approximation-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-pseudocompletion-Metric-Space
+        ( metric-space-Metric-Extension P M))
+  isometry-metric-extension-cauchy-approximation-Pseudometric-Space =
+    isometry-map-cauchy-approximation-isometry-Pseudometric-Space
+      ( P)
+      ( pseudometric-space-Metric-Extension P M)
+      ( isometry-Metric-Extension P M)
+
+  map-metric-extension-cauchy-approximation-Pseudometric-Space :
+    cauchy-approximation-Pseudometric-Space P →
+    cauchy-approximation-Metric-Space
+      ( metric-space-Metric-Extension P M)
+  map-metric-extension-cauchy-approximation-Pseudometric-Space =
+    map-isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-pseudocompletion-Metric-Space
+        ( metric-space-Metric-Extension P M))
+      ( isometry-metric-extension-cauchy-approximation-Pseudometric-Space)
+
+  is-isometry-map-metric-extenion-cauchy-approximation-Pseudometric-Space :
+    is-isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-pseudocompletion-Metric-Space
+        ( metric-space-Metric-Extension P M))
+      ( map-metric-extension-cauchy-approximation-Pseudometric-Space)
+  is-isometry-map-metric-extenion-cauchy-approximation-Pseudometric-Space =
+    is-isometry-map-isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-pseudocompletion-Metric-Space
+        ( metric-space-Metric-Extension P M))
+      ( isometry-metric-extension-cauchy-approximation-Pseudometric-Space)
+```
+
+### Adherent points of metric extensions
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Pseudometric-Space l1 l2)
+  (M : Metric-Extension l3 l4 P)
+  (u : cauchy-approximation-Pseudometric-Space P)
+  (y : type-metric-space-Metric-Extension P M)
+  where
+
+  is-limit-map-metric-extension-prop-cauchy-approximation-Pseudometric-Space :
+    Prop l4
+  is-limit-map-metric-extension-prop-cauchy-approximation-Pseudometric-Space =
+    is-limit-cauchy-approximation-prop-Metric-Space
+      ( metric-space-Metric-Extension P M)
+      ( map-metric-extension-cauchy-approximation-Pseudometric-Space P M u)
+      ( y)
+
+  is-limit-map-metric-extension-cauchy-approximation-Pseudometric-Space : UU l4
+  is-limit-map-metric-extension-cauchy-approximation-Pseudometric-Space =
+    type-Prop
+      is-limit-map-metric-extension-prop-cauchy-approximation-Pseudometric-Space
+```
+
+### Cauchy approximations converging to the same image in a metric extension are similar in the Cauchy pseudocompletion
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Pseudometric-Space l1 l2)
+  (M : Metric-Extension l3 l4 P)
+  (y : type-metric-space-Metric-Extension P M)
+  (u v : cauchy-approximation-Pseudometric-Space P)
+  where
+
+  lemma-sim-is-limit-map-metric-extension-cauchy-approximation-Pseudometric-Space :
+    is-limit-map-metric-extension-cauchy-approximation-Pseudometric-Space
+      ( P)
+      ( M)
+      ( u)
+      ( y) →
+    is-limit-map-metric-extension-cauchy-approximation-Pseudometric-Space
+      ( P)
+      ( M)
+      ( v)
+      ( y) →
+    sim-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( u)
+      ( v)
+  lemma-sim-is-limit-map-metric-extension-cauchy-approximation-Pseudometric-Space
+    lim-u lim-v =
+    reflects-sim-map-isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-pseudocompletion-Metric-Space
+        ( metric-space-Metric-Extension P M))
+      ( isometry-metric-extension-cauchy-approximation-Pseudometric-Space P M)
+      ( u)
+      ( v)
+      ( transitive-sim-Pseudometric-Space
+        ( cauchy-pseudocompletion-Metric-Space
+          ( metric-space-Metric-Extension P M))
+        ( map-metric-extension-cauchy-approximation-Pseudometric-Space P M u)
+        ( const-cauchy-approximation-Metric-Space
+          ( metric-space-Metric-Extension P M)
+          ( y))
+        ( map-metric-extension-cauchy-approximation-Pseudometric-Space P M v)
+        ( symmetric-sim-Pseudometric-Space
+          ( cauchy-pseudocompletion-Metric-Space
+            ( metric-space-Metric-Extension P M))
+          ( map-metric-extension-cauchy-approximation-Pseudometric-Space P M v)
+          ( const-cauchy-approximation-Metric-Space
+            ( metric-space-Metric-Extension P M)
+            ( y))
+          ( sim-const-is-limit-cauchy-approximation-Metric-Space
+            ( metric-space-Metric-Extension P M)
+            ( map-metric-extension-cauchy-approximation-Pseudometric-Space
+              ( P)
+              ( M)
+              ( v))
+            ( y)
+            ( lim-v)))
+        ( sim-const-is-limit-cauchy-approximation-Metric-Space
+          ( metric-space-Metric-Extension P M)
+          ( map-metric-extension-cauchy-approximation-Pseudometric-Space P M u)
+          ( y)
+          ( lim-u)))
+```
diff --git a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md
index ffecd0aafc..3f48274856 100644
--- a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md
+++ b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md
@@ -386,6 +386,20 @@ module _
   map-subtype-metric-quotient-Pseudometric-Space =
     inhabitant-equivalence-class-quotient-map-set-quotient
       ( equivalence-relation-sim-Pseudometric-Space M)
+
+  eq-map-is-in-class-metric-quotient-Pseudometric-Space :
+    (X : type-metric-quotient-Pseudometric-Space M) →
+    {x : type-Pseudometric-Space M} →
+    is-in-class-metric-quotient-Pseudometric-Space
+      ( M)
+      ( X)
+      ( x) →
+    map-metric-quotient-Pseudometric-Space x ＝ X
+  eq-map-is-in-class-metric-quotient-Pseudometric-Space X {x} x∈X =
+    eq-set-quotient-equivalence-class-set-quotient
+      ( equivalence-relation-sim-Pseudometric-Space M)
+      ( X)
+      ( x∈X)
 ```
 
 ### The mapping from a pseudometric space its quotient metric space is an isometry
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 f9caa041d2..168c7d6710 100644
--- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md
+++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md
@@ -22,6 +22,7 @@ open import foundation.propositions
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
+open import metric-spaces.isometries-pseudometric-spaces
 open import metric-spaces.pseudometric-spaces
 open import metric-spaces.rational-neighborhood-relations
 open import metric-spaces.short-functions-pseudometric-spaces
@@ -314,15 +315,34 @@ module _
   ( A : Pseudometric-Space l1 l2)
   ( B : Pseudometric-Space l1' l2')
   ( f : short-function-Pseudometric-Space A B)
-  where
+  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)
+```
 
-  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)
+### Isometries between pseudometric spaces reflect similarity
+
+```agda
+module _
+  { l1 l2 l1' l2' : Level}
+  ( A : Pseudometric-Space l1 l2)
+  ( B : Pseudometric-Space l1' l2')
+  ( f : isometry-Pseudometric-Space A B)
+  where abstract
+
+  reflects-sim-map-isometry-Pseudometric-Space :
+    ( x y : type-Pseudometric-Space A) →
+    ( sim-Pseudometric-Space B
+      ( map-isometry-Pseudometric-Space A B f x)
+      ( map-isometry-Pseudometric-Space A B f y)) →
+    ( sim-Pseudometric-Space A x y)
+  reflects-sim-map-isometry-Pseudometric-Space x y fx~fy d =
+    reflects-neighborhood-map-isometry-Pseudometric-Space A B f d x y (fx~fy d)
 ```