diff --git a/src/foundation/equivalence-classes.lagda.md b/src/foundation/equivalence-classes.lagda.md
index 71954bae57..39adccde10 100644
--- a/src/foundation/equivalence-classes.lagda.md
+++ b/src/foundation/equivalence-classes.lagda.md
@@ -8,11 +8,15 @@ module foundation.equivalence-classes where
 
 ```agda
 open import foundation.conjunction
+open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.effective-maps-equivalence-relations
+open import foundation.equivalences
 open import foundation.existential-quantification
+open import foundation.function-types
 open import foundation.functoriality-propositional-truncation
 open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
 open import foundation.inhabited-subtypes
 open import foundation.locally-small-types
 open import foundation.logical-equivalences
@@ -23,13 +27,13 @@ open import foundation.small-types
 open import foundation.subtype-identity-principle
 open import foundation.subtypes
 open import foundation.surjective-maps
+open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universal-property-image
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
 open import foundation-core.embeddings
 open import foundation-core.equivalence-relations
-open import foundation-core.equivalences
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.identity-types
 open import foundation-core.propositions
@@ -315,12 +319,13 @@ module _
       ( λ D → is-in-equivalence-class-Prop R D a)
       ( eq-class-equivalence-class R C H)
 
-  is-torsorial-is-in-equivalence-class :
-    is-torsorial (λ P → is-in-equivalence-class R P a)
-  pr1 is-torsorial-is-in-equivalence-class =
-    center-total-is-in-equivalence-class
-  pr2 is-torsorial-is-in-equivalence-class =
-    contraction-total-is-in-equivalence-class
+  abstract
+    is-torsorial-is-in-equivalence-class :
+      is-torsorial (λ P → is-in-equivalence-class R P a)
+    pr1 is-torsorial-is-in-equivalence-class =
+      center-total-is-in-equivalence-class
+    pr2 is-torsorial-is-in-equivalence-class =
+      contraction-total-is-in-equivalence-class
 
   is-in-equivalence-class-eq-equivalence-class :
     (q : equivalence-class R) → class R a ＝ q →
@@ -338,6 +343,26 @@ module _
         ( is-in-equivalence-class-eq-equivalence-class)
 ```
 
+### Σ-decompositions of types induced by equivalence classes
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  equiv-total-is-in-equivalence-class :
+    Σ A (λ x → Σ (equivalence-class R) (λ X → is-in-equivalence-class R X x)) ≃
+    ( A)
+  equiv-total-is-in-equivalence-class =
+    right-unit-law-Σ-is-contr
+      ( is-torsorial-is-in-equivalence-class R)
+
+  Σ-decomposition-is-in-equivalence-class :
+    Σ (equivalence-class R) (type-subtype ∘ is-in-equivalence-class-Prop R) ≃ A
+  Σ-decomposition-is-in-equivalence-class =
+    equiv-total-is-in-equivalence-class ∘e equiv-left-swap-Σ
+```
+
 ### The map `class : A → equivalence-class R` is an effective quotient map
 
 ```agda
diff --git a/src/foundation/set-quotients.lagda.md b/src/foundation/set-quotients.lagda.md
index 26fd53a4bf..4ed14ec988 100644
--- a/src/foundation/set-quotients.lagda.md
+++ b/src/foundation/set-quotients.lagda.md
@@ -8,18 +8,29 @@ module foundation.set-quotients where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.contractible-maps
+open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.effective-maps-equivalence-relations
 open import foundation.embeddings
+open import foundation.equality-dependent-pair-types
 open import foundation.equivalence-classes
 open import foundation.equivalences
+open import foundation.fibers-of-maps
 open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.inhabited-subtypes
+open import foundation.logical-equivalences
 open import foundation.reflecting-maps-equivalence-relations
 open import foundation.sets
 open import foundation.slice
 open import foundation.surjective-maps
+open import foundation.torsorial-type-families
+open import foundation.transport-along-identifications
+open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.uniqueness-set-quotients
 open import foundation.universal-property-image
 open import foundation.universal-property-set-quotients
@@ -27,9 +38,7 @@ open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import foundation-core.equivalence-relations
-open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-function-types
-open import foundation-core.homotopies
 open import foundation-core.propositions
 open import foundation-core.small-types
 open import foundation-core.subtypes
@@ -152,7 +161,38 @@ module _
       ( is-surjective-quotient-map)
 ```
 
-### The map `class : A → equivalence-class R` is an effective quotient map
+### Any element is in the class of its quotient
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  is-in-equivalence-class-quotient-map-set-quotient :
+    (x : A) →
+    is-in-equivalence-class-set-quotient
+      ( R)
+      ( quotient-map R x)
+      ( x)
+  is-in-equivalence-class-quotient-map-set-quotient x =
+    is-in-equivalence-class-eq-equivalence-class
+      ( R)
+      ( x)
+      ( equivalence-class-set-quotient R (quotient-map R x))
+      ( inv
+        ( is-retraction-equivalence-class-set-quotient R (class R x)))
+
+  inhabitant-equivalence-class-quotient-map-set-quotient :
+    (x : A) →
+    type-subtype
+      ( subtype-set-quotient R (quotient-map R x))
+  inhabitant-equivalence-class-quotient-map-set-quotient x =
+    (x , is-in-equivalence-class-quotient-map-set-quotient x)
+```
+
+## Properties
+
+### The map `class : A → set-quotient R` is an effective quotient map
 
 ```agda
 module _
@@ -417,6 +457,127 @@ module _
       B f Uf
 ```
 
+### Any quotient class containing a given element `x` is equal to `quotient-map x`
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  eq-set-quotient-equivalence-class-set-quotient :
+    (X : set-quotient R) {x : A} →
+    is-in-equivalence-class-set-quotient R X x →
+    quotient-map R x ＝ X
+  eq-set-quotient-equivalence-class-set-quotient X {x} H =
+    ( ap
+      ( set-quotient-equivalence-class R)
+      ( eq-class-equivalence-class
+        ( R)
+        ( equivalence-class-set-quotient R X)
+        ( H))) ∙
+    ( is-section-equivalence-class-set-quotient R X)
+```
+
+### Two quotient classes that contain similar elements are equal
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  eq-set-quotient-sim-element-set-quotient :
+    (X : set-quotient R) {x : A} →
+    (Y : set-quotient R) {y : A} →
+    is-in-equivalence-class-set-quotient R X x →
+    is-in-equivalence-class-set-quotient R Y y →
+    sim-equivalence-relation R x y →
+    X ＝ Y
+  eq-set-quotient-sim-element-set-quotient X {x} Y {y} x∈X y∈Y x~y =
+    ( ( inv (eq-set-quotient-equivalence-class-set-quotient R X x∈X)) ∙
+      ( apply-effectiveness-quotient-map' R x~y) ∙
+      ( eq-set-quotient-equivalence-class-set-quotient R Y y∈Y))
+```
+
+### Any element in the quotient class of another is similar to it
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  sim-is-in-equivalence-class-set-quotient :
+    (x y : A) →
+    is-in-equivalence-class-set-quotient
+      ( R)
+      ( quotient-map R x)
+      ( y) →
+    sim-equivalence-relation R x y
+  sim-is-in-equivalence-class-set-quotient x y y∈X =
+    apply-effectiveness-quotient-map
+      ( R)
+      ( inv
+        ( eq-set-quotient-equivalence-class-set-quotient
+          ( R)
+          ( quotient-map R x)
+          ( y∈X)))
+```
+
+### Σ-decompositions of types induced by set quotients
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  abstract
+    is-torsorial-is-in-equivalence-class-set-quotient :
+      (x : A) →
+      is-contr
+        ( Σ ( set-quotient R)
+            ( λ X → is-in-equivalence-class-set-quotient R X x))
+    is-torsorial-is-in-equivalence-class-set-quotient x =
+      is-contr-equiv'
+        ( Σ (equivalence-class R) (λ X → is-in-equivalence-class R X x))
+        ( equiv-Σ
+          ( λ X → is-in-equivalence-class-set-quotient R X x)
+          ( compute-set-quotient R)
+          ( λ X →
+            equiv-iff-is-prop
+              ( is-prop-is-in-equivalence-class R X x)
+              ( is-prop-is-in-equivalence-class-set-quotient
+                ( R)
+                ( set-quotient-equivalence-class R X)
+                ( x))
+              ( λ x∈X →
+                inv-tr
+                  ( λ Y → is-in-equivalence-class R Y x)
+                  ( is-retraction-equivalence-class-set-quotient R X)
+                  ( x∈X))
+              ( λ x∈X →
+                tr
+                  ( λ Y → is-in-equivalence-class R Y x)
+                  ( is-retraction-equivalence-class-set-quotient R X)
+                  ( x∈X))))
+        ( is-torsorial-is-in-equivalence-class R x)
+
+  equiv-total-is-in-equivalence-class-set-quotient :
+    Σ ( A)
+      ( λ x →
+        Σ ( set-quotient R)
+          ( λ X → is-in-equivalence-class-set-quotient R X x)) ≃
+    ( A)
+  equiv-total-is-in-equivalence-class-set-quotient =
+    right-unit-law-Σ-is-contr
+      ( is-torsorial-is-in-equivalence-class-set-quotient)
+
+  Σ-decomposition-is-in-equivalence-class-set-quotient :
+    Σ ( set-quotient R)
+      ( type-subtype ∘ is-in-equivalence-class-set-quotient-Prop R) ≃
+    ( A)
+  Σ-decomposition-is-in-equivalence-class-set-quotient =
+    equiv-total-is-in-equivalence-class-set-quotient ∘e equiv-left-swap-Σ
+```
+
 ## See also
 
 - [Set coequalizers](foundation.set-coequalizers.md) for an equivalent notion
diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md
index 63dca9f747..504d515b72 100644
--- a/src/metric-spaces.lagda.md
+++ b/src/metric-spaces.lagda.md
@@ -55,6 +55,7 @@ open import metric-spaces.complete-metric-spaces public
 open import metric-spaces.continuous-functions-metric-spaces public
 open import metric-spaces.convergent-cauchy-approximations-metric-spaces public
 open import metric-spaces.convergent-sequences-metric-spaces public
+open import metric-spaces.decomposition-metric-spaces-elements-at-bounded-distance-metric-spaces public
 open import metric-spaces.dependent-products-metric-spaces public
 open import metric-spaces.discrete-metric-spaces public
 open import metric-spaces.elements-at-bounded-distance-metric-spaces public
@@ -74,6 +75,7 @@ open import metric-spaces.limits-of-functions-metric-spaces public
 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.metric-quotients-of-pseudometric-spaces public
 open import metric-spaces.metric-space-of-cauchy-approximations-complete-metric-spaces public
 open import metric-spaces.metric-space-of-cauchy-approximations-metric-spaces public
 open import metric-spaces.metric-space-of-convergent-cauchy-approximations-metric-spaces public
diff --git a/src/metric-spaces/decomposition-metric-spaces-elements-at-bounded-distance-metric-spaces.lagda.md b/src/metric-spaces/decomposition-metric-spaces-elements-at-bounded-distance-metric-spaces.lagda.md
new file mode 100644
index 0000000000..2b4ce0a37e
--- /dev/null
+++ b/src/metric-spaces/decomposition-metric-spaces-elements-at-bounded-distance-metric-spaces.lagda.md
@@ -0,0 +1,364 @@
+# Decomposition of metric spaces as indexed sums of metric spaces with elements at bounded distance
+
+```agda
+module metric-spaces.decomposition-metric-spaces-elements-at-bounded-distance-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.equivalence-classes
+open import foundation.equivalence-relations
+open import foundation.equivalences
+open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.functoriality-propositional-truncation
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.set-quotients
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import metric-spaces.elements-at-bounded-distance-metric-spaces
+open import metric-spaces.equality-of-metric-spaces
+open import metric-spaces.functions-metric-spaces
+open import metric-spaces.indexed-sums-metric-spaces
+open import metric-spaces.isometries-metric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.subspaces-metric-spaces
+```
+
+</details>
+
+## Idea
+
+Any [metric space](metric-spaces.metric-spaces.md) is
+[isometrically equivalent](metric-spaces.equality-of-metric-spaces.md) to its
+{{#concept "Σ-decomposition into subspaces of elements at bounded distance" Agda=Σ-components-at-bounded-distance-Metric-Space}},
+the [indexed sum](metric-spaces.indexed-sums-metric-spaces.md) of its
+[subspaces](metric-spaces.subspaces-metric-spaces.md) of
+[elements at bounded distance](metric-spaces.elements-at-bounded-distance-metric-spaces.md)
+indexed by the [set quotient](foundation.set-quotients.md) of the metric space
+by the [equivalence relation](foundation.equivalence-relations.md) of being at
+bounded distance.
+
+## Definitions
+
+### The set of components of subspaces of elements at bounded distance in a metric space
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  where
+
+  set-components-at-bounded-distance-Metric-Space : Set (l1 ⊔ l2)
+  set-components-at-bounded-distance-Metric-Space =
+    quotient-Set
+      ( equivalence-relation-bounded-dist-Metric-Space A)
+
+  type-components-at-bounded-distance-Metric-Space : UU (l1 ⊔ l2)
+  type-components-at-bounded-distance-Metric-Space =
+    type-Set set-components-at-bounded-distance-Metric-Space
+
+  map-type-components-at-bounded-distance-Metric-Space :
+    type-Metric-Space A →
+    type-components-at-bounded-distance-Metric-Space
+  map-type-components-at-bounded-distance-Metric-Space =
+    quotient-map
+      ( equivalence-relation-bounded-dist-Metric-Space A)
+```
+
+### The metric subspaces of elements at bounded distance in a metric space
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  (x : type-components-at-bounded-distance-Metric-Space A)
+  where
+
+  subspace-components-at-bounded-distance-Metric-Space :
+    Metric-Space (l1 ⊔ l2) l2
+  subspace-components-at-bounded-distance-Metric-Space =
+    subspace-Metric-Space
+      ( A)
+      ( subtype-set-quotient
+        ( equivalence-relation-bounded-dist-Metric-Space A)
+        ( x))
+
+  type-subspace-components-at-bounded-distance-Metric-Space : UU (l1 ⊔ l2)
+  type-subspace-components-at-bounded-distance-Metric-Space =
+    type-Metric-Space
+      subspace-components-at-bounded-distance-Metric-Space
+```
+
+### The sum of metric subspaces of elements at bounded distance indexed by the set of components
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  where
+
+  Σ-components-at-bounded-distance-Metric-Space :
+    Metric-Space (l1 ⊔ l2) (l1 ⊔ l2)
+  Σ-components-at-bounded-distance-Metric-Space =
+    indexed-sum-Metric-Space
+      ( set-components-at-bounded-distance-Metric-Space A)
+      ( subspace-components-at-bounded-distance-Metric-Space A)
+
+  type-Σ-components-at-bounded-distance-Metric-Space : UU (l1 ⊔ l2)
+  type-Σ-components-at-bounded-distance-Metric-Space =
+    type-Metric-Space Σ-components-at-bounded-distance-Metric-Space
+```
+
+## Properties
+
+### All elements in a subspace of elements at bounded distance are at bounded distance
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  (X : type-components-at-bounded-distance-Metric-Space A)
+  where
+
+  all-elements-at-bounded-distance-subspace-components-at-bounded-distance-Metric-Space :
+    (x y : type-subspace-components-at-bounded-distance-Metric-Space A X) →
+    bounded-dist-Metric-Space
+      ( subspace-components-at-bounded-distance-Metric-Space A X)
+      ( x)
+      ( y)
+  all-elements-at-bounded-distance-subspace-components-at-bounded-distance-Metric-Space
+    (x , x∈X) (y , y∈X) =
+    apply-effectiveness-quotient-map
+      ( equivalence-relation-bounded-dist-Metric-Space A)
+      ( ( eq-set-quotient-equivalence-class-set-quotient
+          ( equivalence-relation-bounded-dist-Metric-Space A)
+          ( X)
+          ( x∈X)) ∙
+        ( inv
+          ( eq-set-quotient-equivalence-class-set-quotient
+            ( equivalence-relation-bounded-dist-Metric-Space A)
+            ( X)
+            ( y∈X))))
+```
+
+### Neighborhoods in subspaces of equal components are neigborhoods in the ambient metric space
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  where
+
+  lemma-iff-neighborhood-Σ-components-at-bounded-distance-Metric-Space :
+    ( d : ℚ⁺) →
+    ( X Y : type-components-at-bounded-distance-Metric-Space A) →
+    ( eqXY : X ＝ Y) →
+    ( x : type-subspace-components-at-bounded-distance-Metric-Space A X) →
+    ( y : type-subspace-components-at-bounded-distance-Metric-Space A Y) →
+    ( neighborhood-Metric-Space
+      ( subspace-components-at-bounded-distance-Metric-Space A Y)
+      ( d)
+      ( tr
+        ( type-Metric-Space ∘
+          subspace-components-at-bounded-distance-Metric-Space A)
+        ( eqXY)
+        ( x))
+      ( y)) ↔
+    neighborhood-Metric-Space A d (pr1 x) (pr1 y)
+  lemma-iff-neighborhood-Σ-components-at-bounded-distance-Metric-Space
+    d X .X refl (x , x∈X) (y , y∈X) = id-iff
+```
+
+### Any metric space is isometrically equivalent to the indexed sum of its subspaces of components of elements at bounded distance
+
+#### Equivalence of underlying types
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  where
+
+  equiv-type-Σ-components-at-bounded-distance-Metric-Space :
+    type-Σ-components-at-bounded-distance-Metric-Space A ≃
+    type-Metric-Space A
+  equiv-type-Σ-components-at-bounded-distance-Metric-Space =
+    Σ-decomposition-is-in-equivalence-class-set-quotient
+      ( equivalence-relation-bounded-dist-Metric-Space A)
+
+  map-equiv-Σ-components-at-bounded-distance-Metric-Space :
+    type-function-Metric-Space
+      ( Σ-components-at-bounded-distance-Metric-Space A)
+      ( A)
+  map-equiv-Σ-components-at-bounded-distance-Metric-Space =
+    map-equiv
+      ( equiv-type-Σ-components-at-bounded-distance-Metric-Space)
+```
+
+#### The equivalence between a metric space and its decompositions into subspaces of elements at bounded distance is an isometry
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  where
+
+  preserves-neighborhood-map-equiv-Σ-components-at-bounded-distance-Metric-Space :
+    ( d : ℚ⁺)
+    ( x y : type-Σ-components-at-bounded-distance-Metric-Space A) →
+    neighborhood-Metric-Space
+      ( Σ-components-at-bounded-distance-Metric-Space A)
+      ( d)
+      ( x)
+      ( y) →
+    neighborhood-Metric-Space A d
+      ( map-equiv-Σ-components-at-bounded-distance-Metric-Space A x)
+      ( map-equiv-Σ-components-at-bounded-distance-Metric-Space A y)
+  preserves-neighborhood-map-equiv-Σ-components-at-bounded-distance-Metric-Space
+    d (X , x , x∈X) (Y , y , y∈Y) (X=Y , Nxy) =
+    forward-implication
+      ( lemma-iff-neighborhood-Σ-components-at-bounded-distance-Metric-Space
+        ( A)
+        ( d)
+        ( X)
+        ( Y)
+        ( X=Y)
+        ( x , x∈X)
+        ( y , y∈Y))
+      ( Nxy)
+
+  reflects-neighborhood-map-equiv-Σ-components-at-bounded-distance-Metric-Space :
+    ( d : ℚ⁺)
+    ( x y : type-Σ-components-at-bounded-distance-Metric-Space A) →
+    neighborhood-Metric-Space A d
+      ( map-equiv-Σ-components-at-bounded-distance-Metric-Space A x)
+      ( map-equiv-Σ-components-at-bounded-distance-Metric-Space A y) →
+    neighborhood-Metric-Space
+      ( Σ-components-at-bounded-distance-Metric-Space A)
+      ( d)
+      ( x)
+      ( y)
+  reflects-neighborhood-map-equiv-Σ-components-at-bounded-distance-Metric-Space
+    d (X , x , x∈X) (Y , y , y∈Y) Nxy =
+    ( lemma-eq ,
+      backward-implication
+        ( lemma-iff-neighborhood-Σ-components-at-bounded-distance-Metric-Space
+          ( A)
+          ( d)
+          ( X)
+          ( Y)
+          ( lemma-eq)
+          ( x , x∈X)
+          ( y , y∈Y))
+        ( Nxy))
+    where
+
+      lemma-eq-Y :
+        map-type-components-at-bounded-distance-Metric-Space A y ＝ Y
+      lemma-eq-Y =
+        eq-set-quotient-equivalence-class-set-quotient
+          ( equivalence-relation-bounded-dist-Metric-Space A)
+          ( Y)
+          ( y∈Y)
+
+      lemma-eq-X :
+        map-type-components-at-bounded-distance-Metric-Space A x ＝ X
+      lemma-eq-X =
+        eq-set-quotient-equivalence-class-set-quotient
+          ( equivalence-relation-bounded-dist-Metric-Space A)
+          ( X)
+          ( x∈X)
+
+      lemma-eq-map-type-components-at-bounded-distance-Metric-Space :
+        ( map-type-components-at-bounded-distance-Metric-Space A x) ＝
+        ( map-type-components-at-bounded-distance-Metric-Space A y)
+      lemma-eq-map-type-components-at-bounded-distance-Metric-Space =
+        apply-effectiveness-quotient-map'
+          ( equivalence-relation-bounded-dist-Metric-Space A)
+          ( unit-trunc-Prop (d , Nxy))
+
+      lemma-eq : X ＝ Y
+      lemma-eq =
+        ( inv lemma-eq-X) ∙
+        ( lemma-eq-map-type-components-at-bounded-distance-Metric-Space) ∙
+        ( lemma-eq-Y)
+
+  is-isometry-map-equiv-Σ-components-at-bounded-distance-Metric-Space :
+    is-isometry-Metric-Space
+      ( Σ-components-at-bounded-distance-Metric-Space A)
+      ( A)
+      ( map-equiv-Σ-components-at-bounded-distance-Metric-Space A)
+  is-isometry-map-equiv-Σ-components-at-bounded-distance-Metric-Space d x y =
+    ( ( preserves-neighborhood-map-equiv-Σ-components-at-bounded-distance-Metric-Space
+        ( d)
+        ( x)
+        ( y)) ,
+      ( reflects-neighborhood-map-equiv-Σ-components-at-bounded-distance-Metric-Space
+        ( d)
+        ( x)
+        ( y)))
+```
+
+#### The isometric equivalence between a metric space and its decompositions into subspaces of elements at bounded distance
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  where
+
+  isometric-equiv-Σ-components-at-bounded-distance-Metric-Space :
+    isometric-equiv-Metric-Space
+      ( Σ-components-at-bounded-distance-Metric-Space A)
+      ( A)
+  isometric-equiv-Σ-components-at-bounded-distance-Metric-Space =
+    ( equiv-type-Σ-components-at-bounded-distance-Metric-Space A ,
+      is-isometry-map-equiv-Σ-components-at-bounded-distance-Metric-Space A)
+```
+
+### The decomposition into subspaces of elements at bounded distance is idempotent
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  where
+
+  idempotent-Σ-components-at-bounded-distance-Metric-Space :
+    Σ-components-at-bounded-distance-Metric-Space
+      ( Σ-components-at-bounded-distance-Metric-Space A) ＝
+    Σ-components-at-bounded-distance-Metric-Space A
+  idempotent-Σ-components-at-bounded-distance-Metric-Space =
+    eq-isometric-equiv-Metric-Space
+      ( Σ-components-at-bounded-distance-Metric-Space
+        ( Σ-components-at-bounded-distance-Metric-Space A))
+      ( Σ-components-at-bounded-distance-Metric-Space A)
+      ( isometric-equiv-Σ-components-at-bounded-distance-Metric-Space
+        ( Σ-components-at-bounded-distance-Metric-Space A))
+```
+
+### Universal property of the decomposition into subspaces of elements at bounded distance
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  where
+
+  eq-Σ-components-at-bounded-distance-Metric-Space :
+    (M : Metric-Space (l1 ⊔ l2) (l1 ⊔ l2)) →
+    isometric-equiv-Metric-Space A M →
+    Σ-components-at-bounded-distance-Metric-Space A ＝ M
+  eq-Σ-components-at-bounded-distance-Metric-Space M isometric-equiv-M =
+    eq-isometric-equiv-Metric-Space
+      ( Σ-components-at-bounded-distance-Metric-Space A)
+      ( M)
+      ( comp-isometric-equiv-Metric-Space
+        ( Σ-components-at-bounded-distance-Metric-Space A)
+        ( A)
+        ( M)
+        ( isometric-equiv-M)
+        ( isometric-equiv-Σ-components-at-bounded-distance-Metric-Space A))
+```
diff --git a/src/metric-spaces/equality-of-metric-spaces.lagda.md b/src/metric-spaces/equality-of-metric-spaces.lagda.md
index d66c56acff..f589d893af 100644
--- a/src/metric-spaces/equality-of-metric-spaces.lagda.md
+++ b/src/metric-spaces/equality-of-metric-spaces.lagda.md
@@ -201,6 +201,27 @@ module _
         ( is-torsorial-Id A)
 ```
 
+### Composition of isometric equivalences
+
+```agda
+module _
+  {la la' lb lb' lc lc' : Level}
+  (A : Metric-Space la la') (B : Metric-Space lb lb') (C : Metric-Space lc lc')
+  where
+
+  comp-isometric-equiv-Metric-Space :
+    isometric-equiv-Metric-Space B C →
+    isometric-equiv-Metric-Space A B →
+    isometric-equiv-Metric-Space A C
+  comp-isometric-equiv-Metric-Space (B≃C , isometry-B≃C) (A≃B , isometry-A≃B) =
+    ( B≃C ∘e A≃B ,
+      is-isometry-comp-is-isometry-Metric-Space A B C
+        ( map-equiv B≃C)
+        ( map-equiv A≃B)
+        ( isometry-B≃C)
+        ( isometry-A≃B))
+```
+
 ### Two metric spaces are isometrically equivalent if and only if there is an isometric equivalence between them
 
 ```agda
diff --git a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..36d41a5dd3
--- /dev/null
+++ b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md
@@ -0,0 +1,790 @@
+# Metric quotients of pseudometric spaces
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module metric-spaces.metric-quotients-of-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-relations
+open import foundation.binary-transport
+open import foundation.contractible-maps
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equivalence-classes
+open import foundation.equivalences
+open import foundation.existential-quantification
+open import foundation.fibers-of-maps
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.reflecting-maps-equivalence-relations
+open import foundation.retractions
+open import foundation.sections
+open import foundation.set-quotients
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universal-property-set-quotients
+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.convergent-cauchy-approximations-metric-spaces
+open import metric-spaces.equality-of-metric-spaces
+open import metric-spaces.extensionality-pseudometric-spaces
+open import metric-spaces.functions-metric-spaces
+open import metric-spaces.isometries-metric-spaces
+open import metric-spaces.isometries-pseudometric-spaces
+open import metric-spaces.limits-of-cauchy-approximations-metric-spaces
+open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.pseudometric-spaces
+open import metric-spaces.rational-neighborhood-relations
+open import metric-spaces.short-functions-metric-spaces
+open import metric-spaces.short-functions-pseudometric-spaces
+open import metric-spaces.similarity-of-elements-pseudometric-spaces
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "metric quotient" Disambiguation="of a pseudometric space" Agda=metric-quotient-Pseudometric-Space}}
+of a [pseudometric space](metric-spaces.pseudometric-spaces.md) is the
+[metric space](metric-spaces.metric-spaces.md) whose points are
+[quotient classes](foundation.set-quotients.md) of `M` by the
+[similarity relation](metric-spaces.similarity-of-elements-pseudometric-spaces.md)
+and [neighborhoods](metric-spaces.rational-neighborhood-relations.md) given by
+neighborhoods of inhabitants of the quotient classes: two quotient classes `X`,
+`Y` are in a `d`-neighborhood if for all `x ∈ X` and `y ∈ Y`, `x` and `y` are
+`d`-neighbors in the pseudometric space.
+
+Any metric space is
+[isometrically equivalent](metric-spaces.equality-of-metric-spaces.md) to its
+induced metric space.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  set-metric-quotient-Pseudometric-Space : Set (l1 ⊔ l2)
+  set-metric-quotient-Pseudometric-Space =
+    quotient-Set (equivalence-relation-sim-Pseudometric-Space M)
+
+  type-metric-quotient-Pseudometric-Space : UU (l1 ⊔ l2)
+  type-metric-quotient-Pseudometric-Space =
+    type-Set set-metric-quotient-Pseudometric-Space
+
+  type-subtype-metric-quotient-Pseudometric-Space :
+    (X : type-metric-quotient-Pseudometric-Space) → UU (l1 ⊔ l2)
+  type-subtype-metric-quotient-Pseudometric-Space X =
+    type-subtype
+      ( subtype-set-quotient
+        ( equivalence-relation-sim-Pseudometric-Space M)
+        ( X))
+
+  neighborhood-prop-metric-quotient-Pseudometric-Space :
+    Rational-Neighborhood-Relation
+      ( l1 ⊔ l2)
+      ( type-metric-quotient-Pseudometric-Space)
+  neighborhood-prop-metric-quotient-Pseudometric-Space ε X Y =
+    Π-Prop
+      ( type-subtype-metric-quotient-Pseudometric-Space X)
+      ( λ (x , x∈X) →
+        Π-Prop
+          ( type-subtype-metric-quotient-Pseudometric-Space Y)
+          ( λ (y , y∈Y) → neighborhood-prop-Pseudometric-Space M ε x y))
+
+  neighborhood-metric-quotient-Pseudometric-Space :
+    ℚ⁺ → Relation (l1 ⊔ l2) type-metric-quotient-Pseudometric-Space
+  neighborhood-metric-quotient-Pseudometric-Space ε X Y =
+    type-Prop (neighborhood-prop-metric-quotient-Pseudometric-Space ε X Y)
+```
+
+## Properties
+
+### The quotient neighborhood relation is reflexive
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    is-reflexive-neighborhood-metric-quotient-Pseudometric-Space :
+      (d : ℚ⁺) (X : type-metric-quotient-Pseudometric-Space M) →
+      neighborhood-metric-quotient-Pseudometric-Space M d X X
+    is-reflexive-neighborhood-metric-quotient-Pseudometric-Space
+      d X (x , x∈X) (y , y∈X) =
+      apply-effectiveness-quotient-map
+        ( equivalence-relation-sim-Pseudometric-Space M)
+        ( ( eq-set-quotient-equivalence-class-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space M)
+            ( X)
+            ( x∈X)) ∙
+          ( inv
+            ( eq-set-quotient-equivalence-class-set-quotient
+              ( equivalence-relation-sim-Pseudometric-Space M)
+              ( X)
+              ( y∈X))))
+        ( d)
+```
+
+### The quotient neighborhood relation is symmetric
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    is-symmetric-neighborhood-metric-quotient-Pseudometric-Space :
+      (d : ℚ⁺) (x y : type-metric-quotient-Pseudometric-Space M) →
+      neighborhood-metric-quotient-Pseudometric-Space M d x y →
+      neighborhood-metric-quotient-Pseudometric-Space M d y x
+    is-symmetric-neighborhood-metric-quotient-Pseudometric-Space
+      d X Y d⟨X,Y⟩ (y , y∈Y) (x , x∈X) =
+      symmetric-neighborhood-Pseudometric-Space
+        ( M)
+        ( d)
+        ( x)
+        ( y)
+        ( d⟨X,Y⟩ (x , x∈X) (y , y∈Y))
+```
+
+### The quotient neighborhood relation is triangular
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  (X Y Z : type-metric-quotient-Pseudometric-Space M)
+  (d₁ d₂ : ℚ⁺)
+  where
+
+  abstract
+    is-triangular-neighborhood-metric-quotient-Pseudometric-Space :
+      neighborhood-metric-quotient-Pseudometric-Space M d₂ Y Z →
+      neighborhood-metric-quotient-Pseudometric-Space M d₁ X Y →
+      neighborhood-metric-quotient-Pseudometric-Space M (d₁ +ℚ⁺ d₂) X Z
+    is-triangular-neighborhood-metric-quotient-Pseudometric-Space
+      d₂⟨Y,Z⟩ d₁⟨X,Y⟩ (x , x∈X) (z , z∈Z) =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( neighborhood-prop-Pseudometric-Space M (d₁ +ℚ⁺ d₂) x z)
+      in do
+        (y , y∈Y) ←
+          is-inhabited-subtype-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space M)
+            ( Y)
+        triangular-neighborhood-Pseudometric-Space
+          ( M)
+          ( x)
+          ( y)
+          ( z)
+          ( d₁)
+          ( d₂)
+          ( d₂⟨Y,Z⟩ (y , y∈Y) (z , z∈Z))
+          ( d₁⟨X,Y⟩ (x , x∈X) (y , y∈Y))
+```
+
+### The quotient neighborhood relation is saturated
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    is-saturated-neighborhood-metric-quotient-Pseudometric-Space :
+      (ε : ℚ⁺) (X Y : type-metric-quotient-Pseudometric-Space M) →
+      ((δ : ℚ⁺) →
+        neighborhood-metric-quotient-Pseudometric-Space M (ε +ℚ⁺ δ) X Y) →
+      neighborhood-metric-quotient-Pseudometric-Space M ε X Y
+    is-saturated-neighborhood-metric-quotient-Pseudometric-Space
+      ε X Y H (x , x∈X) (y , y∈Y) =
+      saturated-neighborhood-Pseudometric-Space M ε x y
+        ( λ δ → H δ (x , x∈X) (y , y∈Y))
+```
+
+### The quotient pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  pseudometric-metric-quotient-Pseudometric-Space :
+    Pseudometric-Space (l1 ⊔ l2) (l1 ⊔ l2)
+  pseudometric-metric-quotient-Pseudometric-Space =
+    ( type-metric-quotient-Pseudometric-Space M ,
+      neighborhood-prop-metric-quotient-Pseudometric-Space M ,
+      is-reflexive-neighborhood-metric-quotient-Pseudometric-Space M ,
+      is-symmetric-neighborhood-metric-quotient-Pseudometric-Space M ,
+      is-triangular-neighborhood-metric-quotient-Pseudometric-Space M ,
+      is-saturated-neighborhood-metric-quotient-Pseudometric-Space M)
+```
+
+### The quotient pseudometric space is tight and extensional
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    is-tight-pseudometric-metric-quotient-Pseudometric-Space :
+      is-tight-Pseudometric-Space
+        (pseudometric-metric-quotient-Pseudometric-Space M)
+    is-tight-pseudometric-metric-quotient-Pseudometric-Space X Y X~Y =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( Id-Prop
+              ( set-metric-quotient-Pseudometric-Space M)
+              ( X)
+              ( Y))
+      in do
+        ( x , x∈X) ←
+          is-inhabited-subtype-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space M)
+            ( X)
+
+        ( y , y∈Y) ←
+          is-inhabited-subtype-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space M)
+            ( Y)
+
+        eq-set-quotient-sim-element-set-quotient
+          ( equivalence-relation-sim-Pseudometric-Space M)
+          ( X)
+          ( Y)
+          ( x∈X)
+          ( y∈Y)
+          ( λ d → X~Y d (x , x∈X) (y , y∈Y))
+
+    is-extensional-pseudometric-metric-quotient-Pseudometric-Space :
+      is-extensional-Pseudometric-Space
+        ( pseudometric-metric-quotient-Pseudometric-Space M)
+    is-extensional-pseudometric-metric-quotient-Pseudometric-Space =
+      is-extensional-is-tight-Pseudometric-Space
+        ( pseudometric-metric-quotient-Pseudometric-Space M)
+        ( is-tight-pseudometric-metric-quotient-Pseudometric-Space)
+```
+
+### The quotient metric space of a pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  metric-quotient-Pseudometric-Space : Metric-Space (l1 ⊔ l2) (l1 ⊔ l2)
+  metric-quotient-Pseudometric-Space =
+    make-Metric-Space
+      ( type-metric-quotient-Pseudometric-Space M)
+      ( neighborhood-prop-metric-quotient-Pseudometric-Space M)
+      ( is-reflexive-neighborhood-metric-quotient-Pseudometric-Space M)
+      ( is-symmetric-neighborhood-metric-quotient-Pseudometric-Space M)
+      ( is-triangular-neighborhood-metric-quotient-Pseudometric-Space M)
+      ( is-saturated-neighborhood-metric-quotient-Pseudometric-Space M)
+      ( is-extensional-pseudometric-metric-quotient-Pseudometric-Space M)
+```
+
+### Mapping from a pseudometric space to its quotient metric space
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  map-metric-quotient-Pseudometric-Space :
+    type-Pseudometric-Space M → type-metric-quotient-Pseudometric-Space M
+  map-metric-quotient-Pseudometric-Space =
+    quotient-map (equivalence-relation-sim-Pseudometric-Space M)
+
+  map-subtype-metric-quotient-Pseudometric-Space :
+    (x : type-Pseudometric-Space M) →
+    type-subtype-metric-quotient-Pseudometric-Space M
+      ( map-metric-quotient-Pseudometric-Space x)
+  map-subtype-metric-quotient-Pseudometric-Space =
+    inhabitant-equivalence-class-quotient-map-set-quotient
+      ( equivalence-relation-sim-Pseudometric-Space M)
+```
+
+### The mapping from a pseudometric space its quotient metric space is an isometry
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Pseudometric-Space l1 l2)
+  where
+
+  abstract
+    preserves-neighborhood-map-metric-quotient-Pseudometric-Space :
+      (d : ℚ⁺) (x y : type-Pseudometric-Space M) →
+      neighborhood-Pseudometric-Space M d x y →
+      neighborhood-metric-quotient-Pseudometric-Space
+        ( M)
+        ( d)
+        ( map-metric-quotient-Pseudometric-Space M x)
+        ( map-metric-quotient-Pseudometric-Space M y)
+    preserves-neighborhood-map-metric-quotient-Pseudometric-Space
+      d x y d⟨x,y⟩ (x' , x≈x') (y' , y≈y') =
+      let
+        x~x' =
+          sim-is-in-equivalence-class-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space M)
+            ( x)
+            ( x')
+            ( x≈x')
+
+        y~y' =
+          sim-is-in-equivalence-class-set-quotient
+            ( equivalence-relation-sim-Pseudometric-Space M)
+            ( y)
+            ( y')
+            ( y≈y')
+
+      in
+        preserves-neighborhood-sim-Pseudometric-Space' M y~y' d x'
+          ( preserves-neighborhood-sim-Pseudometric-Space M x~x' d y d⟨x,y⟩)
+
+    reflects-neighborhood-map-metric-quotient-Pseudometric-Space :
+      (d : ℚ⁺) (x y : type-Pseudometric-Space M) →
+      neighborhood-metric-quotient-Pseudometric-Space
+        ( M)
+        ( d)
+        ( map-metric-quotient-Pseudometric-Space M x)
+        ( map-metric-quotient-Pseudometric-Space M y) →
+      neighborhood-Pseudometric-Space M d x y
+    reflects-neighborhood-map-metric-quotient-Pseudometric-Space
+      d x y Nxy =
+        Nxy
+          ( map-subtype-metric-quotient-Pseudometric-Space M x)
+          ( map-subtype-metric-quotient-Pseudometric-Space M y)
+
+  is-isometry-map-metric-quotient-Pseudometric-Space :
+    is-isometry-Pseudometric-Space
+      ( M)
+      ( pseudometric-metric-quotient-Pseudometric-Space M)
+      ( map-metric-quotient-Pseudometric-Space M)
+  is-isometry-map-metric-quotient-Pseudometric-Space d x y =
+    ( preserves-neighborhood-map-metric-quotient-Pseudometric-Space d x y ,
+      reflects-neighborhood-map-metric-quotient-Pseudometric-Space d x y)
+```
+
+### The isometry from a pseudometric space to its quotient metric space
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  isometry-map-metric-quotient-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( M)
+      ( pseudometric-metric-quotient-Pseudometric-Space M)
+  isometry-map-metric-quotient-Pseudometric-Space =
+    ( map-metric-quotient-Pseudometric-Space M ,
+      is-isometry-map-metric-quotient-Pseudometric-Space M)
+```
+
+### The short map from a pseudometric space to its quotient metric space
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  short-map-metric-quotient-Pseudometric-Space :
+    short-function-Pseudometric-Space
+      ( M)
+      ( pseudometric-metric-quotient-Pseudometric-Space M)
+  short-map-metric-quotient-Pseudometric-Space =
+    short-isometry-Pseudometric-Space
+      ( M)
+      ( pseudometric-metric-quotient-Pseudometric-Space M)
+      ( isometry-map-metric-quotient-Pseudometric-Space M)
+```
+
+### The isometric equivalence between a metric space and the quotient metric space of its pseudometric
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Metric-Space l1 l2)
+  where
+
+  map-metric-quotient-Metric-Space :
+    type-Metric-Space M →
+    type-metric-quotient-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+  map-metric-quotient-Metric-Space =
+    map-metric-quotient-Pseudometric-Space
+      ( pseudometric-Metric-Space M)
+
+  abstract
+    is-contr-map-metric-quotient-Metric-Space :
+      is-contr-map map-metric-quotient-Metric-Space
+    is-contr-map-metric-quotient-Metric-Space X =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( is-contr-Prop
+              ( fiber map-metric-quotient-Metric-Space X))
+        in do
+          ( x , x∈X) ←
+            is-inhabited-subtype-set-quotient
+              ( equivalence-relation-sim-Metric-Space M)
+              ( X)
+
+          ( ( x ,
+              eq-set-quotient-equivalence-class-set-quotient
+                ( equivalence-relation-sim-Metric-Space M)
+                ( X)
+                ( x∈X)) ,
+            ( λ (y , Y＝X) →
+              eq-type-subtype
+                ( λ z →
+                  Id-Prop
+                    ( set-metric-quotient-Pseudometric-Space
+                      ( pseudometric-Metric-Space M))
+                      ( map-metric-quotient-Metric-Space z)
+                      ( X))
+                ( eq-sim-Metric-Space
+                  ( M)
+                  ( x)
+                  ( y)
+                  ( apply-effectiveness-quotient-map
+                    ( equivalence-relation-sim-Metric-Space M)
+                    ( ( eq-set-quotient-equivalence-class-set-quotient
+                        ( equivalence-relation-sim-Metric-Space M)
+                        ( X)
+                        ( x∈X)) ∙
+                      ( inv Y＝X))))))
+
+    is-equiv-map-metric-quotient-Metric-Space :
+      is-equiv map-metric-quotient-Metric-Space
+    is-equiv-map-metric-quotient-Metric-Space =
+      is-equiv-is-contr-map
+        ( is-contr-map-metric-quotient-Metric-Space)
+
+    is-isometry-map-metric-quotient-Metric-Space :
+      is-isometry-Metric-Space
+        ( M)
+        ( metric-quotient-Pseudometric-Space
+          ( pseudometric-Metric-Space M))
+        ( map-metric-quotient-Metric-Space)
+    is-isometry-map-metric-quotient-Metric-Space =
+      is-isometry-map-metric-quotient-Pseudometric-Space
+        ( pseudometric-Metric-Space M)
+
+  isometric-equiv-metric-quotient-Metric-Space' :
+    isometric-equiv-Metric-Space'
+      ( M)
+      ( metric-quotient-Pseudometric-Space
+        ( pseudometric-Metric-Space M))
+  isometric-equiv-metric-quotient-Metric-Space' =
+    ( map-metric-quotient-Metric-Space ,
+      is-equiv-map-metric-quotient-Metric-Space ,
+      is-isometry-map-metric-quotient-Metric-Space)
+```
+
+### The construction of the quotient metric space of a pseudometric space is idempotent
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  is-idempotent-metric-quotient-Pseudometric-Space :
+    metric-quotient-Pseudometric-Space
+      ( pseudometric-Metric-Space
+        ( metric-quotient-Pseudometric-Space M)) ＝
+    metric-quotient-Pseudometric-Space M
+  is-idempotent-metric-quotient-Pseudometric-Space =
+    inv
+      ( eq-isometric-equiv-Metric-Space'
+        ( metric-quotient-Pseudometric-Space M)
+        ( metric-quotient-Pseudometric-Space
+          ( pseudometric-Metric-Space
+            ( metric-quotient-Pseudometric-Space M)))
+        ( isometric-equiv-metric-quotient-Metric-Space'
+          ( metric-quotient-Pseudometric-Space M)))
+```
+
+### The pointwise quotient of a Cauchy approximation in a pseudometric space is a Cauchy approximation in the quotient metric space
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  where
+
+  map-metric-quotient-cauchy-approximation-Pseudometric-Space :
+    cauchy-approximation-Pseudometric-Space M →
+    cauchy-approximation-Metric-Space
+      ( metric-quotient-Pseudometric-Space M)
+  map-metric-quotient-cauchy-approximation-Pseudometric-Space =
+    map-short-function-cauchy-approximation-Pseudometric-Space
+      ( M)
+      ( pseudometric-metric-quotient-Pseudometric-Space M)
+      ( short-isometry-Pseudometric-Space
+        ( M)
+        ( pseudometric-metric-quotient-Pseudometric-Space M)
+        ( isometry-map-metric-quotient-Pseudometric-Space M))
+```
+
+### The pointwise quotient of Cauchy approximations in the quotient metric space preserves limits
+
+```agda
+module _
+  {l1 l2 : Level} (M : Pseudometric-Space l1 l2)
+  (u : cauchy-approximation-Pseudometric-Space M)
+  (lim : type-Pseudometric-Space M)
+  (is-lim :
+    is-limit-cauchy-approximation-Pseudometric-Space M u lim)
+  where
+
+  preserves-limit-map-metric-quotient-cauchy-approximation-Pseudometric-Space :
+    is-limit-cauchy-approximation-Metric-Space
+      ( metric-quotient-Pseudometric-Space M)
+      ( map-metric-quotient-cauchy-approximation-Pseudometric-Space M u)
+      ( map-metric-quotient-Pseudometric-Space M lim)
+  preserves-limit-map-metric-quotient-cauchy-approximation-Pseudometric-Space
+    ε δ (x , x∈uε) (y , y∈lim) =
+    let
+      lim~y : sim-Pseudometric-Space M lim y
+      lim~y =
+        sim-is-in-equivalence-class-set-quotient
+          ( equivalence-relation-sim-Pseudometric-Space M)
+          ( lim)
+          ( y)
+          ( y∈lim)
+
+      uε~x :
+        sim-Pseudometric-Space M
+          ( map-cauchy-approximation-Pseudometric-Space M u ε)
+          ( x)
+      uε~x =
+        sim-is-in-equivalence-class-set-quotient
+          ( equivalence-relation-sim-Pseudometric-Space M)
+          ( map-cauchy-approximation-Pseudometric-Space M u ε)
+          ( x)
+          ( x∈uε)
+    in
+      preserves-neighborhood-sim-Pseudometric-Space'
+        ( M)
+        ( lim~y)
+        ( ε +ℚ⁺ δ)
+        ( x)
+        ( preserves-neighborhood-sim-Pseudometric-Space
+          ( M)
+          ( uε~x)
+          ( ε +ℚ⁺ δ)
+          ( lim)
+          ( is-lim ε δ))
+
+  convergent-map-metric-quotient-cauchy-approximation-Pseudometric-Space :
+    convergent-cauchy-approximation-Metric-Space
+      ( metric-quotient-Pseudometric-Space M)
+  convergent-map-metric-quotient-cauchy-approximation-Pseudometric-Space =
+    ( map-metric-quotient-cauchy-approximation-Pseudometric-Space M u ,
+      map-metric-quotient-Pseudometric-Space M lim ,
+      preserves-limit-map-metric-quotient-cauchy-approximation-Pseudometric-Space)
+```
+
+### Characterization of functions from the quotient metric space into metric spaces
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2)
+  (B : Metric-Space l1' l2')
+  where
+
+  precomp-map-metric-quotient-Pseudometric-Space :
+    type-function-Metric-Space
+      ( metric-quotient-Pseudometric-Space A)
+      ( B) →
+    reflecting-map-equivalence-relation
+      ( equivalence-relation-sim-Pseudometric-Space A)
+      ( type-Metric-Space B)
+  precomp-map-metric-quotient-Pseudometric-Space =
+    precomp-Set-Quotient
+      ( equivalence-relation-sim-Pseudometric-Space A)
+      ( set-metric-quotient-Pseudometric-Space A)
+      ( reflecting-map-quotient-map
+        ( equivalence-relation-sim-Pseudometric-Space A))
+      ( set-Metric-Space B)
+
+  is-equiv-precomp-map-metric-quotient-Pseudometric-Space :
+    is-equiv precomp-map-metric-quotient-Pseudometric-Space
+  is-equiv-precomp-map-metric-quotient-Pseudometric-Space =
+    is-set-quotient-set-quotient
+      ( equivalence-relation-sim-Pseudometric-Space A)
+      ( set-Metric-Space B)
+
+  equiv-type-function-metric-quotient-Pseudometric-Space :
+    type-function-Metric-Space
+      ( metric-quotient-Pseudometric-Space A)
+      ( B) ≃
+    reflecting-map-equivalence-relation
+      ( equivalence-relation-sim-Pseudometric-Space A)
+      ( type-Metric-Space B)
+  equiv-type-function-metric-quotient-Pseudometric-Space =
+    ( precomp-map-metric-quotient-Pseudometric-Space ,
+      is-equiv-precomp-map-metric-quotient-Pseudometric-Space)
+```
+
+### Induced short function from the quotient metric space into a metric space
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2)
+  (B : Metric-Space l1' l2')
+  (f : short-function-Pseudometric-Space A (pseudometric-Metric-Space B))
+  where
+
+  map-short-function-metric-quotient-Pseudometric-space :
+    type-function-Metric-Space
+      ( metric-quotient-Pseudometric-Space A)
+      ( B)
+  map-short-function-metric-quotient-Pseudometric-space =
+    inv-precomp-set-quotient
+      ( equivalence-relation-sim-Pseudometric-Space A)
+      ( set-Metric-Space B)
+      ( reflecting-map-short-function-metric-space-Pseudometric-Space A B f)
+
+  htpy-map-short-function-metric-quotient-Pseudometric-Space :
+    ( ( map-short-function-metric-quotient-Pseudometric-space) ∘
+      ( map-metric-quotient-Pseudometric-Space A)) ~
+    ( map-short-function-Pseudometric-Space A (pseudometric-Metric-Space B) f)
+  htpy-map-short-function-metric-quotient-Pseudometric-Space =
+    is-section-inv-precomp-set-quotient
+      ( equivalence-relation-sim-Pseudometric-Space A)
+      ( set-Metric-Space B)
+      ( reflecting-map-short-function-metric-space-Pseudometric-Space A B f)
+
+  abstract
+    is-short-map-short-function-metric-quotient-Pseudometric-Space :
+      is-short-function-Metric-Space
+        ( metric-quotient-Pseudometric-Space A)
+        ( B)
+        ( map-short-function-metric-quotient-Pseudometric-space)
+    is-short-map-short-function-metric-quotient-Pseudometric-Space
+      d X Y N⟨X,Y⟩ =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( neighborhood-prop-Metric-Space
+              ( B)
+              ( d)
+              ( map-short-function-metric-quotient-Pseudometric-space X)
+              ( map-short-function-metric-quotient-Pseudometric-space Y))
+        in do
+          ( x , x∈X) ←
+            is-inhabited-subtype-set-quotient
+              ( equivalence-relation-sim-Pseudometric-Space A)
+              ( X)
+          ( y , y∈Y) ←
+            is-inhabited-subtype-set-quotient
+              ( equivalence-relation-sim-Pseudometric-Space A)
+              ( Y)
+          let
+            lemma-eq-X :
+              map-metric-quotient-Pseudometric-Space A x ＝ X
+            lemma-eq-X =
+              eq-set-quotient-equivalence-class-set-quotient
+                ( equivalence-relation-sim-Pseudometric-Space A)
+                ( X)
+                ( x∈X)
+
+            lemma-eq-fX :
+              ( map-short-function-Pseudometric-Space
+                ( A)
+                ( pseudometric-Metric-Space B)
+                ( f)
+                ( x)) ＝
+              ( map-short-function-metric-quotient-Pseudometric-space X)
+            lemma-eq-fX =
+              ( inv
+                ( htpy-map-short-function-metric-quotient-Pseudometric-Space
+                  ( x))) ∙
+              ( ap
+                ( map-short-function-metric-quotient-Pseudometric-space)
+                ( lemma-eq-X))
+
+            lemma-eq-Y :
+              map-metric-quotient-Pseudometric-Space A y ＝ Y
+            lemma-eq-Y =
+              eq-set-quotient-equivalence-class-set-quotient
+                ( equivalence-relation-sim-Pseudometric-Space A)
+                ( Y)
+                ( y∈Y)
+
+            lemma-eq-fY :
+              ( map-short-function-Pseudometric-Space
+                ( A)
+                ( pseudometric-Metric-Space B)
+                ( f)
+                ( y)) ＝
+              ( map-short-function-metric-quotient-Pseudometric-space Y)
+            lemma-eq-fY =
+              ( inv
+                ( htpy-map-short-function-metric-quotient-Pseudometric-Space
+                  ( y))) ∙
+              ( ap
+                ( map-short-function-metric-quotient-Pseudometric-space)
+                ( lemma-eq-Y))
+
+          binary-tr
+            ( neighborhood-Metric-Space B d)
+            ( lemma-eq-fX)
+            ( lemma-eq-fY)
+            ( is-short-map-short-function-Pseudometric-Space
+              ( A)
+              ( pseudometric-Metric-Space B)
+              ( f)
+              ( d)
+              ( x)
+              ( y)
+              ( N⟨X,Y⟩ (x , x∈X) (y , y∈Y)))
+
+  short-function-metric-quotient-Pseudometric-Space :
+    short-function-Metric-Space
+      ( metric-quotient-Pseudometric-Space A)
+      ( B)
+  short-function-metric-quotient-Pseudometric-Space =
+    ( map-short-function-metric-quotient-Pseudometric-space ,
+      is-short-map-short-function-metric-quotient-Pseudometric-Space)
+```
+
+## External links
+
+- [Metric identification](https://en.wikipedia.org/wiki/Pseudometric_space#Metric_identification)
+  on pseudometric spaces at Wikipedia
diff --git a/src/metric-spaces/metric-spaces.lagda.md b/src/metric-spaces/metric-spaces.lagda.md
index 9d9e823937..d857545e04 100644
--- a/src/metric-spaces/metric-spaces.lagda.md
+++ b/src/metric-spaces/metric-spaces.lagda.md
@@ -17,6 +17,7 @@ open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions
+open import foundation.reflecting-maps-equivalence-relations
 open import foundation.sets
 open import foundation.subtypes
 open import foundation.transport-along-identifications
@@ -30,6 +31,7 @@ open import metric-spaces.pseudometric-spaces
 open import metric-spaces.rational-neighborhood-relations
 open import metric-spaces.reflexive-rational-neighborhood-relations
 open import metric-spaces.saturated-rational-neighborhood-relations
+open import metric-spaces.short-functions-pseudometric-spaces
 open import metric-spaces.similarity-of-elements-pseudometric-spaces
 open import metric-spaces.symmetric-rational-neighborhood-relations
 open import metric-spaces.triangular-rational-neighborhood-relations
@@ -328,6 +330,53 @@ module _
     map-inv-equiv (equiv-sim-eq-Metric-Space x y)
 ```
 
+### Short maps from a pseudometric space to a metric space reflect similarity
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2)
+  (B : Metric-Space l1' l2')
+  (f : short-function-Pseudometric-Space A (pseudometric-Metric-Space B))
+  where
+
+  reflects-sim-map-short-function-metric-space-Pseudometric-Space :
+    {x y : type-Pseudometric-Space A} →
+    sim-Pseudometric-Space A x y →
+    map-short-function-Pseudometric-Space A (pseudometric-Metric-Space B) f x ＝
+    map-short-function-Pseudometric-Space A (pseudometric-Metric-Space B) f y
+  reflects-sim-map-short-function-metric-space-Pseudometric-Space {x} {y} x~y =
+    eq-sim-Metric-Space B
+      ( map-short-function-Pseudometric-Space
+        ( A)
+        ( pseudometric-Metric-Space B)
+        ( f)
+        ( x))
+      ( map-short-function-Pseudometric-Space
+        ( A)
+        ( pseudometric-Metric-Space B)
+        ( f)
+        ( y))
+      ( preserves-sim-map-short-function-Pseudometric-Space
+        ( A)
+        ( pseudometric-Metric-Space B)
+        ( f)
+        ( x)
+        ( y)
+        ( x~y))
+
+  reflecting-map-short-function-metric-space-Pseudometric-Space :
+    reflecting-map-equivalence-relation
+      ( equivalence-relation-sim-Pseudometric-Space A)
+      ( type-Metric-Space B)
+  reflecting-map-short-function-metric-space-Pseudometric-Space =
+    ( ( map-short-function-Pseudometric-Space
+        ( A)
+        ( pseudometric-Metric-Space B)
+        ( f)) ,
+      ( reflects-sim-map-short-function-metric-space-Pseudometric-Space))
+```
+
 ## External links
 
 - [`MetricSpaces.Type`](https://www.cs.bham.ac.uk/~mhe/TypeTopology/MetricSpaces.Type.html)
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 c48a4bb7ef..cc4d35de83 100644
--- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md
+++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md
@@ -23,6 +23,7 @@ open import foundation.universe-levels
 
 open import metric-spaces.pseudometric-spaces
 open import metric-spaces.rational-neighborhood-relations
+open import metric-spaces.short-functions-pseudometric-spaces
 ```
 
 </details>
@@ -200,6 +201,17 @@ module _
               ( y)
               ( x≍y δ))))
 
+  preserves-neighborhood-sim-Pseudometric-Space' :
+    { x y : type-Pseudometric-Space A} →
+    ( sim-Pseudometric-Space A x y) →
+    ( d : ℚ⁺) (z : type-Pseudometric-Space A) →
+    neighborhood-Pseudometric-Space A d z x →
+    neighborhood-Pseudometric-Space A d z y
+  preserves-neighborhood-sim-Pseudometric-Space' {x} {y} x≍y d z Nzx =
+    symmetric-neighborhood-Pseudometric-Space A d y z
+      ( preserves-neighborhood-sim-Pseudometric-Space x≍y d z
+        ( symmetric-neighborhood-Pseudometric-Space A d z x Nzx))
+
   iff-same-neighbors-sim-Pseudometric-Space :
     { x y : type-Pseudometric-Space A} →
     ( sim-Pseudometric-Space A x y) ↔
@@ -258,3 +270,23 @@ module _
     ( iff-same-neighbors-same-neighborhood-Pseudometric-Space) ∘iff
     ( iff-same-neighbors-sim-Pseudometric-Space A)
 ```
+
+### Short maps between pseudometric spaces preserves similarity
+
+```agda
+module _
+  { l1 l2 l1' l2' : Level}
+  ( A : Pseudometric-Space l1 l2)
+  ( B : Pseudometric-Space l1' l2')
+  ( f : short-function-Pseudometric-Space A B)
+  where
+
+  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)
+```