diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md
index bc48c2ee7e7..ee5c43ff9ae 100644
--- a/src/metric-spaces.lagda.md
+++ b/src/metric-spaces.lagda.md
@@ -97,6 +97,7 @@ open import metric-spaces.images-uniformly-continuous-functions-metric-spaces pu
 open import metric-spaces.indexed-sums-metric-spaces public
 open import metric-spaces.inhabited-totally-bounded-subspaces-metric-spaces public
 open import metric-spaces.interior-subsets-metric-spaces public
+open import metric-spaces.isometries-between-metric-extensions-of-pseudometric-spaces public
 open import metric-spaces.isometries-metric-spaces public
 open import metric-spaces.isometries-pseudometric-spaces public
 open import metric-spaces.limits-of-cauchy-approximations-metric-spaces public
@@ -106,6 +107,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/bounded-distance-decompositions-of-metric-spaces.lagda.md b/src/metric-spaces/bounded-distance-decompositions-of-metric-spaces.lagda.md
index ea2bf3aa077..57bdd01bc5a 100644
--- a/src/metric-spaces/bounded-distance-decompositions-of-metric-spaces.lagda.md
+++ b/src/metric-spaces/bounded-distance-decompositions-of-metric-spaces.lagda.md
@@ -213,7 +213,7 @@ module _
   {l1 l2 : Level} (A : Metric-Space l1 l2)
   where
 
-  preserves-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space :
+  preserves-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space :
     ( d : ℚ⁺)
     ( x y : type-bounded-distance-decomposition-Metric-Space A) →
     neighborhood-Metric-Space
@@ -224,7 +224,7 @@ module _
     neighborhood-Metric-Space A d
       ( map-equiv-bounded-distance-decomposition-Metric-Space A x)
       ( map-equiv-bounded-distance-decomposition-Metric-Space A y)
-  preserves-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space
+  preserves-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space
     d (X , x , x∈X) (Y , y , y∈Y) (X=Y , Nxy) =
     forward-implication
       ( lemma-iff-neighborhood-bounded-distance-decomposition-Metric-Space
@@ -237,7 +237,7 @@ module _
         ( y , y∈Y))
       ( Nxy)
 
-  reflects-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space :
+  reflects-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space :
     ( d : ℚ⁺)
     ( x y : type-bounded-distance-decomposition-Metric-Space A) →
     neighborhood-Metric-Space A d
@@ -248,7 +248,7 @@ module _
       ( d)
       ( x)
       ( y)
-  reflects-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space
+  reflects-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space
     d (X , x , x∈X) (Y , y , y∈Y) Nxy =
     ( lemma-eq ,
       backward-implication
@@ -280,11 +280,11 @@ module _
       ( map-equiv-bounded-distance-decomposition-Metric-Space A)
   is-isometry-map-equiv-bounded-distance-decomposition-Metric-Space
     d x y =
-    ( ( preserves-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space
+    ( ( preserves-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space
         ( d)
         ( x)
         ( y)) ,
-      ( reflects-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space
+      ( reflects-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space
         ( d)
         ( x)
         ( y)))
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 9184f29af6a..b5ce744455e 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)
@@ -233,7 +233,7 @@ module _
           ( x)
           ( x∈uε)
     in
-      preserves-neighborhood-sim-Pseudometric-Space
+      preserves-neighborhoods-sim-Pseudometric-Space
         ( M)
         ( uε~x)
         ( lim~y)
diff --git a/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md
index caf5ee3d31c..e48cfc33262 100644
--- a/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md
+++ b/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md
@@ -10,9 +10,6 @@ module metric-spaces.cauchy-approximations-metric-spaces where
 open import elementary-number-theory.addition-positive-rational-numbers
 open import elementary-number-theory.positive-rational-numbers
 
-open import foundation.constant-maps
-open import foundation.dependent-pair-types
-open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
@@ -20,7 +17,6 @@ open import foundation.propositions
 open import foundation.subtypes
 open import foundation.universe-levels
 
-open import metric-spaces.cartesian-products-metric-spaces
 open import metric-spaces.cauchy-approximations-pseudometric-spaces
 open import metric-spaces.metric-spaces
 open import metric-spaces.short-functions-metric-spaces
@@ -123,7 +119,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)
@@ -137,7 +133,7 @@ module _
     map-short-function-cauchy-approximation-Metric-Space
       ( A)
       ( A)
-      ( short-id-Metric-Space A) ＝
+      ( id-short-function-Metric-Space A) ＝
     id
   eq-id-map-short-function-cauchy-approximation-Metric-Space = refl
 
diff --git a/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md
index 3f7b863d422..b6b0b62a391 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-pseudocompletion-of-metric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md
index 9dad3ad6549..802663a17b7 100644
--- a/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md
+++ b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md
@@ -9,17 +9,13 @@ module metric-spaces.cauchy-pseudocompletion-of-metric-spaces where
 ```agda
 open import elementary-number-theory.addition-positive-rational-numbers
 open import elementary-number-theory.positive-rational-numbers
-open import elementary-number-theory.strict-inequality-rational-numbers
 
-open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.binary-relations
-open import foundation.binary-transport
 open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
-open import foundation.propositions
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
@@ -27,7 +23,6 @@ open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.cauchy-approximations-pseudometric-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.functions-pseudometric-spaces
 open import metric-spaces.isometries-pseudometric-spaces
 open import metric-spaces.limits-of-cauchy-approximations-metric-spaces
@@ -354,7 +349,7 @@ module _
         ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space))
   is-short-const-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
     d x y =
-      preserves-neighborhood-sim-Pseudometric-Space
+      preserves-neighborhoods-sim-Pseudometric-Space
         ( cauchy-pseudocompletion-Metric-Space M)
         { x}
         { const-cauchy-approximation-Metric-Space
@@ -437,3 +432,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-neighborhoods-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-neighborhoods-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+      δ x y Nδ =
+      reflects-neighborhoods-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-neighborhoods-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-neighborhoods-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 5bc301fcc11..41506234ff6 100644
--- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md
+++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md
@@ -17,24 +17,16 @@ open import elementary-number-theory.strict-inequality-rational-numbers
 open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.binary-relations
-open import foundation.binary-transport
 open import foundation.dependent-pair-types
 open import foundation.function-types
-open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
-open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.cauchy-approximations-pseudometric-spaces
-open import metric-spaces.complete-metric-spaces
-open import metric-spaces.convergent-cauchy-approximations-metric-spaces
-open import metric-spaces.functions-pseudometric-spaces
 open import metric-spaces.isometries-pseudometric-spaces
-open import metric-spaces.limits-of-cauchy-approximations-metric-spaces
 open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces
-open import metric-spaces.metric-spaces
 open import metric-spaces.pseudometric-spaces
 open import metric-spaces.rational-neighborhood-relations
 open import metric-spaces.short-functions-pseudometric-spaces
@@ -303,7 +295,7 @@ module _
     const-cauchy-approximation-Pseudometric-Space M
 
   abstract
-    preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space :
+    preserves-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space :
       (d : ℚ⁺) (x y : type-Pseudometric-Space M) →
       neighborhood-Pseudometric-Space M d x y →
       neighborhood-cauchy-pseudocompletion-Pseudometric-Space
@@ -311,13 +303,13 @@ module _
         ( d)
         ( map-cauchy-pseudocompletion-Pseudometric-Space x)
         ( map-cauchy-pseudocompletion-Pseudometric-Space y)
-    preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space
+    preserves-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space
       d x y Nxy δ ε =
       monotonic-neighborhood-Pseudometric-Space M x y d (δ +ℚ⁺ ε +ℚ⁺ d)
         ( le-right-add-ℚ⁺ (δ +ℚ⁺ ε) d)
         ( Nxy)
 
-    reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space :
+    reflects-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space :
       (d : ℚ⁺) (x y : type-Pseudometric-Space M) →
       neighborhood-cauchy-pseudocompletion-Pseudometric-Space
         ( M)
@@ -325,7 +317,7 @@ module _
         ( map-cauchy-pseudocompletion-Pseudometric-Space x)
         ( map-cauchy-pseudocompletion-Pseudometric-Space y) →
       neighborhood-Pseudometric-Space M d x y
-    reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space
+    reflects-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space
       d x y Nxy =
       saturated-neighborhood-Pseudometric-Space M d x y
         ( λ δ →
@@ -343,11 +335,11 @@ module _
         ( cauchy-pseudocompletion-Pseudometric-Space M)
         ( map-cauchy-pseudocompletion-Pseudometric-Space)
     is-isometry-map-cauchy-pseudocompletion-Pseudometric-Space d x y =
-      ( ( preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space
+      ( ( preserves-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space
           ( d)
           ( x)
           ( y)) ,
-        (reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space
+        (reflects-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space
           ( d)
           ( x)
           ( y)))
@@ -412,6 +404,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
@@ -616,7 +666,7 @@ module _
             ( M)))
     is-short-function-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
       d u v =
-      preserves-neighborhood-sim-Pseudometric-Space
+      preserves-neighborhoods-sim-Pseudometric-Space
         ( cauchy-pseudocompletion-Pseudometric-Space
           ( cauchy-pseudocompletion-Pseudometric-Space M))
         { u}
@@ -647,7 +697,7 @@ module _
         ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M)
     is-short-function-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space
       d u v Nuv =
-      reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space
+      reflects-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space
         ( cauchy-pseudocompletion-Pseudometric-Space M)
         ( d)
         ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
@@ -680,7 +730,7 @@ module _
   where
 
   abstract
-    reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+    reflects-neighborhoods-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
       ( d : ℚ⁺) →
       ( u v :
         cauchy-approximation-Pseudometric-Space
@@ -700,9 +750,9 @@ module _
         ( d)
         ( u)
         ( v)
-    reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+    reflects-neighborhoods-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
       d u v N-lim =
-      reflects-neighborhood-sim-Pseudometric-Space
+      reflects-neighborhoods-sim-Pseudometric-Space
         ( cauchy-pseudocompletion-Pseudometric-Space
           ( cauchy-pseudocompletion-Pseudometric-Space M))
         { u}
@@ -724,7 +774,7 @@ module _
           ( M)
           ( v))
         ( d)
-        ( preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space
+        ( preserves-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space
           ( cauchy-pseudocompletion-Pseudometric-Space M)
           ( d)
           ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
@@ -748,7 +798,7 @@ module _
           ( d)
           ( x)
           ( y)) ,
-        ( reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+        ( reflects-neighborhoods-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
           ( d)
           ( x)
           ( y)))
@@ -772,12 +822,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 +835,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-neighborhoods-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-neighborhoods-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-neighborhoods-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-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space
+    d x y Nxy α β =
+    reflects-neighborhoods-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-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space
+        ( d)
+        ( x)
+        ( y)) ,
+      ( reflects-neighborhoods-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 +937,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 +971,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 +982,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/indexed-sums-metric-spaces.lagda.md b/src/metric-spaces/indexed-sums-metric-spaces.lagda.md
index 4ed15b71da2..c07e513fe37 100644
--- a/src/metric-spaces/indexed-sums-metric-spaces.lagda.md
+++ b/src/metric-spaces/indexed-sums-metric-spaces.lagda.md
@@ -295,7 +295,7 @@ module _
     ( map-emb-fiber-indexed-sum-Metric-Space A P x ,
       is-short-emb-fiber-indexed-sum-Metric-Space)
 
-  reflects-neighborhood-emb-fiber-indexed-sum-Metric-Space :
+  reflects-neighborhoods-emb-fiber-indexed-sum-Metric-Space :
     (d : ℚ⁺) (px px' : type-Metric-Space (P x)) →
     neighborhood-Metric-Space
       ( indexed-sum-Metric-Space A P)
@@ -307,7 +307,8 @@ module _
       ( d)
       ( px)
       ( px')
-  reflects-neighborhood-emb-fiber-indexed-sum-Metric-Space d px px' (e , Nxx') =
+  reflects-neighborhoods-emb-fiber-indexed-sum-Metric-Space
+    d px px' (e , Nxx') =
     inv-tr
       ( λ e' →
         neighborhood-Metric-Space
@@ -328,7 +329,7 @@ module _
       ( map-emb-fiber-indexed-sum-Metric-Space A P x)
   is-isometry-emb-fiber-indexed-sum-Metric-Space d px px' =
     ( is-short-emb-fiber-indexed-sum-Metric-Space d px px' ,
-      reflects-neighborhood-emb-fiber-indexed-sum-Metric-Space d px px')
+      reflects-neighborhoods-emb-fiber-indexed-sum-Metric-Space d px px')
 
   isometry-emb-fiber-indexed-Metric-Space :
     isometry-Metric-Space (P x) (indexed-sum-Metric-Space A P)
diff --git a/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md
new file mode 100644
index 00000000000..411d45fc060
--- /dev/null
+++ b/src/metric-spaces/isometries-between-metric-extensions-of-pseudometric-spaces.lagda.md
@@ -0,0 +1,299 @@
+# Isometries between metric extensions of a pseudometric space
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module metric-spaces.isometries-between-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 foundation.whiskering-homotopies-composition
+
+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
+
+An
+{{#concept "isometry" Disambiguation="between metric extensions of a pseudometric space" Agda=isometry-Metric-Extension}}
+between two
+[metric extensions](metric-spaces.metric-extensions-of-pseudometric-spaces.md)
+of a [pseudometric space](metric-spaces.pseudometric-spaces.md) `P`, `i : P → M`
+and `j : P → N`, is an [isometry](metric-spaces.isometries-metric-spaces.md)
+`f : M → N` such that
+
+```text
+  f ∘ i ~ j.
+```
+
+## Definitions
+
+### The property of being an isometry between metric extensions
+
+```agda
+module _
+  { l1 l2 l3 l4 l5 l6 : Level}
+  ( P : Pseudometric-Space l1 l2)
+  ( M : Metric-Extension l3 l4 P)
+  ( N : Metric-Extension l5 l6 P)
+  ( f :
+    isometry-Metric-Space
+      ( metric-space-Metric-Extension P M)
+      ( metric-space-Metric-Extension P N))
+  where
+
+  coherence-triangle-prop-isometry-metric-space-Metric-Extension :
+    Prop (l1 ⊔ l5)
+  coherence-triangle-prop-isometry-metric-space-Metric-Extension =
+    Π-Prop
+      ( type-Pseudometric-Space P)
+      ( λ x →
+        Id-Prop
+          ( set-Metric-Space
+            ( metric-space-Metric-Extension P N))
+          ( map-isometry-Pseudometric-Space
+            ( P)
+            ( pseudometric-space-Metric-Extension P N)
+            ( comp-isometry-Pseudometric-Space
+              ( P)
+              ( pseudometric-space-Metric-Extension P M)
+              ( pseudometric-space-Metric-Extension P N)
+              ( f)
+              ( isometry-metric-space-Metric-Extension P M))
+            ( x))
+          ( map-isometry-metric-space-Metric-Extension P N x))
+
+  coherence-triangle-isometry-metric-space-Metric-Extension : UU (l1 ⊔ l5)
+  coherence-triangle-isometry-metric-space-Metric-Extension =
+    type-Prop
+      coherence-triangle-prop-isometry-metric-space-Metric-Extension
+
+  is-prop-coherence-triangle-isometry-metric-space-Metric-Extension :
+    is-prop coherence-triangle-isometry-metric-space-Metric-Extension
+  is-prop-coherence-triangle-isometry-metric-space-Metric-Extension =
+    is-prop-type-Prop
+      coherence-triangle-prop-isometry-metric-space-Metric-Extension
+```
+
+### The type of isometries between metric extensions of a pseudometric space
+
+```agda
+module _
+  { l1 l2 l3 l4 l5 l6 : Level}
+  ( P : Pseudometric-Space l1 l2)
+  ( M : Metric-Extension l3 l4 P)
+  ( N : Metric-Extension l5 l6 P)
+  where
+
+  isometry-Metric-Extension : UU (l1 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
+  isometry-Metric-Extension =
+    type-subtype
+      ( coherence-triangle-prop-isometry-metric-space-Metric-Extension P M N)
+
+module _
+  { l1 l2 l3 l4 l5 l6 : Level}
+  ( P : Pseudometric-Space l1 l2)
+  ( M : Metric-Extension l3 l4 P)
+  ( N : Metric-Extension l5 l6 P)
+  ( f : isometry-Metric-Extension P M N)
+  where
+
+  isometry-metric-space-isometry-Metric-Extension :
+    isometry-Metric-Space
+      ( metric-space-Metric-Extension P M)
+      ( metric-space-Metric-Extension P N)
+  isometry-metric-space-isometry-Metric-Extension = pr1 f
+
+  map-metric-space-isometry-Metric-Extension :
+    type-metric-space-Metric-Extension P M →
+    type-metric-space-Metric-Extension P N
+  map-metric-space-isometry-Metric-Extension =
+    map-isometry-Metric-Space
+      ( metric-space-Metric-Extension P M)
+      ( metric-space-Metric-Extension P N)
+      ( isometry-metric-space-isometry-Metric-Extension)
+
+  is-isometry-map-metric-space-isometry-Metric-Extension :
+    is-isometry-Metric-Space
+      ( metric-space-Metric-Extension P M)
+      ( metric-space-Metric-Extension P N)
+      ( map-metric-space-isometry-Metric-Extension)
+  is-isometry-map-metric-space-isometry-Metric-Extension =
+    is-isometry-map-isometry-Metric-Space
+      ( metric-space-Metric-Extension P M)
+      ( metric-space-Metric-Extension P N)
+      ( isometry-metric-space-isometry-Metric-Extension)
+
+  coh-isometry-Metric-Extension :
+    coherence-triangle-isometry-metric-space-Metric-Extension
+      ( P)
+      ( M)
+      ( N)
+      ( isometry-metric-space-isometry-Metric-Extension)
+  coh-isometry-Metric-Extension = pr2 f
+```
+
+## Properties
+
+### Isometries of metric spaces are isometries of metric extensions
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (M : Metric-Space l1 l2)
+  (N : Metric-Space l3 l4)
+  (f : isometry-Metric-Space M N)
+  where
+
+  forgetful-isometry-Metric-Extension :
+    isometry-Metric-Extension
+      ( pseudometric-Metric-Space M)
+      ( forgetful-Metric-Extension M)
+      ( N , f)
+  forgetful-isometry-Metric-Extension = (f , refl-htpy)
+```
+
+### The identity isometry of a metric extension
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Pseudometric-Space l1 l2)
+  (M : Metric-Extension l3 l4 P)
+  where
+
+  id-isometry-Metric-Extension : isometry-Metric-Extension P M M
+  pr1 id-isometry-Metric-Extension =
+    id-isometry-Metric-Space (metric-space-Metric-Extension P M)
+  pr2 id-isometry-Metric-Extension = refl-htpy
+```
+
+### Composition of isometries between metric extensions
+
+```agda
+module _
+  {l l' lu lu' lv lv' lw lw' : Level}
+  (P : Pseudometric-Space l l')
+  (U : Metric-Extension lu lu' P)
+  (V : Metric-Extension lv lv' P)
+  (W : Metric-Extension lw lw' P)
+  (g : isometry-Metric-Extension P V W)
+  (f : isometry-Metric-Extension P U V)
+  where
+
+  abstract
+    coh-comp-isometry-Metric-Extension :
+      coherence-triangle-isometry-metric-space-Metric-Extension P U W
+        ( comp-isometry-Metric-Space
+          ( metric-space-Metric-Extension P U)
+          ( metric-space-Metric-Extension P V)
+          ( metric-space-Metric-Extension P W)
+          ( isometry-metric-space-isometry-Metric-Extension P V W g)
+          ( isometry-metric-space-isometry-Metric-Extension P U V f))
+    coh-comp-isometry-Metric-Extension =
+      ( ( map-metric-space-isometry-Metric-Extension P V W g) ·l
+        ( coh-isometry-Metric-Extension P U V f)) ∙h
+      ( coh-isometry-Metric-Extension P V W g)
+
+  comp-isometry-Metric-Extension : isometry-Metric-Extension P U W
+  pr1 comp-isometry-Metric-Extension =
+    comp-isometry-Metric-Space
+      ( metric-space-Metric-Extension P U)
+      ( metric-space-Metric-Extension P V)
+      ( metric-space-Metric-Extension P W)
+      ( isometry-metric-space-isometry-Metric-Extension P V W g)
+      ( isometry-metric-space-isometry-Metric-Extension P U V f)
+  pr2 comp-isometry-Metric-Extension = coh-comp-isometry-Metric-Extension
+```
+
+### Homotopic isometries between metric extensions are equal
+
+```agda
+module _
+  { l1 l2 l3 l4 l5 l6 : Level}
+  ( P : Pseudometric-Space l1 l2)
+  ( M : Metric-Extension l3 l4 P)
+  ( N : Metric-Extension l5 l6 P)
+  ( f g : isometry-Metric-Extension P M N)
+  where
+
+  htpy-isometry-Metric-Extension : UU (l3 ⊔ l5)
+  htpy-isometry-Metric-Extension =
+    ( map-metric-space-isometry-Metric-Extension P M N f ~
+      map-metric-space-isometry-Metric-Extension P M N g)
+
+  is-prop-htpy-isometry-Metric-Extension :
+    is-prop htpy-isometry-Metric-Extension
+  is-prop-htpy-isometry-Metric-Extension =
+    is-prop-Π
+      ( λ x →
+        is-set-type-Metric-Space
+          ( metric-space-Metric-Extension P N)
+          ( map-metric-space-isometry-Metric-Extension P M N f x)
+          ( map-metric-space-isometry-Metric-Extension P M N g x))
+
+  htpy-prop-isometry-Metric-Extension : Prop (l3 ⊔ l5)
+  htpy-prop-isometry-Metric-Extension =
+    ( htpy-isometry-Metric-Extension , is-prop-htpy-isometry-Metric-Extension)
+
+  eq-htpy-isometry-Metric-Extension :
+    htpy-isometry-Metric-Extension → f ＝ g
+  eq-htpy-isometry-Metric-Extension f~g =
+    eq-type-subtype
+      ( coherence-triangle-prop-isometry-metric-space-Metric-Extension P M N)
+      ( eq-htpy-map-isometry-Metric-Space
+        ( metric-space-Metric-Extension P M)
+        ( metric-space-Metric-Extension P N)
+        ( isometry-metric-space-isometry-Metric-Extension P M N f)
+        ( isometry-metric-space-isometry-Metric-Extension P M N g)
+        ( f~g))
+```
diff --git a/src/metric-spaces/isometries-metric-spaces.lagda.md b/src/metric-spaces/isometries-metric-spaces.lagda.md
index 3fee4dcad8f..92c1c0a3e88 100644
--- a/src/metric-spaces/isometries-metric-spaces.lagda.md
+++ b/src/metric-spaces/isometries-metric-spaces.lagda.md
@@ -125,8 +125,8 @@ module _
     is-isometry-Metric-Space A A (id-Metric-Space A)
   is-isometry-id-Metric-Space d x y = id-iff
 
-  isometry-id-Metric-Space : isometry-Metric-Space A A
-  isometry-id-Metric-Space =
+  id-isometry-Metric-Space : isometry-Metric-Space A A
+  id-isometry-Metric-Space =
     id-Metric-Space A , is-isometry-id-Metric-Space
 ```
 
@@ -171,7 +171,7 @@ module _
   (f : isometry-Metric-Space A B)
   where
 
-  preserves-neighborhood-map-isometry-Metric-Space :
+  preserves-neighborhoods-map-isometry-Metric-Space :
     (d : ℚ⁺) (x y : type-Metric-Space A) →
     neighborhood-Metric-Space A d x y →
     neighborhood-Metric-Space
@@ -179,11 +179,11 @@ module _
       ( d)
       ( map-isometry-Metric-Space A B f x)
       ( map-isometry-Metric-Space A B f y)
-  preserves-neighborhood-map-isometry-Metric-Space d x y =
+  preserves-neighborhoods-map-isometry-Metric-Space d x y =
     forward-implication
       ( is-isometry-map-isometry-Metric-Space A B f d x y)
 
-  reflects-neighborhood-map-isometry-Metric-Space :
+  reflects-neighborhoods-map-isometry-Metric-Space :
     (d : ℚ⁺) (x y : type-Metric-Space A) →
     neighborhood-Metric-Space
       ( B)
@@ -191,7 +191,7 @@ module _
       ( map-isometry-Metric-Space A B f x)
       ( map-isometry-Metric-Space A B f y) →
     neighborhood-Metric-Space A d x y
-  reflects-neighborhood-map-isometry-Metric-Space d x y =
+  reflects-neighborhoods-map-isometry-Metric-Space d x y =
     backward-implication
       ( is-isometry-map-isometry-Metric-Space A B f d x y)
 ```
@@ -238,7 +238,7 @@ module _
 
   left-unit-law-comp-isometry-Metric-Space :
     ( comp-isometry-Metric-Space A B B
-      (isometry-id-Metric-Space B)
+      ( id-isometry-Metric-Space B)
       ( f)) ＝
     ( f)
   left-unit-law-comp-isometry-Metric-Space =
@@ -250,7 +250,7 @@ module _
   right-unit-law-comp-isometry-Metric-Space :
     ( comp-isometry-Metric-Space A A B
       ( f)
-      ( isometry-id-Metric-Space A)) ＝
+      ( id-isometry-Metric-Space A)) ＝
     ( f)
   right-unit-law-comp-isometry-Metric-Space =
     right-unit-law-comp-isometry-Pseudometric-Space
@@ -335,7 +335,7 @@ module _
       B
       f
       isometry-inv-is-equiv-isometry-Metric-Space) ＝
-    ( isometry-id-Metric-Space B)
+    ( id-isometry-Metric-Space B)
   is-section-isometry-inv-is-equiv-isometry-Metric-Space =
     is-section-isometry-inv-is-equiv-isometry-Pseudometric-Space
       ( pseudometric-Metric-Space A)
@@ -350,7 +350,7 @@ module _
       A
       isometry-inv-is-equiv-isometry-Metric-Space
       f) ＝
-    ( isometry-id-Metric-Space A)
+    ( id-isometry-Metric-Space A)
   is-retraction-isometry-inv-is-equiv-isometry-Metric-Space =
     is-retraction-isometry-inv-is-equiv-isometry-Pseudometric-Space
       ( pseudometric-Metric-Space A)
diff --git a/src/metric-spaces/isometries-pseudometric-spaces.lagda.md b/src/metric-spaces/isometries-pseudometric-spaces.lagda.md
index 35d81a521c0..7147daf5c02 100644
--- a/src/metric-spaces/isometries-pseudometric-spaces.lagda.md
+++ b/src/metric-spaces/isometries-pseudometric-spaces.lagda.md
@@ -113,8 +113,8 @@ module _
     is-isometry-Pseudometric-Space A A (id-Pseudometric-Space A)
   is-isometry-id-Pseudometric-Space d x y = id-iff
 
-  isometry-id-Pseudometric-Space : isometry-Pseudometric-Space A A
-  isometry-id-Pseudometric-Space =
+  id-isometry-Pseudometric-Space : isometry-Pseudometric-Space A A
+  id-isometry-Pseudometric-Space =
     ( id-Pseudometric-Space A , is-isometry-id-Pseudometric-Space)
 ```
 
@@ -162,7 +162,7 @@ module _
   (f : isometry-Pseudometric-Space A B)
   where
 
-  preserves-neighborhood-map-isometry-Pseudometric-Space :
+  preserves-neighborhoods-map-isometry-Pseudometric-Space :
     (d : ℚ⁺) (x y : type-Pseudometric-Space A) →
     neighborhood-Pseudometric-Space A d x y →
     neighborhood-Pseudometric-Space
@@ -170,11 +170,11 @@ module _
       ( d)
       ( map-isometry-Pseudometric-Space A B f x)
       ( map-isometry-Pseudometric-Space A B f y)
-  preserves-neighborhood-map-isometry-Pseudometric-Space d x y =
+  preserves-neighborhoods-map-isometry-Pseudometric-Space d x y =
     forward-implication
       ( is-isometry-map-isometry-Pseudometric-Space A B f d x y)
 
-  reflects-neighborhood-map-isometry-Pseudometric-Space :
+  reflects-neighborhoods-map-isometry-Pseudometric-Space :
     (d : ℚ⁺) (x y : type-Pseudometric-Space A) →
     neighborhood-Pseudometric-Space
       ( B)
@@ -182,7 +182,7 @@ module _
       ( map-isometry-Pseudometric-Space A B f x)
       ( map-isometry-Pseudometric-Space A B f y) →
     neighborhood-Pseudometric-Space A d x y
-  reflects-neighborhood-map-isometry-Pseudometric-Space d x y =
+  reflects-neighborhoods-map-isometry-Pseudometric-Space d x y =
     backward-implication
       ( is-isometry-map-isometry-Pseudometric-Space A B f d x y)
 ```
@@ -232,7 +232,7 @@ module _
 
   left-unit-law-comp-isometry-Pseudometric-Space :
     ( comp-isometry-Pseudometric-Space A B B
-      (isometry-id-Pseudometric-Space B)
+      ( id-isometry-Pseudometric-Space B)
       ( f)) ＝
     ( f)
   left-unit-law-comp-isometry-Pseudometric-Space =
@@ -243,7 +243,7 @@ module _
         ( A)
         ( B)
         ( B)
-        (isometry-id-Pseudometric-Space B)
+        ( id-isometry-Pseudometric-Space B)
         ( f))
       ( f)
       ( refl-htpy)
@@ -251,7 +251,7 @@ module _
   right-unit-law-comp-isometry-Pseudometric-Space :
     ( comp-isometry-Pseudometric-Space A A B
       ( f)
-      ( isometry-id-Pseudometric-Space A)) ＝
+      ( id-isometry-Pseudometric-Space A)) ＝
     ( f)
   right-unit-law-comp-isometry-Pseudometric-Space =
     eq-htpy-map-isometry-Pseudometric-Space
@@ -263,7 +263,7 @@ module _
         ( A)
         ( B)
         ( f)
-        ( isometry-id-Pseudometric-Space A))
+        ( id-isometry-Pseudometric-Space A))
       ( refl-htpy)
 ```
 
@@ -357,25 +357,25 @@ module _
     ( comp-isometry-Pseudometric-Space B A B
       ( f)
       ( isometry-inv-is-equiv-isometry-Pseudometric-Space)) ＝
-    ( isometry-id-Pseudometric-Space B)
+    ( id-isometry-Pseudometric-Space B)
   is-section-isometry-inv-is-equiv-isometry-Pseudometric-Space =
     eq-htpy-map-isometry-Pseudometric-Space B B
       ( comp-isometry-Pseudometric-Space B A B
         ( f)
         ( isometry-inv-is-equiv-isometry-Pseudometric-Space))
-      ( isometry-id-Pseudometric-Space B)
+      ( id-isometry-Pseudometric-Space B)
       ( is-section-map-inv-is-equiv E)
 
   is-retraction-isometry-inv-is-equiv-isometry-Pseudometric-Space :
     ( comp-isometry-Pseudometric-Space A B A
       ( isometry-inv-is-equiv-isometry-Pseudometric-Space)
       ( f)) ＝
-    ( isometry-id-Pseudometric-Space A)
+    ( id-isometry-Pseudometric-Space A)
   is-retraction-isometry-inv-is-equiv-isometry-Pseudometric-Space =
     eq-htpy-map-isometry-Pseudometric-Space A A
       ( comp-isometry-Pseudometric-Space A B A
         ( isometry-inv-is-equiv-isometry-Pseudometric-Space)
         ( f))
-      ( isometry-id-Pseudometric-Space A)
+      ( id-isometry-Pseudometric-Space A)
       ( is-retraction-map-inv-is-equiv E)
 ```
diff --git a/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md b/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md
index d9a5fe6ea14..84a29eb976c 100644
--- a/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md
+++ b/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md
@@ -10,12 +10,9 @@ module metric-spaces.limits-of-cauchy-approximations-metric-spaces where
 open import elementary-number-theory.addition-positive-rational-numbers
 open import elementary-number-theory.positive-rational-numbers
 
-open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.identity-types
 open import foundation.propositions
-open import foundation.subtypes
-open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import metric-spaces.cauchy-approximations-metric-spaces
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 00000000000..4868e97993a
--- /dev/null
+++ b/src/metric-spaces/metric-extensions-of-pseudometric-spaces.lagda.md
@@ -0,0 +1,255 @@
+# 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-space-Metric-Extension :
+    isometry-Pseudometric-Space P pseudometric-space-Metric-Extension
+  isometry-metric-space-Metric-Extension = pr2 M
+
+  map-isometry-metric-space-Metric-Extension :
+    type-Pseudometric-Space P → type-metric-space-Metric-Extension
+  map-isometry-metric-space-Metric-Extension =
+    map-isometry-Pseudometric-Space
+      ( P)
+      ( pseudometric-space-Metric-Extension)
+      ( isometry-metric-space-Metric-Extension)
+```
+
+## Properties
+
+### The forgetful metric extension of a metric space into itself
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+  forgetful-Metric-Extension :
+    Metric-Extension l1 l2 (pseudometric-Metric-Space M)
+  forgetful-Metric-Extension = (M , id-isometry-Metric-Space M)
+```
+
+### 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-cauchy-pseudocompletion-Metric-Extension :
+    isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-pseudocompletion-Metric-Space
+        ( metric-space-Metric-Extension P M))
+  isometry-cauchy-pseudocompletion-Metric-Extension =
+    isometry-map-cauchy-approximation-isometry-Pseudometric-Space
+      ( P)
+      ( pseudometric-space-Metric-Extension P M)
+      ( isometry-metric-space-Metric-Extension P M)
+
+  map-cauchy-pseudocompletion-Metric-Extension :
+    cauchy-approximation-Pseudometric-Space P →
+    cauchy-approximation-Metric-Space
+      ( metric-space-Metric-Extension P M)
+  map-cauchy-pseudocompletion-Metric-Extension =
+    map-isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-pseudocompletion-Metric-Space
+        ( metric-space-Metric-Extension P M))
+      ( isometry-cauchy-pseudocompletion-Metric-Extension)
+
+  is-isometry-map-cauchy-pseudocompletion-Metric-Extension :
+    is-isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-pseudocompletion-Metric-Space
+        ( metric-space-Metric-Extension P M))
+      ( map-cauchy-pseudocompletion-Metric-Extension)
+  is-isometry-map-cauchy-pseudocompletion-Metric-Extension =
+    is-isometry-map-isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( cauchy-pseudocompletion-Metric-Space
+        ( metric-space-Metric-Extension P M))
+      ( isometry-cauchy-pseudocompletion-Metric-Extension)
+```
+
+### Limit points in 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-cauchy-pseudocompletion-prop-Metric-Extension : Prop l4
+  is-limit-map-cauchy-pseudocompletion-prop-Metric-Extension =
+    is-limit-cauchy-approximation-prop-Metric-Space
+      ( metric-space-Metric-Extension P M)
+      ( map-cauchy-pseudocompletion-Metric-Extension P M u)
+      ( y)
+
+  is-limit-map-cauchy-pseudocompletion-Metric-Extension : UU l4
+  is-limit-map-cauchy-pseudocompletion-Metric-Extension =
+    type-Prop
+      is-limit-map-cauchy-pseudocompletion-prop-Metric-Extension
+
+  is-prop-is-limit-map-cauchy-pseudocompletion-Metric-Extension :
+    is-prop is-limit-map-cauchy-pseudocompletion-Metric-Extension
+  is-prop-is-limit-map-cauchy-pseudocompletion-Metric-Extension =
+    is-prop-type-Prop
+      is-limit-map-cauchy-pseudocompletion-prop-Metric-Extension
+```
+
+### Similarity in the Cauchy pseudocompletion of a pseudometric space preserves and reflects limits in a metric extension
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Pseudometric-Space l1 l2)
+  (M : Metric-Extension l3 l4 P)
+  (u v : cauchy-approximation-Pseudometric-Space P)
+  (y : type-metric-space-Metric-Extension P M)
+  where
+
+  sim-has-same-limit-map-cauchy-pseudocompletion-Metric-Extension :
+    is-limit-map-cauchy-pseudocompletion-Metric-Extension P M u y →
+    is-limit-map-cauchy-pseudocompletion-Metric-Extension P M v y →
+    sim-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( u)
+      ( v)
+  sim-has-same-limit-map-cauchy-pseudocompletion-Metric-Extension 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-cauchy-pseudocompletion-Metric-Extension P M)
+      ( u)
+      ( v)
+      ( sim-has-same-limit-cauchy-approximation-Pseudometric-Space
+        ( pseudometric-space-Metric-Extension P M)
+        ( map-cauchy-pseudocompletion-Metric-Extension P M u)
+        ( map-cauchy-pseudocompletion-Metric-Extension P M v)
+        ( y)
+        ( lim-u)
+        ( lim-v))
+
+  has-same-limit-map-cauchy-sim-pseudocompletion-Metric-Extension :
+    sim-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space P)
+      ( u)
+      ( v) →
+    is-limit-map-cauchy-pseudocompletion-Metric-Extension P M u y →
+    is-limit-map-cauchy-pseudocompletion-Metric-Extension P M v y
+  has-same-limit-map-cauchy-sim-pseudocompletion-Metric-Extension u~v =
+    has-same-limit-sim-cauchy-approximation-Pseudometric-Space
+      ( pseudometric-space-Metric-Extension P M)
+      ( map-cauchy-pseudocompletion-Metric-Extension P M u)
+      ( map-cauchy-pseudocompletion-Metric-Extension P M v)
+      ( y)
+      ( preserves-sim-map-isometry-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space P)
+        ( cauchy-pseudocompletion-Metric-Space
+          ( metric-space-Metric-Extension P M))
+        ( isometry-cauchy-pseudocompletion-Metric-Extension P M)
+        ( u)
+        ( v)
+        ( u~v))
+```
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 ffecd0aafca..d4228503f38 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,17 @@ 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
@@ -397,7 +408,7 @@ module _
   where
 
   abstract
-    preserves-neighborhood-map-metric-quotient-Pseudometric-Space :
+    preserves-neighborhoods-map-metric-quotient-Pseudometric-Space :
       (d : ℚ⁺) (x y : type-Pseudometric-Space M) →
       neighborhood-Pseudometric-Space M d x y →
       neighborhood-metric-quotient-Pseudometric-Space
@@ -405,7 +416,7 @@ module _
         ( d)
         ( map-metric-quotient-Pseudometric-Space M x)
         ( map-metric-quotient-Pseudometric-Space M y)
-    preserves-neighborhood-map-metric-quotient-Pseudometric-Space
+    preserves-neighborhoods-map-metric-quotient-Pseudometric-Space
       d x y d⟨x,y⟩ (x' , x≈x') (y' , y≈y') =
       let
         x~x' =
@@ -423,15 +434,15 @@ module _
             ( y≈y')
 
       in
-        preserves-neighborhood-right-sim-Pseudometric-Space M y~y' d x'
-          ( preserves-neighborhood-left-sim-Pseudometric-Space
+        preserves-neighborhoods-right-sim-Pseudometric-Space M y~y' d x'
+          ( preserves-neighborhoods-left-sim-Pseudometric-Space
             ( M)
             ( x~x')
             ( d)
             ( y)
             ( d⟨x,y⟩))
 
-    reflects-neighborhood-map-metric-quotient-Pseudometric-Space :
+    reflects-neighborhoods-map-metric-quotient-Pseudometric-Space :
       (d : ℚ⁺) (x y : type-Pseudometric-Space M) →
       neighborhood-metric-quotient-Pseudometric-Space
         ( M)
@@ -439,7 +450,7 @@ module _
         ( map-metric-quotient-Pseudometric-Space M x)
         ( map-metric-quotient-Pseudometric-Space M y) →
       neighborhood-Pseudometric-Space M d x y
-    reflects-neighborhood-map-metric-quotient-Pseudometric-Space
+    reflects-neighborhoods-map-metric-quotient-Pseudometric-Space
       d x y Nxy =
         Nxy
           ( map-subtype-metric-quotient-Pseudometric-Space M x)
@@ -451,8 +462,8 @@ module _
         ( pseudometric-metric-quotient-Pseudometric-Space M)
         ( map-metric-quotient-Pseudometric-Space M)
     is-isometry-map-metric-quotient-Pseudometric-Space d x y =
-      ( preserves-neighborhood-map-metric-quotient-Pseudometric-Space d x y ,
-        reflects-neighborhood-map-metric-quotient-Pseudometric-Space d x y)
+      ( preserves-neighborhoods-map-metric-quotient-Pseudometric-Space d x y ,
+        reflects-neighborhoods-map-metric-quotient-Pseudometric-Space d x y)
 ```
 
 ### The isometry from a pseudometric space to its quotient metric space
@@ -758,7 +769,7 @@ module _
         ( f))
 
   abstract
-    preserves-neighborhood-map-isometry-metric-quotient-Pseudometric-Space :
+    preserves-neighborhoods-map-isometry-metric-quotient-Pseudometric-Space :
       (d : ℚ⁺) →
       (x y : type-metric-quotient-Pseudometric-Space A) →
       neighborhood-metric-quotient-Pseudometric-Space
@@ -771,7 +782,7 @@ module _
         ( d)
         ( map-isometry-metric-quotient-Pseudometric-Space x)
         ( map-isometry-metric-quotient-Pseudometric-Space y)
-    preserves-neighborhood-map-isometry-metric-quotient-Pseudometric-Space =
+    preserves-neighborhoods-map-isometry-metric-quotient-Pseudometric-Space =
       is-short-map-short-function-metric-quotient-Pseudometric-Space
         ( A)
         ( B)
@@ -780,7 +791,7 @@ module _
           ( pseudometric-Metric-Space B)
           ( f))
 
-    reflects-neighborhood-map-isometry-metric-quotient-Pseudometric-Space :
+    reflects-neighborhoods-map-isometry-metric-quotient-Pseudometric-Space :
       (d : ℚ⁺) →
       (x y : type-metric-quotient-Pseudometric-Space A) →
       neighborhood-Metric-Space
@@ -793,9 +804,9 @@ module _
         ( d)
         ( x)
         ( y)
-    reflects-neighborhood-map-isometry-metric-quotient-Pseudometric-Space
+    reflects-neighborhoods-map-isometry-metric-quotient-Pseudometric-Space
       d X Y N⟨fX,fY⟩ (x , x∈X) (y , y∈Y) =
-      reflects-neighborhood-map-isometry-Pseudometric-Space
+      reflects-neighborhoods-map-isometry-Pseudometric-Space
         ( A)
         ( pseudometric-Metric-Space B)
         ( f)
@@ -814,11 +825,11 @@ module _
         ( B)
         ( map-isometry-metric-quotient-Pseudometric-Space)
     is-isometry-map-isometry-metric-quotient-Pseudometric-Space d x y =
-      ( preserves-neighborhood-map-isometry-metric-quotient-Pseudometric-Space
+      ( preserves-neighborhoods-map-isometry-metric-quotient-Pseudometric-Space
         ( d)
         ( x)
         ( y) ,
-        reflects-neighborhood-map-isometry-metric-quotient-Pseudometric-Space
+        reflects-neighborhoods-map-isometry-metric-quotient-Pseudometric-Space
           ( d)
           ( x)
           ( y))
diff --git a/src/metric-spaces/precategory-of-metric-spaces-and-isometries.lagda.md b/src/metric-spaces/precategory-of-metric-spaces-and-isometries.lagda.md
index ba315c5ba83..04989c2beae 100644
--- a/src/metric-spaces/precategory-of-metric-spaces-and-isometries.lagda.md
+++ b/src/metric-spaces/precategory-of-metric-spaces-and-isometries.lagda.md
@@ -55,7 +55,7 @@ module _
       ( Metric-Space l1 l2)
       ( set-isometry-Metric-Space)
       ( λ {A B C} → comp-isometry-Metric-Space A B C)
-      ( isometry-id-Metric-Space)
+      ( id-isometry-Metric-Space)
       ( λ {A B C D} → associative-comp-isometry-Metric-Space A B C D)
       ( λ {A B} → left-unit-law-comp-isometry-Metric-Space A B)
       ( λ {A B} → right-unit-law-comp-isometry-Metric-Space A B)
diff --git a/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md b/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md
index 6d3251395db..c494f32b3d5 100644
--- a/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md
+++ b/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md
@@ -56,7 +56,7 @@ module _
       ( Metric-Space l1 l2)
       ( set-short-function-Metric-Space)
       ( λ {A B C} → comp-short-function-Metric-Space A B C)
-      ( short-id-Metric-Space)
+      ( id-short-function-Metric-Space)
       ( λ {A B C D} → associative-comp-short-function-Metric-Space A B C D)
       ( λ {A B} → left-unit-law-comp-short-function-Metric-Space A B)
       ( λ {A B} → right-unit-law-comp-short-function-Metric-Space A B)
@@ -149,7 +149,7 @@ module _
         ( B)
         ( f)
         ( short-inverse))
-      ( short-id-Metric-Space B)
+      ( id-short-function-Metric-Space B)
       ( is-section-map-inv-is-equiv E)) ,
       ( eq-htpy-map-short-function-Metric-Space
         ( A)
@@ -160,7 +160,7 @@ module _
           ( A)
           ( short-inverse)
           ( f))
-        ( short-id-Metric-Space A)
+        ( id-short-function-Metric-Space A)
         ( is-retraction-map-inv-is-equiv E)))
       where
 
diff --git a/src/metric-spaces/short-functions-metric-spaces.lagda.md b/src/metric-spaces/short-functions-metric-spaces.lagda.md
index 64e55931bc5..e0cb7d72f27 100644
--- a/src/metric-spaces/short-functions-metric-spaces.lagda.md
+++ b/src/metric-spaces/short-functions-metric-spaces.lagda.md
@@ -140,9 +140,9 @@ module _
     is-short-id-Pseudometric-Space
       ( pseudometric-Metric-Space A)
 
-  short-id-Metric-Space : short-function-Metric-Space A A
-  short-id-Metric-Space =
-    short-id-Pseudometric-Space (pseudometric-Metric-Space A)
+  id-short-function-Metric-Space : short-function-Metric-Space A A
+  id-short-function-Metric-Space =
+    id-short-function-Pseudometric-Space (pseudometric-Metric-Space A)
 ```
 
 ### Equality of short functions between metric spaces is characterized by homotopy of their carrier maps
@@ -216,7 +216,7 @@ module _
 
   left-unit-law-comp-short-function-Metric-Space :
     ( comp-short-function-Metric-Space A B B
-      ( short-id-Metric-Space B)
+      ( id-short-function-Metric-Space B)
       ( f)) ＝
     ( f)
   left-unit-law-comp-short-function-Metric-Space =
@@ -228,7 +228,7 @@ module _
   right-unit-law-comp-short-function-Metric-Space :
     ( comp-short-function-Metric-Space A A B
       ( f)
-      ( short-id-Metric-Space A)) ＝
+      ( id-short-function-Metric-Space A)) ＝
     ( f)
   right-unit-law-comp-short-function-Metric-Space =
     right-unit-law-comp-short-function-Pseudometric-Space
diff --git a/src/metric-spaces/short-functions-pseudometric-spaces.lagda.md b/src/metric-spaces/short-functions-pseudometric-spaces.lagda.md
index 2075b6e1006..c4e262d3a3d 100644
--- a/src/metric-spaces/short-functions-pseudometric-spaces.lagda.md
+++ b/src/metric-spaces/short-functions-pseudometric-spaces.lagda.md
@@ -116,9 +116,10 @@ module _
     is-short-function-Pseudometric-Space A A (id-Pseudometric-Space A)
   is-short-id-Pseudometric-Space d x y H = H
 
-  short-id-Pseudometric-Space : short-function-Pseudometric-Space A A
-  short-id-Pseudometric-Space =
-    id-Pseudometric-Space A , is-short-id-Pseudometric-Space
+  id-short-function-Pseudometric-Space :
+    short-function-Pseudometric-Space A A
+  id-short-function-Pseudometric-Space =
+    ( id-Pseudometric-Space A , is-short-id-Pseudometric-Space)
 ```
 
 ### Equality of short functions between pseudometric spaces is characterized by homotopy of their carrier maps
@@ -192,7 +193,7 @@ module _
 
   left-unit-law-comp-short-function-Pseudometric-Space :
     ( comp-short-function-Pseudometric-Space A B B
-      ( short-id-Pseudometric-Space B)
+      ( id-short-function-Pseudometric-Space B)
       ( f)) ＝
     ( f)
   left-unit-law-comp-short-function-Pseudometric-Space =
@@ -203,7 +204,7 @@ module _
         ( A)
         ( B)
         ( B)
-        ( short-id-Pseudometric-Space B)
+        ( id-short-function-Pseudometric-Space B)
         ( f))
       ( f)
       ( λ x → refl)
@@ -211,7 +212,7 @@ module _
   right-unit-law-comp-short-function-Pseudometric-Space :
     ( comp-short-function-Pseudometric-Space A A B
       ( f)
-      ( short-id-Pseudometric-Space A)) ＝
+      ( id-short-function-Pseudometric-Space A)) ＝
     ( f)
   right-unit-law-comp-short-function-Pseudometric-Space =
     eq-htpy-map-short-function-Pseudometric-Space
@@ -223,7 +224,7 @@ module _
         ( A)
         ( B)
         ( f)
-        ( short-id-Pseudometric-Space A))
+        ( id-short-function-Pseudometric-Space A))
       ( λ x → refl)
 ```
 
@@ -295,7 +296,7 @@ module _
     is-isometry-Pseudometric-Space A B f →
     is-short-function-Pseudometric-Space A B f
   is-short-is-isometry-Pseudometric-Space I =
-    preserves-neighborhood-map-isometry-Pseudometric-Space A B (f , I)
+    preserves-neighborhoods-map-isometry-Pseudometric-Space A B (f , I)
 ```
 
 ### The embedding of isometries of pseudometric spaces into short maps
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 f9caa041d21..6a249158e43 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
@@ -172,13 +173,13 @@ module _
   where
 
   abstract
-    preserves-neighborhood-left-sim-Pseudometric-Space :
+    preserves-neighborhoods-left-sim-Pseudometric-Space :
       { x y : type-Pseudometric-Space A} →
       ( sim-Pseudometric-Space A x y) →
       ( d : ℚ⁺) (z : type-Pseudometric-Space A) →
       neighborhood-Pseudometric-Space A d x z →
       neighborhood-Pseudometric-Space A d y z
-    preserves-neighborhood-left-sim-Pseudometric-Space {x} {y} x≍y d z Nxz =
+    preserves-neighborhoods-left-sim-Pseudometric-Space {x} {y} x≍y d z Nxz =
       saturated-neighborhood-Pseudometric-Space
         ( A)
         ( d)
@@ -203,46 +204,46 @@ module _
                 ( y)
                 ( x≍y δ))))
 
-    preserves-neighborhood-right-sim-Pseudometric-Space :
+    preserves-neighborhoods-right-sim-Pseudometric-Space :
       { x y : type-Pseudometric-Space A} →
       ( sim-Pseudometric-Space A x y) →
       ( d : ℚ⁺) (z : type-Pseudometric-Space A) →
       neighborhood-Pseudometric-Space A d z x →
       neighborhood-Pseudometric-Space A d z y
-    preserves-neighborhood-right-sim-Pseudometric-Space {x} {y} x≍y d z Nzx =
+    preserves-neighborhoods-right-sim-Pseudometric-Space {x} {y} x≍y d z Nzx =
       symmetric-neighborhood-Pseudometric-Space A d y z
-        ( preserves-neighborhood-left-sim-Pseudometric-Space x≍y d z
+        ( preserves-neighborhoods-left-sim-Pseudometric-Space x≍y d z
           ( symmetric-neighborhood-Pseudometric-Space A d z x Nzx))
 
-    preserves-neighborhood-sim-Pseudometric-Space :
+    preserves-neighborhoods-sim-Pseudometric-Space :
       {x x' y y' : type-Pseudometric-Space A} →
       sim-Pseudometric-Space A x x' →
       sim-Pseudometric-Space A y y' →
       (d : ℚ⁺) →
       neighborhood-Pseudometric-Space A d x y →
       neighborhood-Pseudometric-Space A d x' y'
-    preserves-neighborhood-sim-Pseudometric-Space
+    preserves-neighborhoods-sim-Pseudometric-Space
       {x} {x'} {y} {y'} x~x' y~y' d Nxy =
-      preserves-neighborhood-left-sim-Pseudometric-Space
+      preserves-neighborhoods-left-sim-Pseudometric-Space
         ( x~x')
         ( d)
         ( y')
-        ( preserves-neighborhood-right-sim-Pseudometric-Space
+        ( preserves-neighborhoods-right-sim-Pseudometric-Space
           ( y~y')
           ( d)
           ( x)
           ( Nxy))
 
-    reflects-neighborhood-sim-Pseudometric-Space :
+    reflects-neighborhoods-sim-Pseudometric-Space :
       {x x' y y' : type-Pseudometric-Space A} →
       sim-Pseudometric-Space A x x' →
       sim-Pseudometric-Space A y y' →
       (d : ℚ⁺) →
       neighborhood-Pseudometric-Space A d x' y' →
       neighborhood-Pseudometric-Space A d x y
-    reflects-neighborhood-sim-Pseudometric-Space
+    reflects-neighborhoods-sim-Pseudometric-Space
       {x} {x'} {y} {y'} x~x' y~y' =
-      preserves-neighborhood-sim-Pseudometric-Space
+      preserves-neighborhoods-sim-Pseudometric-Space
         ( inv-sim-Pseudometric-Space A x~x')
         ( inv-sim-Pseudometric-Space A y~y')
 
@@ -254,8 +255,8 @@ module _
         neighborhood-Pseudometric-Space A d y z)
     same-neighbors-iff-sim-Pseudometric-Space =
       ( λ x≍y d z →
-        ( preserves-neighborhood-left-sim-Pseudometric-Space x≍y d z) ,
-        ( preserves-neighborhood-left-sim-Pseudometric-Space
+        ( preserves-neighborhoods-left-sim-Pseudometric-Space x≍y d z) ,
+        ( preserves-neighborhoods-left-sim-Pseudometric-Space
           ( inv-sim-Pseudometric-Space A x≍y)
           ( d)
           ( z))) ,
@@ -314,15 +315,46 @@ 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 preserve and 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
+
+  preserves-sim-map-isometry-Pseudometric-Space :
+    ( x y : type-Pseudometric-Space A) →
+    ( sim-Pseudometric-Space A x y) →
+    ( sim-Pseudometric-Space B
+      ( map-isometry-Pseudometric-Space A B f x)
+      ( map-isometry-Pseudometric-Space A B f y))
+  preserves-sim-map-isometry-Pseudometric-Space =
+    preserves-sim-map-short-function-Pseudometric-Space
+      ( A)
+      ( B)
+      ( short-isometry-Pseudometric-Space A B f)
+
+  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-neighborhoods-map-isometry-Pseudometric-Space A B f d x y (fx~fy d)
 ```