diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md
index bc48c2ee7e..6c3a41a83c 100644
--- a/src/metric-spaces.lagda.md
+++ b/src/metric-spaces.lagda.md
@@ -57,6 +57,9 @@ metric space, `N d₂ x y` [or](foundation.disjunction.md)
 module metric-spaces where
 
 open import metric-spaces.accumulation-points-subsets-located-metric-spaces public
+open import metric-spaces.action-on-cauchy-approximations-isometries-pseudometric-spaces public
+open import metric-spaces.action-on-cauchy-approximations-short-maps-metric-spaces public
+open import metric-spaces.action-on-cauchy-approximations-short-maps-pseudometric-spaces public
 open import metric-spaces.apartness-located-metric-spaces public
 open import metric-spaces.approximations-located-metric-spaces public
 open import metric-spaces.approximations-metric-spaces public
@@ -64,6 +67,7 @@ open import metric-spaces.bounded-distance-decompositions-of-metric-spaces publi
 open import metric-spaces.cartesian-products-metric-spaces public
 open import metric-spaces.category-of-metric-spaces-and-isometries public
 open import metric-spaces.category-of-metric-spaces-and-short-functions public
+open import metric-spaces.cauchy-approximations-in-cauchy-pseudocompletions-of-pseudometric-spaces 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
@@ -86,6 +90,8 @@ open import metric-spaces.elements-at-bounded-distance-metric-spaces public
 open import metric-spaces.equality-of-metric-spaces public
 open import metric-spaces.equality-of-pseudometric-spaces public
 open import metric-spaces.extensionality-pseudometric-spaces public
+open import metric-spaces.extensions-metric-spaces public
+open import metric-spaces.extensions-pseudometric-spaces public
 open import metric-spaces.functions-metric-spaces public
 open import metric-spaces.functions-pseudometric-spaces public
 open import metric-spaces.functor-category-set-functions-isometry-metric-spaces public
@@ -106,6 +112,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-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/accumulation-points-subsets-located-metric-spaces.lagda.md b/src/metric-spaces/accumulation-points-subsets-located-metric-spaces.lagda.md
index 8f84ddb509..4eb9cb1637 100644
--- a/src/metric-spaces/accumulation-points-subsets-located-metric-spaces.lagda.md
+++ b/src/metric-spaces/accumulation-points-subsets-located-metric-spaces.lagda.md
@@ -28,6 +28,7 @@ open import lists.sequences
 
 open import logic.functoriality-existential-quantification
 
+open import metric-spaces.action-on-cauchy-approximations-short-maps-metric-spaces
 open import metric-spaces.apartness-located-metric-spaces
 open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.cauchy-sequences-metric-spaces
diff --git a/src/metric-spaces/action-on-cauchy-approximations-isometries-pseudometric-spaces.lagda.md b/src/metric-spaces/action-on-cauchy-approximations-isometries-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..5a517b342c
--- /dev/null
+++ b/src/metric-spaces/action-on-cauchy-approximations-isometries-pseudometric-spaces.lagda.md
@@ -0,0 +1,137 @@
+# The action on Cauchy approximations of isometries between pseudometric spaces
+
+```agda
+module metric-spaces.action-on-cauchy-approximations-isometries-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import metric-spaces.action-on-cauchy-approximations-short-maps-pseudometric-spaces
+open import metric-spaces.cauchy-approximations-pseudometric-spaces
+open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces
+open import metric-spaces.isometries-pseudometric-spaces
+open import metric-spaces.pseudometric-spaces
+open import metric-spaces.short-functions-pseudometric-spaces
+```
+
+</details>
+
+## Idea
+
+[Isometries](metric-spaces.isometries-pseudometric-spaces.md) between
+[pseudometric spaces](metric-spaces.pseudometric-spaces.md) act on
+[Cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md)
+and induce an isometry between the
+[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces.md).
+
+## Definitions
+
+### 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)
+```
+
+## Properties
+
+### 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 =
+    preserves-neighborhoods-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)
+```
diff --git a/src/metric-spaces/action-on-cauchy-approximations-short-maps-metric-spaces.lagda.md b/src/metric-spaces/action-on-cauchy-approximations-short-maps-metric-spaces.lagda.md
new file mode 100644
index 0000000000..140b8de55b
--- /dev/null
+++ b/src/metric-spaces/action-on-cauchy-approximations-short-maps-metric-spaces.lagda.md
@@ -0,0 +1,83 @@
+# The action on Cauchy approximations of short maps between metric spaces
+
+```agda
+module metric-spaces.action-on-cauchy-approximations-short-maps-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import metric-spaces.action-on-cauchy-approximations-short-maps-pseudometric-spaces
+open import metric-spaces.cauchy-approximations-metric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.short-functions-metric-spaces
+```
+
+</details>
+
+## Idea
+
+[metric spaces](metric-spaces.metric-spaces.md) act on
+[cauchy approximations](metric-spaces.cauchy-approximations-metric-spaces.md)
+and induce a short map between the
+[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-metric-spaces.md).
+
+## Definitions
+
+### The action of short maps on Cauchy approximations
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space l1 l2) (B : Metric-Space l1' l2')
+  (f : short-function-Metric-Space A B)
+  where
+
+  map-short-function-cauchy-approximation-Metric-Space :
+    cauchy-approximation-Metric-Space A →
+    cauchy-approximation-Metric-Space B
+  map-short-function-cauchy-approximation-Metric-Space =
+    map-cauchy-approximation-short-function-Pseudometric-Space
+      ( pseudometric-Metric-Space A)
+      ( pseudometric-Metric-Space B)
+      ( f)
+```
+
+## Properties
+
+### Functoriality of the action of short maps
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A : Metric-Space l1 l2)
+  where
+
+  htpy-id-map-short-function-cauchy-approximation-Metric-Space :
+    map-short-function-cauchy-approximation-Metric-Space
+      ( A)
+      ( A)
+      ( id-short-function-Metric-Space A) ＝
+    id
+  htpy-id-map-short-function-cauchy-approximation-Metric-Space = refl
+
+module _
+  {l1a l2a l1b l2b l1c l2c : Level}
+  (A : Metric-Space l1a l2a)
+  (B : Metric-Space l1b l2b)
+  (C : Metric-Space l1c l2c)
+  (g : short-function-Metric-Space B C)
+  (f : short-function-Metric-Space A B)
+  where
+
+  htpy-comp-map-short-function-cauchy-approximation-Metric-Space :
+    ( map-short-function-cauchy-approximation-Metric-Space B C g ∘
+      map-short-function-cauchy-approximation-Metric-Space A B f) ＝
+    ( map-short-function-cauchy-approximation-Metric-Space A C
+      ( comp-short-function-Metric-Space A B C g f))
+  htpy-comp-map-short-function-cauchy-approximation-Metric-Space = refl
+```
diff --git a/src/metric-spaces/action-on-cauchy-approximations-short-maps-pseudometric-spaces.lagda.md b/src/metric-spaces/action-on-cauchy-approximations-short-maps-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..d4b18f1955
--- /dev/null
+++ b/src/metric-spaces/action-on-cauchy-approximations-short-maps-pseudometric-spaces.lagda.md
@@ -0,0 +1,90 @@
+# The action on Cauchy approximations of short maps between pseudometric spaces
+
+```agda
+module metric-spaces.action-on-cauchy-approximations-short-maps-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.universe-levels
+
+open import metric-spaces.cauchy-approximations-pseudometric-spaces
+open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces
+open import metric-spaces.pseudometric-spaces
+open import metric-spaces.short-functions-pseudometric-spaces
+```
+
+</details>
+
+## Idea
+
+[Short maps](metric-spaces.short-functions-pseudometric-spaces.md) between
+[pseudometric spaces](metric-spaces.pseudometric-spaces.md) act on
+[cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md)
+and induce a short map between the
+[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces.md).
+
+## Definitions
+
+### The action of short maps on Cauchy approximations
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
+  (f : short-function-Pseudometric-Space A B)
+  where
+
+  map-cauchy-approximation-short-function-Pseudometric-Space :
+    cauchy-approximation-Pseudometric-Space A →
+    cauchy-approximation-Pseudometric-Space B
+  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
+          ( A)
+          ( B)
+          ( f)
+          ( ε +ℚ⁺ δ)
+          ( u ε)
+          ( u δ)
+          ( H ε δ))
+```
+
+## Properties
+
+### The action of short maps on Cauchy approximations is short
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
+  (f : short-function-Pseudometric-Space A B)
+  where
+
+  preserves-neighborhoods-map-cauchy-approximation-short-function-Pseudometric-Space :
+    is-short-function-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space A)
+      ( cauchy-pseudocompletion-Pseudometric-Space B)
+      ( map-cauchy-approximation-short-function-Pseudometric-Space A B f)
+  preserves-neighborhoods-map-cauchy-approximation-short-function-Pseudometric-Space
+    d x y Nxy α β =
+    is-short-map-short-function-Pseudometric-Space A B f
+      ( α +ℚ⁺ β +ℚ⁺ d)
+      ( map-cauchy-approximation-Pseudometric-Space A x α)
+      ( map-cauchy-approximation-Pseudometric-Space A y β)
+      ( Nxy α β)
+
+  short-map-cauchy-approximation-short-function-Pseudometric-Space :
+    short-function-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space A)
+      ( cauchy-pseudocompletion-Pseudometric-Space B)
+  short-map-cauchy-approximation-short-function-Pseudometric-Space =
+    ( map-cauchy-approximation-short-function-Pseudometric-Space A B f ,
+      preserves-neighborhoods-map-cauchy-approximation-short-function-Pseudometric-Space)
+```
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 ea2bf3aa07..035604397f 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
@@ -33,6 +33,7 @@ open import foundation.subtypes
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
+open import metric-spaces.action-on-cauchy-approximations-short-maps-metric-spaces
 open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.elements-at-bounded-distance-metric-spaces
 open import metric-spaces.equality-of-metric-spaces
@@ -213,7 +214,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 +225,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 +238,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 +249,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 +281,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-in-cauchy-pseudocompletions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-in-cauchy-pseudocompletions-of-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..d147667cda
--- /dev/null
+++ b/src/metric-spaces/cauchy-approximations-in-cauchy-pseudocompletions-of-pseudometric-spaces.lagda.md
@@ -0,0 +1,469 @@
+# Cauchy approximations in the Cauchy pseudocompletion of a pseudometric space
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module
+  metric-spaces.cauchy-approximations-in-cauchy-pseudocompletions-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.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import metric-spaces.action-on-cauchy-approximations-isometries-pseudometric-spaces
+open import metric-spaces.action-on-cauchy-approximations-short-maps-pseudometric-spaces
+open import metric-spaces.cauchy-approximations-pseudometric-spaces
+open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces
+open import metric-spaces.isometries-pseudometric-spaces
+open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces
+open import metric-spaces.pseudometric-spaces
+open import metric-spaces.rational-neighborhood-relations
+open import metric-spaces.short-functions-pseudometric-spaces
+open import metric-spaces.similarity-of-elements-pseudometric-spaces
+```
+
+</details>
+
+## Idea
+
+[Cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md)
+in the
+[Cauchy pseudocompletion](metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces.md)
+of a [pseudometric space](metric-spaces.pseudometric-spaces.md) have a
+[limit](metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces.md).
+
+## Properties
+
+### Any Cauchy approximation in the Cauchy pseudocompletion of a pseudometric space has a limit
+
+```agda
+module _
+  { l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  ( U :
+    cauchy-approximation-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space M))
+  where
+
+  map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+    ℚ⁺ → ℚ⁺ → type-Pseudometric-Space M
+  map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ε =
+    map-cauchy-approximation-Pseudometric-Space M
+      ( map-cauchy-approximation-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( U)
+        ( ε))
+
+  is-cauchy-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+    (δ ε d₁ d₂ : ℚ⁺) →
+    neighborhood-Pseudometric-Space
+      ( M)
+      ( d₁ +ℚ⁺ d₂ +ℚ⁺ (δ +ℚ⁺ ε))
+      ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+        ( δ)
+        ( d₁))
+      ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+        ( ε)
+        ( d₂))
+  is-cauchy-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+    =
+    is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space M)
+      ( U)
+
+  map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+    ℚ⁺ → type-Pseudometric-Space M
+  map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space d =
+    let
+      (d₁ , d₂ , _) = split-ℚ⁺ d
+    in
+      map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space d₂ d₁
+
+  abstract
+    is-cauchy-map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+      is-cauchy-approximation-Pseudometric-Space
+        ( M)
+        ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space)
+    is-cauchy-map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+      δ ε =
+      let
+        (δ₁ , δ₂ , δ₁+δ₂=δ) = split-ℚ⁺ δ
+        (ε₁ , ε₂ , ε₁+ε₂=ε) = split-ℚ⁺ ε
+
+        lemma-δ+ε :
+          ((δ₁ +ℚ⁺ ε₁) +ℚ⁺ (δ₂ +ℚ⁺ ε₂)) ＝ δ +ℚ⁺ ε
+        lemma-δ+ε =
+          ( interchange-law-add-add-ℚ⁺ δ₁ ε₁ δ₂ ε₂) ∙
+          ( ap-binary add-ℚ⁺ δ₁+δ₂=δ ε₁+ε₂=ε)
+      in
+        tr
+          ( is-upper-bound-dist-Pseudometric-Space
+            ( M)
+            ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              ( δ))
+            ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              ( ε)))
+          ( lemma-δ+ε)
+          ( is-cauchy-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+            _ _ _ _)
+
+  lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+    cauchy-approximation-Pseudometric-Space M
+  lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space =
+    ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ,
+      is-cauchy-map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space)
+
+  abstract
+    is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+      is-limit-cauchy-approximation-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( U)
+        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space)
+    is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+      δ ε η θ =
+      let
+        (θ₁ , θ₂ , θ₁+θ₂=θ) = split-ℚ⁺ θ
+
+        lemma-η+θ+δ :
+          ((η +ℚ⁺ θ₁) +ℚ⁺ (δ +ℚ⁺ θ₂)) ＝ η +ℚ⁺ θ +ℚ⁺ δ
+        lemma-η+θ+δ =
+          ( interchange-law-add-add-ℚ⁺ η θ₁ δ θ₂) ∙
+          ( ap
+            ( add-ℚ⁺ (η +ℚ⁺ δ))
+            ( θ₁+θ₂=θ)) ∙
+          ( associative-add-ℚ⁺ η δ θ) ∙
+          ( ap
+            ( add-ℚ⁺ η)
+            ( commutative-add-ℚ⁺ δ θ)) ∙
+          ( inv (associative-add-ℚ⁺ η θ δ))
+
+        lemma-lim :
+          neighborhood-Pseudometric-Space M
+            ( η +ℚ⁺ θ +ℚ⁺ δ)
+            ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              ( δ)
+              ( η))
+            ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              ( θ₂)
+              ( θ₁))
+        lemma-lim =
+          tr
+            ( is-upper-bound-dist-Pseudometric-Space M
+              ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+                ( δ)
+                ( η))
+              ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+                ( θ)))
+            ( lemma-η+θ+δ)
+            ( is-cauchy-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              _ _ _ _)
+      in
+        tr
+          ( is-upper-bound-dist-Pseudometric-Space M
+            ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              ( δ)
+              ( η))
+            ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              ( θ)))
+          ( associative-add-ℚ⁺
+            ( η +ℚ⁺ θ)
+            ( δ)
+            ( ε))
+          ( monotonic-neighborhood-Pseudometric-Space M
+            ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              ( δ)
+              ( η))
+            ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+              ( θ))
+            ( η +ℚ⁺ θ +ℚ⁺ δ)
+            ( η +ℚ⁺ θ +ℚ⁺ δ +ℚ⁺ ε)
+            ( le-left-add-ℚ⁺ ( η +ℚ⁺ θ +ℚ⁺ δ) ε)
+            ( lemma-lim))
+
+  has-limit-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+    Σ ( cauchy-approximation-Pseudometric-Space M)
+      ( is-limit-cauchy-approximation-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( U))
+  has-limit-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space =
+    ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ,
+      is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space)
+```
+
+### Any Cauchy approximation in the pseudometric completion is similar to the constant Cauchy approximation of its limit
+
+```agda
+module _
+  { l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  ( u :
+    cauchy-approximation-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space M))
+  where
+
+  sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+    sim-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space M))
+      ( u)
+      ( const-cauchy-approximation-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+          ( M)
+          ( u)))
+  sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+    =
+    sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space M)
+      ( u)
+      ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M u)
+      ( is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+        ( M)
+        ( u))
+```
+
+### The map from a Cauchy approximation in the pseudometric completion to its limit is short
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    is-short-function-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+      is-short-function-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M))
+        ( cauchy-pseudocompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M))
+        ( ( const-cauchy-approximation-Pseudometric-Space
+            ( cauchy-pseudocompletion-Pseudometric-Space M)) ∘
+          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+            ( M)))
+    is-short-function-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+      d u v =
+      preserves-neighborhoods-sim-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M))
+        { u}
+        { const-cauchy-approximation-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M)
+          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+            ( M)
+            ( u))}
+        { v}
+        { const-cauchy-approximation-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M)
+          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+            ( M)
+            ( v))}
+        ( sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+          ( M)
+          ( u))
+        ( sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+          ( M)
+          ( v))
+        ( d)
+
+    is-short-function-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space :
+      is-short-function-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M))
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M)
+    is-short-function-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space
+      d u v Nuv =
+      reflects-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( d)
+        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+          ( M)
+          ( u))
+        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+          ( M)
+          ( v))
+        ( is-short-function-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+          ( d)
+          ( u)
+          ( v)
+          ( Nuv))
+
+  short-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space :
+    short-function-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space M))
+      ( cauchy-pseudocompletion-Pseudometric-Space M)
+  short-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space =
+    ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M ,
+      is-short-function-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space)
+```
+
+### The map from a Cauchy approximation in the pseudometric completion to its limit is an isometry
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    reflects-neighborhoods-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+      ( d : ℚ⁺) →
+      ( u v :
+        cauchy-approximation-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M)) →
+      neighborhood-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( d)
+        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+          ( M)
+          ( u))
+        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+          ( M)
+          ( v)) →
+      neighborhood-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M))
+        ( d)
+        ( u)
+        ( v)
+    reflects-neighborhoods-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+      d u v N-lim =
+      reflects-neighborhoods-sim-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M))
+        { u}
+        { const-cauchy-approximation-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M)
+          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+            ( M)
+            ( u))}
+        { v}
+        { const-cauchy-approximation-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M)
+          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+            ( M)
+            ( v))}
+        ( sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+          ( M)
+          ( u))
+        ( sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+          ( M)
+          ( v))
+        ( d)
+        ( preserves-neighborhoods-map-cauchy-pseudocompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M)
+          ( d)
+          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+            ( M)
+            ( u))
+          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+            ( M)
+            ( v))
+          ( N-lim))
+
+    is-isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+      is-isometry-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M))
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M)
+    is-isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+      d x y =
+      ( ( is-short-function-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space
+          ( M)
+          ( d)
+          ( x)
+          ( y)) ,
+        ( reflects-neighborhoods-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
+          ( d)
+          ( x)
+          ( y)))
+
+  isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space M))
+      ( cauchy-pseudocompletion-Pseudometric-Space M)
+  isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space =
+    ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M ,
+      is-isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space)
+```
+
+### The image of a Cauchy approximation in the Cauchy pseudocompletion is convergent
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  (u : cauchy-approximation-Pseudometric-Space M)
+  where
+
+  is-limit-map-cauchy-approximation-cauchy-pseudocompletion-Ppseudometric-Space :
+    is-limit-cauchy-approximation-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space M)
+      ( map-cauchy-approximation-short-function-Pseudometric-Space
+        ( M)
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( short-map-cauchy-pseudocompletion-Pseudometric-Space M)
+        ( u))
+      ( u)
+  is-limit-map-cauchy-approximation-cauchy-pseudocompletion-Ppseudometric-Space
+    ε δ α β =
+    symmetric-neighborhood-Pseudometric-Space M
+      ( (α +ℚ⁺ β) +ℚ⁺ (ε +ℚ⁺ δ))
+      ( map-cauchy-approximation-Pseudometric-Space M u β)
+      ( map-cauchy-approximation-Pseudometric-Space M u ε)
+      ( monotonic-neighborhood-Pseudometric-Space M
+        ( map-cauchy-approximation-Pseudometric-Space M u β)
+        ( map-cauchy-approximation-Pseudometric-Space M u ε)
+        ( β +ℚ⁺ ε)
+        ( (α +ℚ⁺ β) +ℚ⁺ (ε +ℚ⁺ δ))
+        ( preserves-le-add-ℚ
+          { rational-ℚ⁺ β}
+          { rational-ℚ⁺ (α +ℚ⁺ β)}
+          { rational-ℚ⁺ ε}
+          { rational-ℚ⁺ (ε +ℚ⁺ δ)}
+          ( le-right-add-ℚ⁺ α β)
+          ( le-left-add-ℚ⁺ ε δ))
+        ( is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space
+          ( M)
+          ( u)
+          ( β)
+          ( ε)))
+
+  sim-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+    sim-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space M))
+      ( map-cauchy-approximation-short-function-Pseudometric-Space
+        ( M)
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( short-map-cauchy-pseudocompletion-Pseudometric-Space M)
+        ( u))
+      ( map-cauchy-pseudocompletion-Pseudometric-Space
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( u))
+  sim-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space =
+    sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space M)
+      ( map-cauchy-approximation-short-function-Pseudometric-Space
+        ( M)
+        ( cauchy-pseudocompletion-Pseudometric-Space M)
+        ( short-map-cauchy-pseudocompletion-Pseudometric-Space M)
+        ( u))
+      ( u)
+      ( is-limit-map-cauchy-approximation-cauchy-pseudocompletion-Ppseudometric-Space)
+```
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..5945ef2dc0 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
@@ -42,6 +42,7 @@ open import foundation.universe-levels
 
 open import logic.functoriality-existential-quantification
 
+open import metric-spaces.action-on-cauchy-approximations-short-maps-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
@@ -101,40 +102,40 @@ module _
   {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
   where
 
-  short-map-metric-quotient-cauchy-apprtoximation-Pseudometric-Space :
+  short-map-cauchy-approximation-metric-quotient-Pseudometric-Space :
     short-function-Pseudometric-Space
       ( cauchy-pseudocompletion-Pseudometric-Space M)
       ( 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-metric-quotient-Pseudometric-Space =
+    short-map-cauchy-approximation-short-function-Pseudometric-Space
       ( M)
       ( pseudometric-metric-quotient-Pseudometric-Space M)
       ( short-map-metric-quotient-Pseudometric-Space M)
 
-  map-metric-quotient-cauchy-approximation-Pseudometric-Space :
+  map-cauchy-approximation-metric-quotient-Pseudometric-Space :
     cauchy-approximation-Pseudometric-Space M →
     cauchy-approximation-Metric-Space
       ( metric-quotient-Pseudometric-Space M)
-  map-metric-quotient-cauchy-approximation-Pseudometric-Space =
+  map-cauchy-approximation-metric-quotient-Pseudometric-Space =
     map-short-function-Pseudometric-Space
       ( cauchy-pseudocompletion-Pseudometric-Space M)
       ( cauchy-pseudocompletion-Metric-Space
         ( metric-quotient-Pseudometric-Space M))
-      ( short-map-metric-quotient-cauchy-apprtoximation-Pseudometric-Space)
+      ( short-map-cauchy-approximation-metric-quotient-Pseudometric-Space)
 
-  is-short-map-metric-quotient-cauchy-approximation-Pseudometric-Space :
+  is-short-map-cauchy-approximation-metric-quotient-Pseudometric-Space :
     is-short-function-Pseudometric-Space
       ( cauchy-pseudocompletion-Pseudometric-Space M)
       ( cauchy-pseudocompletion-Metric-Space
         ( metric-quotient-Pseudometric-Space M))
-      ( map-metric-quotient-cauchy-approximation-Pseudometric-Space)
-  is-short-map-metric-quotient-cauchy-approximation-Pseudometric-Space =
+      ( map-cauchy-approximation-metric-quotient-Pseudometric-Space)
+  is-short-map-cauchy-approximation-metric-quotient-Pseudometric-Space =
     is-short-map-short-function-Pseudometric-Space
       ( cauchy-pseudocompletion-Pseudometric-Space M)
       ( cauchy-pseudocompletion-Metric-Space
         ( metric-quotient-Pseudometric-Space M))
-      ( short-map-metric-quotient-cauchy-apprtoximation-Pseudometric-Space)
+      ( short-map-cauchy-approximation-metric-quotient-Pseudometric-Space)
 ```
 
 ### Lifts of Cauchy approximations in the quotient metric space up to similarity
@@ -155,7 +156,7 @@ module _
       ( cauchy-pseudocompletion-Pseudometric-Space
         ( pseudometric-metric-quotient-Pseudometric-Space A))
       ( u)
-      ( map-metric-quotient-cauchy-approximation-Pseudometric-Space A v)
+      ( map-cauchy-approximation-metric-quotient-Pseudometric-Space A v)
 
   is-lift-quotient-cauchy-approximation-Pseudometric-Space : UU (l1 ⊔ l2)
   is-lift-quotient-cauchy-approximation-Pseudometric-Space =
@@ -206,12 +207,12 @@ module _
     is-limit-cauchy-approximation-Pseudometric-Space M u lim)
   where
 
-  preserves-limits-map-metric-quotient-cauchy-approximation-Pseudometric-Space :
+  preserves-limits-map-cauchy-approximation-metric-quotient-Pseudometric-Space :
     is-limit-cauchy-approximation-Metric-Space
       ( metric-quotient-Pseudometric-Space M)
-      ( map-metric-quotient-cauchy-approximation-Pseudometric-Space M u)
+      ( map-cauchy-approximation-metric-quotient-Pseudometric-Space M u)
       ( map-metric-quotient-Pseudometric-Space M lim)
-  preserves-limits-map-metric-quotient-cauchy-approximation-Pseudometric-Space
+  preserves-limits-map-cauchy-approximation-metric-quotient-Pseudometric-Space
     ε δ (x , x∈uε) (y , y∈lim) =
     let
       lim~y : sim-Pseudometric-Space M lim y
@@ -233,7 +234,7 @@ module _
           ( x)
           ( x∈uε)
     in
-      preserves-neighborhood-sim-Pseudometric-Space
+      preserves-neighborhoods-sim-Pseudometric-Space
         ( M)
         ( uε~x)
         ( lim~y)
@@ -252,14 +253,14 @@ module _
   has-lift-map-quotient-cauchy-approximation-metric-quotient-Pseudometric-Space :
     has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space
       ( A)
-      ( map-metric-quotient-cauchy-approximation-Pseudometric-Space A u)
+      ( map-cauchy-approximation-metric-quotient-Pseudometric-Space A u)
   has-lift-map-quotient-cauchy-approximation-metric-quotient-Pseudometric-Space =
     unit-trunc-Prop
       ( u ,
         refl-sim-Pseudometric-Space
           ( cauchy-pseudocompletion-Pseudometric-Space
             ( pseudometric-metric-quotient-Pseudometric-Space A))
-          ( map-metric-quotient-cauchy-approximation-Pseudometric-Space A u))
+          ( map-cauchy-approximation-metric-quotient-Pseudometric-Space A u))
 ```
 
 ### Convergent Cauchy approximations in the quotient metric space have a lift up to similarity
diff --git a/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md
index caf5ee3d31..b1fd39f15f 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
@@ -110,54 +106,6 @@ module _
       ( x)
 ```
 
-### The action of short maps on Cauchy approximations
-
-```agda
-module _
-  {l1 l2 l1' l2' : Level}
-  (A : Metric-Space l1 l2) (B : Metric-Space l1' l2')
-  (f : short-function-Metric-Space A B)
-  where
-
-  map-short-function-cauchy-approximation-Metric-Space :
-    cauchy-approximation-Metric-Space A →
-    cauchy-approximation-Metric-Space B
-  map-short-function-cauchy-approximation-Metric-Space =
-    map-short-function-cauchy-approximation-Pseudometric-Space
-      ( pseudometric-Metric-Space A)
-      ( pseudometric-Metric-Space B)
-      ( f)
-
-module _
-  {l1 l2 : Level}
-  (A : Metric-Space l1 l2)
-  where
-
-  eq-id-map-short-function-cauchy-approximation-Metric-Space :
-    map-short-function-cauchy-approximation-Metric-Space
-      ( A)
-      ( A)
-      ( short-id-Metric-Space A) ＝
-    id
-  eq-id-map-short-function-cauchy-approximation-Metric-Space = refl
-
-module _
-  {l1a l2a l1b l2b l1c l2c : Level}
-  (A : Metric-Space l1a l2a)
-  (B : Metric-Space l1b l2b)
-  (C : Metric-Space l1c l2c)
-  (g : short-function-Metric-Space B C)
-  (f : short-function-Metric-Space A B)
-  where
-
-  eq-comp-map-short-function-cauchy-approximation-Metric-Space :
-    ( map-short-function-cauchy-approximation-Metric-Space B C g ∘
-      map-short-function-cauchy-approximation-Metric-Space A B f) ＝
-    ( map-short-function-cauchy-approximation-Metric-Space A C
-      (comp-short-function-Metric-Space A B C g f))
-  eq-comp-map-short-function-cauchy-approximation-Metric-Space = refl
-```
-
 ### Homotopic Cauchy approximations are equal
 
 ```agda
diff --git a/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md
index 3f7b863d42..280b955661 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
 ```
@@ -103,31 +104,6 @@ module _
     refl-neighborhood-Pseudometric-Space A (ε +ℚ⁺ δ) x
 ```
 
-### The action of short maps on Cauchy approximations
-
-```agda
-module _
-  {l1 l2 l1' l2' : Level}
-  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
-  (f : short-function-Pseudometric-Space A B)
-  where
-
-  map-short-function-cauchy-approximation-Pseudometric-Space :
-    cauchy-approximation-Pseudometric-Space A →
-    cauchy-approximation-Pseudometric-Space B
-  map-short-function-cauchy-approximation-Pseudometric-Space (u , H) =
-    ( map-short-function-Pseudometric-Space A B f ∘ u ,
-      λ ε δ →
-        is-short-map-short-function-Pseudometric-Space
-          ( A)
-          ( B)
-          ( f)
-          ( ε +ℚ⁺ δ)
-          ( u ε)
-          ( u δ)
-          ( H ε δ))
-```
-
 ### 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 9dad3ad654..a45d853892 100644
--- a/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md
+++ b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md
@@ -9,25 +9,21 @@ 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
 
+open import metric-spaces.cauchy-approximations-in-cauchy-pseudocompletions-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-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 +350,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 +433,103 @@ module _
       ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u)
       ( is-limit-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u)
 ```
+
+### The isometry mapping a Cauchy approximation in 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 5bc301fcc1..044b7d09c6 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,449 +404,60 @@ module _
         ( λ d → H d α β)
 ```
 
-### Any Cauchy approximation in the Cauchy pseudocompletion of a pseudometric space has a limit
+### Similarity in the Cauchy pseudocompletion preserves and reflects limits
 
 ```agda
 module _
-  { l1 l2 : Level} (M : Pseudometric-Space l1 l2)
-  ( U :
-    cauchy-approximation-Pseudometric-Space
-      ( cauchy-pseudocompletion-Pseudometric-Space M))
-  where
-
-  map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
-    ℚ⁺ → ℚ⁺ → type-Pseudometric-Space M
-  map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ε =
-    map-cauchy-approximation-Pseudometric-Space M
-      ( map-cauchy-approximation-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space M)
-        ( U)
-        ( ε))
-
-  is-cauchy-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
-    (δ ε d₁ d₂ : ℚ⁺) →
-    neighborhood-Pseudometric-Space
-      ( M)
-      ( d₁ +ℚ⁺ d₂ +ℚ⁺ (δ +ℚ⁺ ε))
-      ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-        ( δ)
-        ( d₁))
-      ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-        ( ε)
-        ( d₂))
-  is-cauchy-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-    =
-    is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space
-      ( cauchy-pseudocompletion-Pseudometric-Space M)
-      ( U)
-
-  map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
-    ℚ⁺ → type-Pseudometric-Space M
-  map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space d =
-    let
-      (d₁ , d₂ , _) = split-ℚ⁺ d
-    in
-      map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space d₂ d₁
-
-  is-cauchy-map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
-    is-cauchy-approximation-Pseudometric-Space
-      ( M)
-      ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space)
-  is-cauchy-map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-    δ ε =
-    let
-      (δ₁ , δ₂ , δ₁+δ₂=δ) = split-ℚ⁺ δ
-      (ε₁ , ε₂ , ε₁+ε₂=ε) = split-ℚ⁺ ε
-
-      lemma-δ+ε :
-        ((δ₁ +ℚ⁺ ε₁) +ℚ⁺ (δ₂ +ℚ⁺ ε₂)) ＝ δ +ℚ⁺ ε
-      lemma-δ+ε =
-        ( interchange-law-add-add-ℚ⁺ δ₁ ε₁ δ₂ ε₂) ∙
-        ( ap-binary add-ℚ⁺ δ₁+δ₂=δ ε₁+ε₂=ε)
-    in
-      tr
-        ( is-upper-bound-dist-Pseudometric-Space
-          ( M)
-          ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( δ))
-          ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( ε)))
-        ( lemma-δ+ε)
-        ( is-cauchy-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-          _ _ _ _)
-
-  lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
-    cauchy-approximation-Pseudometric-Space M
-  lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space =
-    ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ,
-      is-cauchy-map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space)
-
-  is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
-    is-limit-cauchy-approximation-Pseudometric-Space
-      ( cauchy-pseudocompletion-Pseudometric-Space M)
-      ( U)
-      ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space)
-  is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-    δ ε η θ =
-    let
-      (θ₁ , θ₂ , θ₁+θ₂=θ) = split-ℚ⁺ θ
-
-      lemma-η+θ+δ :
-        ((η +ℚ⁺ θ₁) +ℚ⁺ (δ +ℚ⁺ θ₂)) ＝ η +ℚ⁺ θ +ℚ⁺ δ
-      lemma-η+θ+δ =
-        ( interchange-law-add-add-ℚ⁺ η θ₁ δ θ₂) ∙
-        ( ap
-          ( add-ℚ⁺ (η +ℚ⁺ δ))
-          ( θ₁+θ₂=θ)) ∙
-        ( associative-add-ℚ⁺ η δ θ) ∙
-        ( ap
-          ( add-ℚ⁺ η)
-          ( commutative-add-ℚ⁺ δ θ)) ∙
-        ( inv (associative-add-ℚ⁺ η θ δ))
-
-      lemma-lim :
-        neighborhood-Pseudometric-Space M
-          ( η +ℚ⁺ θ +ℚ⁺ δ)
-          ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( δ)
-            ( η))
-          ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( θ₂)
-            ( θ₁))
-      lemma-lim =
-        tr
-          ( is-upper-bound-dist-Pseudometric-Space M
-            ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-              ( δ)
-              ( η))
-            ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-              ( θ)))
-          ( lemma-η+θ+δ)
-          ( is-cauchy-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            _ _ _ _)
-    in
-      tr
-        ( is-upper-bound-dist-Pseudometric-Space M
-          ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( δ)
-            ( η))
-          ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( θ)))
-        ( associative-add-ℚ⁺
-          ( η +ℚ⁺ θ)
-          ( δ)
-          ( ε))
-        ( monotonic-neighborhood-Pseudometric-Space M
-          ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( δ)
-            ( η))
-          ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( θ))
-          ( η +ℚ⁺ θ +ℚ⁺ δ)
-          ( η +ℚ⁺ θ +ℚ⁺ δ +ℚ⁺ ε)
-          ( le-left-add-ℚ⁺ ( η +ℚ⁺ θ +ℚ⁺ δ) ε)
-          ( lemma-lim))
-
-  has-limit-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
-    Σ ( cauchy-approximation-Pseudometric-Space M)
-      ( is-limit-cauchy-approximation-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space M)
-        ( U))
-  has-limit-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space =
-    ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ,
-      is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space)
-```
-
-### Any Cauchy approximation in the pseudometric completion is similar to the constant Cauchy approximation of its limit
-
-```agda
-module _
-  { l1 l2 : Level} (M : Pseudometric-Space l1 l2)
-  ( u :
-    cauchy-approximation-Pseudometric-Space
-      ( cauchy-pseudocompletion-Pseudometric-Space M))
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  (u v : cauchy-approximation-Pseudometric-Space M)
+  (x : type-Pseudometric-Space M)
   where
 
-  sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
+  has-same-limit-sim-cauchy-approximation-Pseudometric-Space :
     sim-Pseudometric-Space
-      ( cauchy-pseudocompletion-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space M))
-      ( u)
-      ( const-cauchy-approximation-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space M)
-        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-          ( M)
-          ( u)))
-  sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-    =
-    sim-const-is-limit-cauchy-approximation-Pseudometric-Space
       ( cauchy-pseudocompletion-Pseudometric-Space M)
       ( u)
-      ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M u)
-      ( is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-        ( M)
-        ( u))
-```
-
-### The map from a Cauchy approximation in the pseudometric completion to its limit is short
-
-```agda
-module _
-  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
-  where
-
-  abstract
-    is-short-function-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
-      is-short-function-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space
-          ( cauchy-pseudocompletion-Pseudometric-Space M))
-        ( cauchy-pseudocompletion-Pseudometric-Space
-          ( cauchy-pseudocompletion-Pseudometric-Space M))
-        ( ( const-cauchy-approximation-Pseudometric-Space
-            ( cauchy-pseudocompletion-Pseudometric-Space M)) ∘
-          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( M)))
-    is-short-function-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-      d u v =
-      preserves-neighborhood-sim-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space
-          ( cauchy-pseudocompletion-Pseudometric-Space M))
-        { u}
-        { const-cauchy-approximation-Pseudometric-Space
-          ( cauchy-pseudocompletion-Pseudometric-Space M)
-          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( M)
-            ( u))}
-        { v}
-        { const-cauchy-approximation-Pseudometric-Space
-          ( cauchy-pseudocompletion-Pseudometric-Space M)
-          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( M)
-            ( v))}
-        ( sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-          ( M)
-          ( u))
-        ( sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-          ( M)
-          ( v))
-        ( d)
-
-    is-short-function-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space :
-      is-short-function-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space
-          ( cauchy-pseudocompletion-Pseudometric-Space M))
-        ( cauchy-pseudocompletion-Pseudometric-Space M)
-        ( 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
-        ( cauchy-pseudocompletion-Pseudometric-Space M)
-        ( d)
-        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-          ( M)
-          ( u))
-        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-          ( M)
-          ( v))
-        ( is-short-function-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-          ( d)
-          ( u)
-          ( v)
-          ( Nuv))
-
-  short-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space :
-    short-function-Pseudometric-Space
-      ( cauchy-pseudocompletion-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space M))
-      ( cauchy-pseudocompletion-Pseudometric-Space M)
-  short-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space =
-    ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M ,
-      is-short-function-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space)
-```
-
-### The map from a Cauchy approximation in the pseudometric completion to its limit is an isometry
-
-```agda
-module _
-  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
-  where
-
-  abstract
-    reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
-      ( d : ℚ⁺) →
-      ( u v :
-        cauchy-approximation-Pseudometric-Space
-          ( cauchy-pseudocompletion-Pseudometric-Space M)) →
-      neighborhood-Pseudometric-Space
+      ( 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)
-        ( d)
-        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-          ( M)
-          ( u))
-        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-          ( M)
-          ( v)) →
-      neighborhood-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space
-          ( cauchy-pseudocompletion-Pseudometric-Space M))
-        ( d)
-        ( u)
         ( v)
-    reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-      d u v N-lim =
-      reflects-neighborhood-sim-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space
-          ( cauchy-pseudocompletion-Pseudometric-Space M))
-        { u}
-        { const-cauchy-approximation-Pseudometric-Space
-          ( cauchy-pseudocompletion-Pseudometric-Space M)
-          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( M)
-            ( u))}
-        { v}
-        { const-cauchy-approximation-Pseudometric-Space
-          ( cauchy-pseudocompletion-Pseudometric-Space M)
-          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( M)
-            ( v))}
-        ( sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-          ( M)
-          ( u))
-        ( sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-          ( M)
-          ( v))
-        ( d)
-        ( preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space
-          ( cauchy-pseudocompletion-Pseudometric-Space M)
-          ( d)
-          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( M)
-            ( u))
-          ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-            ( M)
-            ( v))
-          ( N-lim))
-
-    is-isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
-      is-isometry-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space
-          ( cauchy-pseudocompletion-Pseudometric-Space M))
-        ( cauchy-pseudocompletion-Pseudometric-Space M)
-        ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M)
-    is-isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-      d x y =
-      ( ( is-short-function-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space
+        ( u)
+        ( const-cauchy-approximation-Pseudometric-Space M x)
+        ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space
           ( M)
-          ( d)
-          ( x)
-          ( y)) ,
-        ( reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space
-          ( d)
+          ( u)
           ( x)
-          ( y)))
-
-  isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
-    isometry-Pseudometric-Space
-      ( cauchy-pseudocompletion-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space M))
-      ( cauchy-pseudocompletion-Pseudometric-Space M)
-  isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space =
-    ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M ,
-      is-isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space)
-```
-
-### The action of short maps on Cauchy approximations is short
-
-```agda
-module _
-  {l1 l2 l1' l2' : Level}
-  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
-  (f : short-function-Pseudometric-Space A B)
-  where
-
-  is-short-map-short-function-cauchy-approximation-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
-    d x y Nxy α β =
-    is-short-map-short-function-Pseudometric-Space A B f
-      ( α +ℚ⁺ β +ℚ⁺ d)
-      ( map-cauchy-approximation-Pseudometric-Space A x α)
-      ( map-cauchy-approximation-Pseudometric-Space A y β)
-      ( Nxy α β)
-
-  short-map-short-function-cauchy-approximation-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)
-```
-
-### The image of a Cauchy approximation in the Cauchy pseudocompletion is convergent
-
-```agda
-module _
-  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
-  (u : cauchy-approximation-Pseudometric-Space M)
-  where
+          ( lim-u))
+        ( inv-sim-Pseudometric-Space
+          ( cauchy-pseudocompletion-Pseudometric-Space M)
+          ( u~v)))
 
-  is-limit-map-cauchy-approximation-cauchy-pseudocompletion-Ppseudometric-Space :
-    is-limit-cauchy-approximation-Pseudometric-Space
+  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)
-      ( map-short-function-cauchy-approximation-Pseudometric-Space
-        ( M)
-        ( cauchy-pseudocompletion-Pseudometric-Space M)
-        ( short-map-cauchy-pseudocompletion-Pseudometric-Space M)
-        ( u))
       ( u)
-  is-limit-map-cauchy-approximation-cauchy-pseudocompletion-Ppseudometric-Space
-    ε δ α β =
-    symmetric-neighborhood-Pseudometric-Space M
-      ( (α +ℚ⁺ β) +ℚ⁺ (ε +ℚ⁺ δ))
-      ( map-cauchy-approximation-Pseudometric-Space M u β)
-      ( map-cauchy-approximation-Pseudometric-Space M u ε)
-      ( monotonic-neighborhood-Pseudometric-Space M
-        ( map-cauchy-approximation-Pseudometric-Space M u β)
-        ( map-cauchy-approximation-Pseudometric-Space M u ε)
-        ( β +ℚ⁺ ε)
-        ( (α +ℚ⁺ β) +ℚ⁺ (ε +ℚ⁺ δ))
-        ( preserves-le-add-ℚ
-          { rational-ℚ⁺ β}
-          { rational-ℚ⁺ (α +ℚ⁺ β)}
-          { rational-ℚ⁺ ε}
-          { rational-ℚ⁺ (ε +ℚ⁺ δ)}
-          ( le-right-add-ℚ⁺ α β)
-          ( le-left-add-ℚ⁺ ε δ))
-        ( is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space
-          ( M)
-          ( u)
-          ( β)
-          ( ε)))
-
-  sim-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :
-    sim-Pseudometric-Space
-      ( cauchy-pseudocompletion-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space M))
-      ( map-short-function-cauchy-approximation-Pseudometric-Space
-        ( M)
-        ( cauchy-pseudocompletion-Pseudometric-Space M)
-        ( short-map-cauchy-pseudocompletion-Pseudometric-Space M)
-        ( u))
-      ( map-cauchy-pseudocompletion-Pseudometric-Space
-        ( cauchy-pseudocompletion-Pseudometric-Space M)
-        ( u))
-  sim-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space =
-    sim-const-is-limit-cauchy-approximation-Pseudometric-Space
+      ( v)
+  sim-has-same-limit-cauchy-approximation-Pseudometric-Space lim-u lim-v =
+    transitive-sim-Pseudometric-Space
       ( cauchy-pseudocompletion-Pseudometric-Space M)
-      ( map-short-function-cauchy-approximation-Pseudometric-Space
-        ( M)
-        ( cauchy-pseudocompletion-Pseudometric-Space M)
-        ( short-map-cauchy-pseudocompletion-Pseudometric-Space M)
-        ( u))
       ( u)
-      ( is-limit-map-cauchy-approximation-cauchy-pseudocompletion-Ppseudometric-Space)
+      ( 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)
 ```
diff --git a/src/metric-spaces/dependent-products-metric-spaces.lagda.md b/src/metric-spaces/dependent-products-metric-spaces.lagda.md
index 2675d11b69..993b77a8ba 100644
--- a/src/metric-spaces/dependent-products-metric-spaces.lagda.md
+++ b/src/metric-spaces/dependent-products-metric-spaces.lagda.md
@@ -15,6 +15,7 @@ open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
 
+open import metric-spaces.action-on-cauchy-approximations-short-maps-metric-spaces
 open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.complete-metric-spaces
 open import metric-spaces.convergent-cauchy-approximations-metric-spaces
diff --git a/src/metric-spaces/extensions-metric-spaces.lagda.md b/src/metric-spaces/extensions-metric-spaces.lagda.md
new file mode 100644
index 0000000000..0c9e9f6450
--- /dev/null
+++ b/src/metric-spaces/extensions-metric-spaces.lagda.md
@@ -0,0 +1,83 @@
+# Extensions of metric spaces
+
+```agda
+module metric-spaces.extensions-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import metric-spaces.cauchy-approximations-metric-spaces
+open import metric-spaces.cauchy-pseudocompletion-of-metric-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.isometries-metric-spaces
+open import metric-spaces.limits-of-cauchy-approximations-metric-spaces
+open import metric-spaces.metric-spaces
+```
+
+</details>
+
+## Idea
+
+An
+{{#concept "extension" Disambiguation="of a metric space" Agda=extension-Metric-Space}}
+of a [metric space](metric-spaces.metric-spaces.md) `P`is a metric space `Q`
+together with an [isometry](metric-spaces.isometries-metric-spaces.md)
+`i : P → Q`.
+
+## Definition
+
+### Extensions of metric spaces
+
+```agda
+module _
+  {l1 l2 : Level}
+  (l3 l4 : Level)
+  (P : Metric-Space l1 l2)
+  where
+
+  extension-Metric-Space : UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4)
+  extension-Metric-Space =
+    Σ ( Metric-Space l3 l4)
+      ( isometry-Metric-Space P)
+
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Metric-Space l1 l2)
+  (E : extension-Metric-Space l3 l4 P)
+  where
+
+  metric-space-extension-Metric-Space : Metric-Space l3 l4
+  metric-space-extension-Metric-Space = pr1 E
+
+  isometry-metric-space-extension-Metric-Space :
+    isometry-Metric-Space
+      ( P)
+      ( metric-space-extension-Metric-Space)
+  isometry-metric-space-extension-Metric-Space = pr2 E
+
+  map-isometry-metric-space-extension-Metric-Space :
+    type-Metric-Space P →
+    type-Metric-Space metric-space-extension-Metric-Space
+  map-isometry-metric-space-extension-Metric-Space =
+    map-isometry-Metric-Space
+      ( P)
+      ( metric-space-extension-Metric-Space)
+      ( isometry-metric-space-extension-Metric-Space)
+
+  is-isometry-map-extension-Metric-Space :
+    is-isometry-Metric-Space
+      ( P)
+      ( metric-space-extension-Metric-Space)
+      ( map-isometry-metric-space-extension-Metric-Space)
+  is-isometry-map-extension-Metric-Space =
+    is-isometry-map-isometry-Metric-Space
+      ( P)
+      ( metric-space-extension-Metric-Space)
+      ( isometry-metric-space-extension-Metric-Space)
+```
diff --git a/src/metric-spaces/extensions-pseudometric-spaces.lagda.md b/src/metric-spaces/extensions-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..c05d1f55bb
--- /dev/null
+++ b/src/metric-spaces/extensions-pseudometric-spaces.lagda.md
@@ -0,0 +1,77 @@
+# Extensions of pseudometric spaces
+
+```agda
+module metric-spaces.extensions-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import metric-spaces.isometries-pseudometric-spaces
+open import metric-spaces.pseudometric-spaces
+```
+
+</details>
+
+## Idea
+
+An
+{{#concept "extension" Disambiguation="of a pseudometric space" Agda=extension-Pseudometric-Space}}
+of a [pseudometric space](metric-spaces.pseudometric-spaces.md) `P`is a
+pseudometric space `Q` together with an
+[isometry](metric-spaces.isometries-pseudometric-spaces.md) `i : P → Q`.
+
+## Definition
+
+### Extensions of pseudometric spaces
+
+```agda
+module _
+  {l1 l2 : Level}
+  (l3 l4 : Level)
+  (P : Pseudometric-Space l1 l2)
+  where
+
+  extension-Pseudometric-Space : UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4)
+  extension-Pseudometric-Space =
+    Σ ( Pseudometric-Space l3 l4)
+      ( isometry-Pseudometric-Space P)
+
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Pseudometric-Space l1 l2)
+  (E : extension-Pseudometric-Space l3 l4 P)
+  where
+
+  pseudometric-space-extension-Pseudometric-Space : Pseudometric-Space l3 l4
+  pseudometric-space-extension-Pseudometric-Space = pr1 E
+
+  isometry-pseudometric-space-extension-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( P)
+      ( pseudometric-space-extension-Pseudometric-Space)
+  isometry-pseudometric-space-extension-Pseudometric-Space = pr2 E
+
+  map-isometry-pseudometric-space-extension-Pseudometric-Space :
+    type-Pseudometric-Space P →
+    type-Pseudometric-Space pseudometric-space-extension-Pseudometric-Space
+  map-isometry-pseudometric-space-extension-Pseudometric-Space =
+    map-isometry-Pseudometric-Space
+      ( P)
+      ( pseudometric-space-extension-Pseudometric-Space)
+      ( isometry-pseudometric-space-extension-Pseudometric-Space)
+
+  is-isometry-map-extension-Pseudometric-Space :
+    is-isometry-Pseudometric-Space
+      ( P)
+      ( pseudometric-space-extension-Pseudometric-Space)
+      ( map-isometry-pseudometric-space-extension-Pseudometric-Space)
+  is-isometry-map-extension-Pseudometric-Space =
+    is-isometry-map-isometry-Pseudometric-Space
+      ( P)
+      ( pseudometric-space-extension-Pseudometric-Space)
+      ( isometry-pseudometric-space-extension-Pseudometric-Space)
+```
diff --git a/src/metric-spaces/indexed-sums-metric-spaces.lagda.md b/src/metric-spaces/indexed-sums-metric-spaces.lagda.md
index 4ed15b71da..c07e513fe3 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-metric-spaces.lagda.md b/src/metric-spaces/isometries-metric-spaces.lagda.md
index 3fee4dcad8..92c1c0a3e8 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 35d81a521c..7147daf5c0 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 d9a5fe6ea1..38768d09c1 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,14 +10,12 @@ 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.action-on-cauchy-approximations-short-maps-metric-spaces
 open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces
 open import metric-spaces.metric-spaces
diff --git a/src/metric-spaces/metric-extensions-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-extensions-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..7c4c2ead07
--- /dev/null
+++ b/src/metric-spaces/metric-extensions-pseudometric-spaces.lagda.md
@@ -0,0 +1,288 @@
+# Metric extensions of pseudometric spaces
+
+```agda
+module metric-spaces.metric-extensions-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.universe-levels
+
+open import metric-spaces.action-on-cauchy-approximations-isometries-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.extensionality-pseudometric-spaces
+open import metric-spaces.extensions-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.metric-spaces
+open import metric-spaces.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`.
+
+This is equivalent to the type of
+{{#concept "extensional extensions" Disambiguation="of a pseudometric space" Agda=extensional-extension-Pseudometric-Space}},
+[extensions](metric-spaces.extensions-pseudometric-spaces.md) of pseudometric
+spaces `i  : P → Q` such that `Q` is
+[extensional](metric-spaces.extensionality-pseudometric-spaces.md).
+
+## 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)
+```
+
+### Extensional extensions of pseudometric spaces
+
+```agda
+module _
+  {l1 l2 : Level}
+  (l3 l4 : Level)
+  (P : Pseudometric-Space l1 l2)
+  where
+
+  is-extensional-prop-extension-Pseudometric-Space :
+    extension-Pseudometric-Space l3 l4 P → Prop (l3 ⊔ l4)
+  is-extensional-prop-extension-Pseudometric-Space M =
+    is-extensional-prop-Pseudometric-Space
+      ( pseudometric-space-extension-Pseudometric-Space P M)
+
+  extensional-extension-Pseudometric-Space : UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4)
+  extensional-extension-Pseudometric-Space =
+    type-subtype
+      (is-extensional-prop-extension-Pseudometric-Space)
+```
+
+## Properties
+
+### Metric extensions are equivalent to extensional extensions of pseudometric spaces
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Pseudometric-Space l1 l2)
+  where
+
+  equiv-extensional-extension-Metric-Extension :
+    Metric-Extension l3 l4 P ≃ extensional-extension-Pseudometric-Space l3 l4 P
+  equiv-extensional-extension-Metric-Extension = equiv-right-swap-Σ
+```
+
+### 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 ffecd0aafc..d4228503f3 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/metric-space-of-cauchy-approximations-metric-spaces.lagda.md b/src/metric-spaces/metric-space-of-cauchy-approximations-metric-spaces.lagda.md
index 85dc63e6e8..9c7767b0ce 100644
--- a/src/metric-spaces/metric-space-of-cauchy-approximations-metric-spaces.lagda.md
+++ b/src/metric-spaces/metric-space-of-cauchy-approximations-metric-spaces.lagda.md
@@ -17,6 +17,7 @@ open import foundation.involutions
 open import foundation.subtypes
 open import foundation.universe-levels
 
+open import metric-spaces.action-on-cauchy-approximations-short-maps-metric-spaces
 open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.dependent-products-metric-spaces
 open import metric-spaces.equality-of-metric-spaces
diff --git a/src/metric-spaces/metric-spaces.lagda.md b/src/metric-spaces/metric-spaces.lagda.md
index 25fbe2e982..36aac19425 100644
--- a/src/metric-spaces/metric-spaces.lagda.md
+++ b/src/metric-spaces/metric-spaces.lagda.md
@@ -317,6 +317,10 @@ module _
   set-Metric-Space : Set l1
   set-Metric-Space =
     (type-Metric-Space A , is-set-type-Metric-Space)
+
+  eq-prop-Metric-Space :
+    (x y : type-Metric-Space A) → Prop l1
+  eq-prop-Metric-Space = Id-Prop set-Metric-Space
 ```
 
 ### Similarity of elements in a metric space is equivalent to equality
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 ba315c5ba8..04989c2bea 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 6d3251395d..c494f32b3d 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/rational-cauchy-approximations.lagda.md b/src/metric-spaces/rational-cauchy-approximations.lagda.md
index d5f5d1b432..1da25063ea 100644
--- a/src/metric-spaces/rational-cauchy-approximations.lagda.md
+++ b/src/metric-spaces/rational-cauchy-approximations.lagda.md
@@ -19,6 +19,7 @@ open import foundation.propositions
 open import foundation.subtypes
 open import foundation.universe-levels
 
+open import metric-spaces.action-on-cauchy-approximations-short-maps-metric-spaces
 open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.complete-metric-spaces
 open import metric-spaces.convergent-cauchy-approximations-metric-spaces
diff --git a/src/metric-spaces/short-functions-metric-spaces.lagda.md b/src/metric-spaces/short-functions-metric-spaces.lagda.md
index 64e55931bc..e0cb7d72f2 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 2075b6e100..c4e262d3a3 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 f9caa041d2..6a249158e4 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)
 ```
diff --git a/src/real-numbers/proper-closed-intervals-real-numbers.lagda.md b/src/real-numbers/proper-closed-intervals-real-numbers.lagda.md
index 21f5ab7e36..082ca043df 100644
--- a/src/real-numbers/proper-closed-intervals-real-numbers.lagda.md
+++ b/src/real-numbers/proper-closed-intervals-real-numbers.lagda.md
@@ -20,6 +20,7 @@ open import foundation.subtypes
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
+open import metric-spaces.action-on-cauchy-approximations-short-maps-metric-spaces
 open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.closed-subsets-metric-spaces
 open import metric-spaces.complete-metric-spaces