diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md
index 81a017ff2d..f7778db529 100644
--- a/src/metric-spaces.lagda.md
+++ b/src/metric-spaces.lagda.md
@@ -48,29 +48,39 @@ module metric-spaces where
 open import metric-spaces.category-of-metric-spaces-and-isometries public
 open import metric-spaces.category-of-metric-spaces-and-short-functions public
 open import metric-spaces.cauchy-approximations-metric-spaces public
+open import metric-spaces.cauchy-approximations-metric-spaces-WIP public
 open import metric-spaces.cauchy-approximations-premetric-spaces public
 open import metric-spaces.cauchy-sequences-complete-metric-spaces public
 open import metric-spaces.cauchy-sequences-metric-spaces public
 open import metric-spaces.closed-premetric-structures public
 open import metric-spaces.complete-metric-spaces public
+open import metric-spaces.complete-metric-spaces-WIP public
 open import metric-spaces.continuous-functions-metric-spaces public
+open import metric-spaces.continuous-functions-metric-spaces-WIP public
 open import metric-spaces.continuous-functions-premetric-spaces public
 open import metric-spaces.convergent-cauchy-approximations-metric-spaces public
+open import metric-spaces.convergent-cauchy-approximations-metric-spaces-WIP public
 open import metric-spaces.convergent-sequences-metric-spaces public
 open import metric-spaces.dependent-products-metric-spaces public
+open import metric-spaces.dependent-products-metric-spaces-WIP public
 open import metric-spaces.discrete-premetric-structures public
 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-metric-spaces-WIP public
 open import metric-spaces.equality-of-premetric-spaces public
 open import metric-spaces.extensional-premetric-structures public
+open import metric-spaces.extensional-pseudometric-spaces-WIP public
 open import metric-spaces.functions-metric-spaces public
 open import metric-spaces.functor-category-set-functions-isometry-metric-spaces public
 open import metric-spaces.functor-category-short-isometry-metric-spaces public
 open import metric-spaces.induced-premetric-structures-on-preimages public
 open import metric-spaces.isometric-equivalences-premetric-spaces public
 open import metric-spaces.isometries-metric-spaces public
+open import metric-spaces.isometries-metric-spaces-WIP public
 open import metric-spaces.isometries-premetric-spaces public
+open import metric-spaces.limits-of-cauchy-approximations-metric-spaces-WIP public
 open import metric-spaces.limits-of-cauchy-approximations-premetric-spaces public
+open import metric-spaces.limits-of-functions-metric-spaces public
 open import metric-spaces.limits-of-sequences-metric-spaces public
 open import metric-spaces.limits-of-sequences-premetric-spaces public
 open import metric-spaces.limits-of-sequences-pseudometric-spaces public
@@ -84,34 +94,49 @@ open import metric-spaces.metric-space-of-functions-metric-spaces public
 open import metric-spaces.metric-space-of-isometries-metric-spaces public
 open import metric-spaces.metric-space-of-lipschitz-functions-metric-spaces public
 open import metric-spaces.metric-space-of-rational-numbers public
+open import metric-spaces.metric-space-of-rational-numbers-WIP public
 open import metric-spaces.metric-space-of-rational-numbers-with-open-neighborhoods public
 open import metric-spaces.metric-space-of-short-functions-metric-spaces public
 open import metric-spaces.metric-spaces public
+open import metric-spaces.metric-spaces-WIP public
 open import metric-spaces.metric-structures public
 open import metric-spaces.monotonic-premetric-structures public
+open import metric-spaces.monotonic-rational-neighborhoods public
 open import metric-spaces.ordering-premetric-structures public
+open import metric-spaces.ordering-rational-neighborhoods public
 open import metric-spaces.precategory-of-metric-spaces-and-functions public
 open import metric-spaces.precategory-of-metric-spaces-and-isometries public
 open import metric-spaces.precategory-of-metric-spaces-and-short-functions public
+open import metric-spaces.preimage-rational-neighborhoods public
 open import metric-spaces.premetric-spaces public
 open import metric-spaces.premetric-structures public
 open import metric-spaces.pseudometric-spaces public
+open import metric-spaces.pseudometric-spaces-WIP public
 open import metric-spaces.pseudometric-structures public
 open import metric-spaces.rational-approximations-of-zero public
 open import metric-spaces.rational-cauchy-approximations public
+open import metric-spaces.rational-neighborhoods public
 open import metric-spaces.rational-sequences-approximating-zero public
 open import metric-spaces.reflexive-premetric-structures public
+open import metric-spaces.reflexive-rational-neighborhoods public
 open import metric-spaces.saturated-complete-metric-spaces public
 open import metric-spaces.saturated-metric-spaces public
+open import metric-spaces.saturated-rational-neighborhoods public
 open import metric-spaces.sequences-metric-spaces public
 open import metric-spaces.sequences-premetric-spaces public
 open import metric-spaces.sequences-pseudometric-spaces public
 open import metric-spaces.short-functions-metric-spaces public
+open import metric-spaces.short-functions-metric-spaces-WIP public
 open import metric-spaces.short-functions-premetric-spaces public
+open import metric-spaces.similarity-of-elements-pseudometric-spaces public
 open import metric-spaces.subspaces-metric-spaces public
+open import metric-spaces.subspaces-metric-spaces-WIP public
 open import metric-spaces.symmetric-premetric-structures public
+open import metric-spaces.symmetric-rational-neighborhoods public
 open import metric-spaces.triangular-premetric-structures public
+open import metric-spaces.triangular-rational-neighborhoods public
 open import metric-spaces.uniformly-continuous-functions-metric-spaces public
+open import metric-spaces.uniformly-continuous-functions-metric-spaces-WIP public
 open import metric-spaces.uniformly-continuous-functions-premetric-spaces public
 ```
 
diff --git a/src/metric-spaces/cauchy-approximations-metric-spaces-WIP.lagda.md b/src/metric-spaces/cauchy-approximations-metric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..0b763c2aef
--- /dev/null
+++ b/src/metric-spaces/cauchy-approximations-metric-spaces-WIP.lagda.md
@@ -0,0 +1,161 @@
+# Cauchy approximations in metric spaces (WIP)
+
+```agda
+module metric-spaces.cauchy-approximations-metric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.constant-maps
+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.universe-levels
+
+open import metric-spaces.metric-spaces-WIP
+open import metric-spaces.short-functions-metric-spaces-WIP
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "Cauchy approximation" Disambiguation="in a metric space" Agda=is-cauchy-approximation-Metric-Space-WIP}}
+in a [metric space](metric-spaces.metric-spaces.md) `A` is a map `f` from
+[`ℚ⁺`](elementary-number-theory.positive-rational-numbers.md) to its carrier
+type such that for all `(ε δ : ℚ⁺)`, `f ε` and `f δ` are in a
+(`ε + δ`)-[neighborhood](metric-spaces.premetric-structures.md), i.e. the
+distance between `f ε` and `f δ` is bounded by `ε + δ`.
+
+## Definitions
+
+### Cauchy approximations in metric spaces
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  where
+
+  is-cauchy-approximation-prop-Metric-Space-WIP :
+    (ℚ⁺ → type-Metric-Space-WIP A) → Prop l2
+  is-cauchy-approximation-prop-Metric-Space-WIP f =
+    Π-Prop
+      ( ℚ⁺)
+      ( λ ε →
+        Π-Prop
+          ( ℚ⁺)
+          ( λ δ →
+            neighborhood-prop-Metric-Space-WIP A (ε +ℚ⁺ δ) (f ε) (f δ)))
+
+  is-cauchy-approximation-Metric-Space-WIP :
+    (ℚ⁺ → type-Metric-Space-WIP A) → UU l2
+  is-cauchy-approximation-Metric-Space-WIP =
+    type-Prop ∘ is-cauchy-approximation-prop-Metric-Space-WIP
+
+  cauchy-approximation-Metric-Space-WIP : UU (l1 ⊔ l2)
+  cauchy-approximation-Metric-Space-WIP =
+    type-subtype is-cauchy-approximation-prop-Metric-Space-WIP
+```
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  (f : cauchy-approximation-Metric-Space-WIP A)
+  where
+
+  map-cauchy-approximation-Metric-Space-WIP :
+    ℚ⁺ → type-Metric-Space-WIP A
+  map-cauchy-approximation-Metric-Space-WIP = pr1 f
+
+  is-cauchy-approximation-map-cauchy-approximation-Metric-Space-WIP :
+    (ε δ : ℚ⁺) →
+    neighborhood-Metric-Space-WIP
+      ( A)
+      ( ε +ℚ⁺ δ)
+      ( map-cauchy-approximation-Metric-Space-WIP ε)
+      ( map-cauchy-approximation-Metric-Space-WIP δ)
+  is-cauchy-approximation-map-cauchy-approximation-Metric-Space-WIP = pr2 f
+```
+
+## Properties
+
+### Constant maps in metric spaces are Cauchy approximations
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  (x : type-Metric-Space-WIP A)
+  where
+
+  const-cauchy-approximation-Metric-Space-WIP :
+    cauchy-approximation-Metric-Space-WIP A
+  const-cauchy-approximation-Metric-Space-WIP =
+    (const ℚ⁺ x) , (λ ε δ → refl-neighborhood-Metric-Space-WIP A (ε +ℚ⁺ δ) x)
+```
+
+### Short maps between metric spaces are functorial on Cauchy approximations
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  (f : short-function-Metric-Space-WIP A B)
+  where
+
+  map-short-function-cauchy-approximation-Metric-Space-WIP :
+    cauchy-approximation-Metric-Space-WIP A →
+    cauchy-approximation-Metric-Space-WIP B
+  map-short-function-cauchy-approximation-Metric-Space-WIP (u , H) =
+    ( map-short-function-Metric-Space-WIP A B f ∘ u) ,
+    ( λ ε δ →
+      is-short-map-short-function-Metric-Space-WIP
+      ( A)
+      ( B)
+      ( f)
+      ( ε +ℚ⁺ δ)
+      ( u ε)
+      ( u δ)
+      ( H ε δ))
+
+module _
+  {l1 l2 : Level}
+  (A : Metric-Space-WIP l1 l2)
+  where
+
+  eq-id-map-short-function-cauchy-approximation-Metric-Space-WIP :
+    map-short-function-cauchy-approximation-Metric-Space-WIP
+      ( A)
+      ( A)
+      ( short-id-Metric-Space-WIP A) ＝
+    id
+  eq-id-map-short-function-cauchy-approximation-Metric-Space-WIP = refl
+
+module _
+  {l1a l2a l1b l2b l1c l2c : Level}
+  (A : Metric-Space-WIP l1a l2a)
+  (B : Metric-Space-WIP l1b l2b)
+  (C : Metric-Space-WIP l1c l2c)
+  (g : short-function-Metric-Space-WIP B C)
+  (f : short-function-Metric-Space-WIP A B)
+  where
+
+  eq-comp-map-short-function-cauchy-approximation-Metric-Space-WIP :
+    ( map-short-function-cauchy-approximation-Metric-Space-WIP B C g ∘
+      map-short-function-cauchy-approximation-Metric-Space-WIP A B f) ＝
+    ( map-short-function-cauchy-approximation-Metric-Space-WIP A C
+      (comp-short-function-Metric-Space-WIP A B C g f))
+  eq-comp-map-short-function-cauchy-approximation-Metric-Space-WIP = refl
+```
+
+## References
+
+Our definition of Cauchy approximation follows Definition 4.5.5 of
+{{#cite Booij20PhD}} and Definition 11.2.10 of {{#cite UF13}}.
+
+{{#bibliography}}
diff --git a/src/metric-spaces/complete-metric-spaces-WIP.lagda.md b/src/metric-spaces/complete-metric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..8084e84bc6
--- /dev/null
+++ b/src/metric-spaces/complete-metric-spaces-WIP.lagda.md
@@ -0,0 +1,172 @@
+# Complete metric spaces (WIP)
+
+```agda
+module metric-spaces.complete-metric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.retractions
+open import foundation.sections
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import metric-spaces.cauchy-approximations-metric-spaces-WIP
+open import metric-spaces.convergent-cauchy-approximations-metric-spaces-WIP
+open import metric-spaces.limits-of-cauchy-approximations-metric-spaces-WIP
+open import metric-spaces.metric-spaces-WIP
+```
+
+</details>
+
+## Idea
+
+A [metric space](metric-spaces.metric-spaces-WIP.md) is
+{{#concept "complete" Disambiguation="metric space" Agda=is-complete-Metric-Space-WIP WD="complete metric space" WDID=Q848569}}
+if all its
+[Cauchy approximations](metric-spaces.cauchy-approximations-metric-spaces-WIP.md)
+are
+[convergent](metric-spaces.convergent-cauchy-approximations-metric-spaces-WIP.md).
+
+## Definitions
+
+### The property of being a complete metric space
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  where
+
+  is-complete-prop-Metric-Space-WIP : Prop (l1 ⊔ l2)
+  is-complete-prop-Metric-Space-WIP =
+    Π-Prop
+      ( cauchy-approximation-Metric-Space-WIP A)
+      ( is-convergent-prop-cauchy-approximation-Metric-Space-WIP A)
+
+  is-complete-Metric-Space-WIP : UU (l1 ⊔ l2)
+  is-complete-Metric-Space-WIP = type-Prop is-complete-prop-Metric-Space-WIP
+
+  is-prop-is-complete-Metric-Space-WIP : is-prop is-complete-Metric-Space-WIP
+  is-prop-is-complete-Metric-Space-WIP =
+    is-prop-type-Prop is-complete-prop-Metric-Space-WIP
+```
+
+### The type of complete metric spaces
+
+```agda
+module _
+  (l1 l2 : Level)
+  where
+
+  Complete-Metric-Space-WIP : UU (lsuc l1 ⊔ lsuc l2)
+  Complete-Metric-Space-WIP =
+    type-subtype (is-complete-prop-Metric-Space-WIP {l1} {l2})
+```
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A : Complete-Metric-Space-WIP l1 l2)
+  where
+
+  metric-space-Complete-Metric-Space-WIP : Metric-Space-WIP l1 l2
+  metric-space-Complete-Metric-Space-WIP = pr1 A
+
+  type-Complete-Metric-Space-WIP : UU l1
+  type-Complete-Metric-Space-WIP =
+    type-Metric-Space-WIP metric-space-Complete-Metric-Space-WIP
+
+  is-complete-metric-space-Complete-Metric-Space-WIP :
+    is-complete-Metric-Space-WIP metric-space-Complete-Metric-Space-WIP
+  is-complete-metric-space-Complete-Metric-Space-WIP = pr2 A
+```
+
+### The equivalence between Cauchy approximations and convergent Cauchy approximations in a complete metric space
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A : Complete-Metric-Space-WIP l1 l2)
+  where
+
+  convergent-cauchy-approximation-Complete-Metric-Space-WIP :
+    cauchy-approximation-Metric-Space-WIP
+      ( metric-space-Complete-Metric-Space-WIP A) →
+    convergent-cauchy-approximation-Metric-Space-WIP
+      ( metric-space-Complete-Metric-Space-WIP A)
+  convergent-cauchy-approximation-Complete-Metric-Space-WIP u =
+    ( u , is-complete-metric-space-Complete-Metric-Space-WIP A u)
+
+  is-section-convergent-cauchy-approximation-Complete-Metric-Space-WIP :
+    is-section
+      ( convergent-cauchy-approximation-Complete-Metric-Space-WIP)
+      ( inclusion-subtype
+        ( is-convergent-prop-cauchy-approximation-Metric-Space-WIP
+          ( metric-space-Complete-Metric-Space-WIP A)))
+  is-section-convergent-cauchy-approximation-Complete-Metric-Space-WIP u =
+    eq-type-subtype
+      ( is-convergent-prop-cauchy-approximation-Metric-Space-WIP
+        ( metric-space-Complete-Metric-Space-WIP A))
+      ( refl)
+
+  is-retraction-convergent-cauchy-approximation-Metric-Space-WIP :
+    is-retraction
+      ( convergent-cauchy-approximation-Complete-Metric-Space-WIP)
+      ( inclusion-subtype
+        ( is-convergent-prop-cauchy-approximation-Metric-Space-WIP
+          ( metric-space-Complete-Metric-Space-WIP A)))
+  is-retraction-convergent-cauchy-approximation-Metric-Space-WIP u = refl
+
+  is-equiv-convergent-cauchy-approximation-Complete-Metric-Space-WIP :
+    is-equiv convergent-cauchy-approximation-Complete-Metric-Space-WIP
+  pr1 is-equiv-convergent-cauchy-approximation-Complete-Metric-Space-WIP =
+    ( inclusion-subtype
+      ( is-convergent-prop-cauchy-approximation-Metric-Space-WIP
+        ( metric-space-Complete-Metric-Space-WIP A))) ,
+    ( is-section-convergent-cauchy-approximation-Complete-Metric-Space-WIP)
+  pr2 is-equiv-convergent-cauchy-approximation-Complete-Metric-Space-WIP =
+    ( inclusion-subtype
+      ( is-convergent-prop-cauchy-approximation-Metric-Space-WIP
+        ( metric-space-Complete-Metric-Space-WIP A))) ,
+    ( is-retraction-convergent-cauchy-approximation-Metric-Space-WIP)
+```
+
+### The limit of a Cauchy approximation in a complete metric space
+
+```agda
+module _
+  { l1 l2 : Level}
+  ( A : Complete-Metric-Space-WIP l1 l2)
+  ( u : cauchy-approximation-Metric-Space-WIP
+    ( metric-space-Complete-Metric-Space-WIP A))
+  where
+
+  limit-cauchy-approximation-Complete-Metric-Space-WIP :
+    type-Complete-Metric-Space-WIP A
+  limit-cauchy-approximation-Complete-Metric-Space-WIP =
+    limit-convergent-cauchy-approximation-Metric-Space-WIP
+      ( metric-space-Complete-Metric-Space-WIP A)
+      ( convergent-cauchy-approximation-Complete-Metric-Space-WIP A u)
+
+  is-limit-limit-cauchy-approximation-Complete-Metric-Space-WIP :
+    is-limit-cauchy-approximation-Metric-Space-WIP
+      ( metric-space-Complete-Metric-Space-WIP A)
+      ( u)
+      ( limit-cauchy-approximation-Complete-Metric-Space-WIP)
+  is-limit-limit-cauchy-approximation-Complete-Metric-Space-WIP =
+    is-limit-limit-convergent-cauchy-approximation-Metric-Space-WIP
+      ( metric-space-Complete-Metric-Space-WIP A)
+      ( convergent-cauchy-approximation-Complete-Metric-Space-WIP A u)
+```
+
+## External links
+
+- [Complete metric space](https://en.wikipedia.org/wiki/Complete_metric_space)
+  at Wikipedia
diff --git a/src/metric-spaces/continuous-functions-metric-spaces-WIP.lagda.md b/src/metric-spaces/continuous-functions-metric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..7fe2777b1c
--- /dev/null
+++ b/src/metric-spaces/continuous-functions-metric-spaces-WIP.lagda.md
@@ -0,0 +1,70 @@
+# Continuous functions between metric spaces (WIP)
+
+```agda
+module metric-spaces.continuous-functions-metric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.inhabited-subtypes
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import metric-spaces.limits-of-functions-metric-spaces
+open import metric-spaces.metric-spaces-WIP
+```
+
+</details>
+
+## Idea
+
+A [function](metric-spaces.functions-metric-spaces.md) `f` between
+[metric spaces](metric-spaces.metric-spaces.md) `X` and `Y` is
+{{#concept "continuous" Disambiguation="function between metric spaces at a point" WDID=Q170058 WD="continuous function" Agda=is-continuous-at-point-function-Metric-Space-WIP}}
+at a point `x` if `f x` is the
+[limit](metric-spaces.limits-of-functions-metric-spaces.md) of `f` at `x`. I.e.,
+there exists a function `m : ℚ⁺ → ℚ⁺` such that whenever `x'` is in an
+`m ε`-neighborhood of `x`, `f x'` is in an `ε`-neighborhood of `f x`. `m` is
+called a modulus of continuity of `f` at `x`.
+
+## Definitions
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (X : Metric-Space-WIP l1 l2)
+  (Y : Metric-Space-WIP l3 l4)
+  (f : type-function-Metric-Space-WIP X Y)
+  (x : type-Metric-Space-WIP X)
+  where
+
+  is-continuous-at-point-prop-function-Metric-Space-WIP : Prop (l1 ⊔ l2 ⊔ l4)
+  is-continuous-at-point-prop-function-Metric-Space-WIP =
+    is-pt-limit-prop-function-Metric-Space-WIP X Y f x (f x)
+
+  is-continuous-at-point-function-Metric-Space-WIP : UU (l1 ⊔ l2 ⊔ l4)
+  is-continuous-at-point-function-Metric-Space-WIP =
+    is-pt-limit-function-Metric-Space-WIP X Y f x (f x)
+
+  is-modulus-of-continuity-at-point-prop-function-Metric-Space-WIP :
+    (ℚ⁺ → ℚ⁺) → Prop (l1 ⊔ l2 ⊔ l4)
+  is-modulus-of-continuity-at-point-prop-function-Metric-Space-WIP =
+    is-modulus-of-pt-limit-prop-function-Metric-Space-WIP X Y f x (f x)
+
+  is-modulus-of-continuity-at-point-function-Metric-Space-WIP :
+    (ℚ⁺ → ℚ⁺) → UU (l1 ⊔ l2 ⊔ l4)
+  is-modulus-of-continuity-at-point-function-Metric-Space-WIP =
+    is-modulus-of-pt-limit-function-Metric-Space-WIP X Y f x (f x)
+
+  modulus-of-continuity-at-point-function-Metric-Space-WIP : UU (l1 ⊔ l2 ⊔ l4)
+  modulus-of-continuity-at-point-function-Metric-Space-WIP =
+    type-subtype
+      is-modulus-of-continuity-at-point-prop-function-Metric-Space-WIP
+```
diff --git a/src/metric-spaces/convergent-cauchy-approximations-metric-spaces-WIP.lagda.md b/src/metric-spaces/convergent-cauchy-approximations-metric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..a08f84aa68
--- /dev/null
+++ b/src/metric-spaces/convergent-cauchy-approximations-metric-spaces-WIP.lagda.md
@@ -0,0 +1,142 @@
+# Convergent Cauchy approximations in metric spaces (WIP)
+
+```agda
+module metric-spaces.convergent-cauchy-approximations-metric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import metric-spaces.cauchy-approximations-metric-spaces-WIP
+open import metric-spaces.limits-of-cauchy-approximations-metric-spaces-WIP
+open import metric-spaces.metric-spaces-WIP
+```
+
+</details>
+
+## Idea
+
+A [Cauchy approximation](metric-spaces.cauchy-approximations-metric-spaces.md)
+in a [metric space](metric-spaces.metric-spaces.md) is
+{{#concept "convergent" Disambiguation="Cauchy approximation in a metric space" agda=is-convergent-cauchy-approximation-Metric-Space-WIP}}
+if it has a
+[limit](metric-spaces.limits-of-cauchy-approximations-metric-spaces-WIP.md).
+Because limits of Cauchy approximations in metric spaces are unique, this is a
+[subtype](foundation.subtypes.md) of the type of Cauchy approximations.
+
+## Definitions
+
+### The property of being a convergent Cauchy approximation in a metric space
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  (f : cauchy-approximation-Metric-Space-WIP A)
+  where
+
+  is-convergent-cauchy-approximation-Metric-Space-WIP : UU (l1 ⊔ l2)
+  is-convergent-cauchy-approximation-Metric-Space-WIP =
+    Σ ( type-Metric-Space-WIP A)
+      ( is-limit-cauchy-approximation-Metric-Space-WIP A f)
+
+  limit-is-convergent-cauchy-approximation-Metric-Space-WIP :
+    is-convergent-cauchy-approximation-Metric-Space-WIP →
+    type-Metric-Space-WIP A
+  limit-is-convergent-cauchy-approximation-Metric-Space-WIP = pr1
+
+  is-limit-limit-is-convergent-cauchy-approximation-Metric-Space-WIP :
+    (x : is-convergent-cauchy-approximation-Metric-Space-WIP) →
+    is-limit-cauchy-approximation-Metric-Space-WIP
+      ( A)
+      ( f)
+      ( limit-is-convergent-cauchy-approximation-Metric-Space-WIP x)
+  is-limit-limit-is-convergent-cauchy-approximation-Metric-Space-WIP = pr2
+
+  abstract
+    is-prop-is-convergent-cauchy-approximation-Metric-Space-WIP :
+      is-prop is-convergent-cauchy-approximation-Metric-Space-WIP
+    is-prop-is-convergent-cauchy-approximation-Metric-Space-WIP =
+      is-prop-all-elements-equal
+        ( λ x y →
+          eq-type-subtype
+            ( is-limit-cauchy-approximation-prop-Metric-Space-WIP A f)
+            ( all-eq-is-limit-cauchy-approximation-Metric-Space-WIP
+              ( A)
+              ( f)
+              ( limit-is-convergent-cauchy-approximation-Metric-Space-WIP x)
+              ( limit-is-convergent-cauchy-approximation-Metric-Space-WIP y)
+              ( is-limit-limit-is-convergent-cauchy-approximation-Metric-Space-WIP
+                x)
+              ( is-limit-limit-is-convergent-cauchy-approximation-Metric-Space-WIP
+                y)))
+
+  is-convergent-prop-cauchy-approximation-Metric-Space-WIP : Prop (l1 ⊔ l2)
+  is-convergent-prop-cauchy-approximation-Metric-Space-WIP =
+    is-convergent-cauchy-approximation-Metric-Space-WIP ,
+    is-prop-is-convergent-cauchy-approximation-Metric-Space-WIP
+```
+
+### The type of convergent Cauchy approximations in a metric space
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  where
+
+  convergent-cauchy-approximation-Metric-Space-WIP : UU (l1 ⊔ l2)
+  convergent-cauchy-approximation-Metric-Space-WIP =
+    type-subtype (is-convergent-prop-cauchy-approximation-Metric-Space-WIP A)
+```
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  (f : convergent-cauchy-approximation-Metric-Space-WIP A)
+  where
+
+  approximation-convergent-cauchy-approximation-Metric-Space-WIP :
+    cauchy-approximation-Metric-Space-WIP A
+  approximation-convergent-cauchy-approximation-Metric-Space-WIP = pr1 f
+
+  map-convergent-cauchy-approximation-Metric-Space-WIP :
+    ℚ⁺ → type-Metric-Space-WIP A
+  map-convergent-cauchy-approximation-Metric-Space-WIP =
+    map-cauchy-approximation-Metric-Space-WIP
+      A
+      approximation-convergent-cauchy-approximation-Metric-Space-WIP
+
+  is-cauchy-approximation-map-convergent-cauchy-approximation-Metric-Space-WIP :
+    (ε δ : ℚ⁺) →
+    neighborhood-Metric-Space-WIP
+      ( A)
+      ( ε +ℚ⁺ δ)
+      ( map-convergent-cauchy-approximation-Metric-Space-WIP ε)
+      ( map-convergent-cauchy-approximation-Metric-Space-WIP δ)
+  is-cauchy-approximation-map-convergent-cauchy-approximation-Metric-Space-WIP =
+    is-cauchy-approximation-map-cauchy-approximation-Metric-Space-WIP
+      A
+      approximation-convergent-cauchy-approximation-Metric-Space-WIP
+
+  limit-convergent-cauchy-approximation-Metric-Space-WIP :
+    type-Metric-Space-WIP A
+  limit-convergent-cauchy-approximation-Metric-Space-WIP = pr1 (pr2 f)
+
+  is-limit-limit-convergent-cauchy-approximation-Metric-Space-WIP :
+    (ε δ : ℚ⁺) →
+    neighborhood-Metric-Space-WIP
+      ( A)
+      ( ε +ℚ⁺ δ)
+      ( map-convergent-cauchy-approximation-Metric-Space-WIP ε)
+      ( limit-convergent-cauchy-approximation-Metric-Space-WIP)
+  is-limit-limit-convergent-cauchy-approximation-Metric-Space-WIP = pr2 (pr2 f)
+```
diff --git a/src/metric-spaces/dependent-products-metric-spaces-WIP.lagda.md b/src/metric-spaces/dependent-products-metric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..a4496a0e54
--- /dev/null
+++ b/src/metric-spaces/dependent-products-metric-spaces-WIP.lagda.md
@@ -0,0 +1,268 @@
+# Dependent products of metric spaces (WIP)
+
+```agda
+module metric-spaces.dependent-products-metric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.evaluation-functions
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.universe-levels
+
+open import metric-spaces.cauchy-approximations-metric-spaces-WIP
+open import metric-spaces.complete-metric-spaces-WIP
+open import metric-spaces.convergent-cauchy-approximations-metric-spaces-WIP
+open import metric-spaces.extensional-pseudometric-spaces-WIP
+open import metric-spaces.limits-of-cauchy-approximations-metric-spaces-WIP
+open import metric-spaces.metric-spaces-WIP
+open import metric-spaces.monotonic-rational-neighborhoods
+open import metric-spaces.pseudometric-spaces-WIP
+open import metric-spaces.rational-neighborhoods
+open import metric-spaces.reflexive-rational-neighborhoods
+open import metric-spaces.saturated-rational-neighborhoods
+open import metric-spaces.short-functions-metric-spaces-WIP
+open import metric-spaces.symmetric-rational-neighborhoods
+open import metric-spaces.triangular-rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+A family of [metric spaces](metric-spaces.metric-spaces.md) over a type produces
+a {{#concept "product metric space" Agda=Π-Metric-Space-WIP}} on the type of
+dependent functions into the carrier types of the family. Two functions `f` and
+`g` are in a [`d`-neighborhood](metric-spaces.premetric-structures.md) in the
+product structure if this holds for all the evaluations `f x` and `g x`. I.e
+this is the premetric such that
+[upper bounds](metric-spaces.premetric-structures.md) on the distance between
+`f` and `g` are bounded below by the supremum of the distances between each
+`f x` and `g x`. The evaluation functions from the product metric space to each
+projected metric space are
+[short maps](metric-spaces.short-functions-metric-spaces.md).
+
+## Definitions
+
+### Product of metric spaces
+
+```agda
+module _
+  {l l1 l2 : Level} (A : UU l) (P : A → Metric-Space-WIP l1 l2)
+  where
+
+  type-Π-Metric-Space-WIP : UU (l ⊔ l1)
+  type-Π-Metric-Space-WIP = (x : A) → type-Metric-Space-WIP (P x)
+
+  neighborhood-prop-Π-Metric-Space-WIP :
+    Rational-Neighborhood-Relation (l ⊔ l2) type-Π-Metric-Space-WIP
+  neighborhood-prop-Π-Metric-Space-WIP d f g =
+    Π-Prop A (λ x → neighborhood-prop-Metric-Space-WIP (P x) d (f x) (g x))
+
+  is-reflexive-neighborhood-Π-Metric-Space-WIP :
+    is-reflexive-Rational-Neighborhood-Relation
+      neighborhood-prop-Π-Metric-Space-WIP
+  is-reflexive-neighborhood-Π-Metric-Space-WIP d f a =
+    refl-neighborhood-Metric-Space-WIP (P a) d (f a)
+
+  is-symmetric-neighborhood-Π-Metric-Space-WIP :
+    is-symmetric-Rational-Neighborhood-Relation
+      neighborhood-prop-Π-Metric-Space-WIP
+  is-symmetric-neighborhood-Π-Metric-Space-WIP d f g H a =
+    symmetric-neighborhood-Metric-Space-WIP (P a) d (f a) (g a) (H a)
+
+  is-triangular-neighborhood-Π-Metric-Space-WIP :
+    is-triangular-Rational-Neighborhood-Relation
+      neighborhood-prop-Π-Metric-Space-WIP
+  is-triangular-neighborhood-Π-Metric-Space-WIP f g h d₁ d₂ H K a =
+    triangular-neighborhood-Metric-Space-WIP
+      ( P a)
+      ( f a)
+      ( g a)
+      ( h a)
+      ( d₁)
+      ( d₂)
+      ( H a)
+      ( K a)
+
+  is-saturated-neighborhood-Π-Metric-Space-WIP :
+    is-saturated-Rational-Neighborhood-Relation
+      neighborhood-prop-Π-Metric-Space-WIP
+  is-saturated-neighborhood-Π-Metric-Space-WIP ε x y H a =
+    saturated-neighborhood-Metric-Space-WIP
+      ( P a)
+      ( ε)
+      ( x a)
+      ( y a)
+      ( λ d → H d a)
+
+  pseudometric-space-Π-Metric-Space : Pseudometric-Space-WIP (l ⊔ l1) (l ⊔ l2)
+  pseudometric-space-Π-Metric-Space =
+    ( type-Π-Metric-Space-WIP) ,
+    ( neighborhood-prop-Π-Metric-Space-WIP ,
+      is-reflexive-neighborhood-Π-Metric-Space-WIP ,
+      is-symmetric-neighborhood-Π-Metric-Space-WIP ,
+      is-triangular-neighborhood-Π-Metric-Space-WIP ,
+      is-saturated-neighborhood-Π-Metric-Space-WIP)
+
+  is-extensional-pseudometric-space-Π-Metric-Space :
+    is-extensional-Pseudometric-Space-WIP
+      pseudometric-space-Π-Metric-Space
+  is-extensional-pseudometric-space-Π-Metric-Space =
+    is-extensional-is-tight-Pseudometric-Space
+      ( pseudometric-space-Π-Metric-Space)
+      ( λ f g H →
+        eq-htpy
+          ( λ a →
+            eq-sim-Metric-Space-WIP
+              ( P a)
+              ( f a)
+              ( g a)
+              ( λ d → H d a)))
+
+  Π-Metric-Space-WIP : Metric-Space-WIP (l ⊔ l1) (l ⊔ l2)
+  Π-Metric-Space-WIP =
+    make-Metric-Space-WIP
+      type-Π-Metric-Space-WIP
+      neighborhood-prop-Π-Metric-Space-WIP
+      is-reflexive-neighborhood-Π-Metric-Space-WIP
+      is-symmetric-neighborhood-Π-Metric-Space-WIP
+      is-triangular-neighborhood-Π-Metric-Space-WIP
+      is-saturated-neighborhood-Π-Metric-Space-WIP
+      is-extensional-pseudometric-space-Π-Metric-Space
+```
+
+## Properties
+
+### The evaluation maps on a product metric space are short
+
+```agda
+module _
+  {l l1 l2 : Level} (A : UU l) (P : A → Metric-Space-WIP l1 l2) (a : A)
+  where
+
+  is-short-ev-Π-Metric-Space-WIP :
+    is-short-function-Metric-Space-WIP
+      ( Π-Metric-Space-WIP A P)
+      ( P a)
+      ( ev a)
+  is-short-ev-Π-Metric-Space-WIP ε x y H = H a
+
+  short-ev-Π-Metric-Space-WIP :
+    short-function-Metric-Space-WIP
+      ( Π-Metric-Space-WIP A P)
+      ( P a)
+  short-ev-Π-Metric-Space-WIP = (ev a) , (is-short-ev-Π-Metric-Space-WIP)
+```
+
+### The partial applications of a Cauchy approximation in a dependent product metric space are Cauchy approximations
+
+```agda
+module _
+  {l l1 l2 : Level} (A : UU l) (P : A → Metric-Space-WIP l1 l2)
+  (f : cauchy-approximation-Metric-Space-WIP (Π-Metric-Space-WIP A P))
+  where
+
+  ev-cauchy-approximation-Π-Metric-Space-WIP :
+    (x : A) → cauchy-approximation-Metric-Space-WIP (P x)
+  ev-cauchy-approximation-Π-Metric-Space-WIP x =
+    map-short-function-cauchy-approximation-Metric-Space-WIP
+      ( Π-Metric-Space-WIP A P)
+      ( P x)
+      ( short-ev-Π-Metric-Space-WIP A P x)
+      ( f)
+```
+
+### A dependent map is the limit of a Cauchy approximation in a dependent product of metric spaces if and only if it is the pointwise limit of its partial applications
+
+```agda
+module _
+  {l l1 l2 : Level} (A : UU l) (P : A → Metric-Space-WIP l1 l2)
+  (f : cauchy-approximation-Metric-Space-WIP (Π-Metric-Space-WIP A P))
+  (g : type-Π-Metric-Space-WIP A P)
+  where
+
+  is-pointwise-limit-is-limit-cauchy-approximation-Π-Metric-Space-WIP :
+    is-limit-cauchy-approximation-Metric-Space-WIP
+      ( Π-Metric-Space-WIP A P)
+      ( f)
+      ( g) →
+    (x : A) →
+    is-limit-cauchy-approximation-Metric-Space-WIP
+      ( P x)
+      ( ev-cauchy-approximation-Π-Metric-Space-WIP A P f x)
+      ( g x)
+  is-pointwise-limit-is-limit-cauchy-approximation-Π-Metric-Space-WIP L x ε δ =
+    L ε δ x
+
+  is-limit-is-pointwise-limit-cauchy-approximation-Π-Metric-Space-WIP :
+    ( (x : A) →
+      is-limit-cauchy-approximation-Metric-Space-WIP
+        ( P x)
+        ( ev-cauchy-approximation-Π-Metric-Space-WIP A P f x)
+        ( g x)) →
+    is-limit-cauchy-approximation-Metric-Space-WIP
+      ( Π-Metric-Space-WIP A P)
+      ( f)
+      ( g)
+  is-limit-is-pointwise-limit-cauchy-approximation-Π-Metric-Space-WIP L ε δ x =
+    L x ε δ
+```
+
+### A product of complete metric spaces is complete
+
+```agda
+module _
+  {l l1 l2 : Level} (A : UU l) (P : A → Metric-Space-WIP l1 l2)
+  (Π-complete : (x : A) → is-complete-Metric-Space-WIP (P x))
+  where
+
+  limit-cauchy-approximation-Π-is-complete-Metric-Space-WIP :
+    cauchy-approximation-Metric-Space-WIP (Π-Metric-Space-WIP A P) →
+    type-Π-Metric-Space-WIP A P
+  limit-cauchy-approximation-Π-is-complete-Metric-Space-WIP u x =
+    limit-cauchy-approximation-Complete-Metric-Space-WIP
+      ( P x , Π-complete x)
+      ( ev-cauchy-approximation-Π-Metric-Space-WIP A P u x)
+
+  is-limit-limit-cauchy-approximation-Π-is-complete-Metric-Space-WIP :
+    (u : cauchy-approximation-Metric-Space-WIP (Π-Metric-Space-WIP A P)) →
+    is-limit-cauchy-approximation-Metric-Space-WIP
+      ( Π-Metric-Space-WIP A P)
+      ( u)
+      ( limit-cauchy-approximation-Π-is-complete-Metric-Space-WIP u)
+  is-limit-limit-cauchy-approximation-Π-is-complete-Metric-Space-WIP u ε δ x =
+    is-limit-limit-cauchy-approximation-Complete-Metric-Space-WIP
+      ( P x , Π-complete x)
+      ( ev-cauchy-approximation-Π-Metric-Space-WIP A P u x)
+      ( ε)
+      ( δ)
+
+  is-complete-Π-Metric-Space-WIP :
+    is-complete-Metric-Space-WIP (Π-Metric-Space-WIP A P)
+  is-complete-Π-Metric-Space-WIP u =
+    limit-cauchy-approximation-Π-is-complete-Metric-Space-WIP u ,
+    is-limit-limit-cauchy-approximation-Π-is-complete-Metric-Space-WIP u
+```
+
+### The complete product of complete metric spaces
+
+```agda
+module _
+  {l l1 l2 : Level} (A : UU l) (C : A → Complete-Metric-Space-WIP l1 l2)
+  where
+
+  Π-Complete-Metric-Space-WIP : Complete-Metric-Space-WIP (l ⊔ l1) (l ⊔ l2)
+  pr1 Π-Complete-Metric-Space-WIP =
+    Π-Metric-Space-WIP A (metric-space-Complete-Metric-Space-WIP ∘ C)
+  pr2 Π-Complete-Metric-Space-WIP =
+    is-complete-Π-Metric-Space-WIP
+      ( A)
+      ( metric-space-Complete-Metric-Space-WIP ∘ C)
+      ( is-complete-metric-space-Complete-Metric-Space-WIP ∘ C)
+```
diff --git a/src/metric-spaces/equality-of-metric-spaces-WIP.lagda.md b/src/metric-spaces/equality-of-metric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..454284610d
--- /dev/null
+++ b/src/metric-spaces/equality-of-metric-spaces-WIP.lagda.md
@@ -0,0 +1,241 @@
+# Equality of metric spaces (WIP)
+
+```agda
+module metric-spaces.equality-of-metric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.torsorial-type-families
+open import foundation.transport-along-identifications
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import metric-spaces.extensional-pseudometric-spaces-WIP
+open import metric-spaces.isometries-metric-spaces-WIP
+open import metric-spaces.metric-spaces-WIP
+open import metric-spaces.pseudometric-spaces-WIP
+open import metric-spaces.rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+[Equality](foundation-core.identity-types.md) of
+[metric spaces](metric-spaces.metric-spaces-WIP.md) is characterized by the
+following equivalent concepts:
+
+- an [equality](foundation-core.identity-types.md) between their carrier types
+  such that the induced map under [`map-eq`](foundation-core.univalence.md) is
+  an [isometry](metric-spaces.isometries-metric-spaces-WIP.md);
+
+- an [equivalence](foundation-core.equivalences.md) between their carrier types
+  such that the induced map under [`map-equiv`](foundation-core.equivalences.md)
+  is an [isometry](metric-spaces.isometries-metric-spaces-WIP.md);
+
+- a function between their carrier types that is both an
+  [equivalence](foundation-core.equivalences.md) and an
+  [isometry](metric-spaces.isometries-metric-spaces-WIP.md).
+
+## Definitions
+
+### Isometric equality between metric spaces
+
+```agda
+module _
+  {l1 l2 l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1 l2')
+  where
+
+  isometric-eq-Metric-Space-WIP : UU (lsuc l1 ⊔ l2 ⊔ l2')
+  isometric-eq-Metric-Space-WIP =
+    Σ (type-Metric-Space-WIP A ＝ type-Metric-Space-WIP B)
+      (λ e → is-isometry-Metric-Space-WIP A B (map-eq e))
+```
+
+### Isometric equivalence of metric spaces
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  where
+
+  isometric-equiv-Metric-Space-WIP : UU (l1 ⊔ l2 ⊔ l1' ⊔ l2')
+  isometric-equiv-Metric-Space-WIP =
+    Σ (type-Metric-Space-WIP A ≃ type-Metric-Space-WIP B)
+      (λ e → is-isometry-Metric-Space-WIP A B (map-equiv e))
+```
+
+### Isometric equivalences between metric spaces
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  where
+
+  isometric-equiv-Metric-Space-WIP' : UU (l1 ⊔ l2 ⊔ l1' ⊔ l2')
+  isometric-equiv-Metric-Space-WIP' =
+    Σ ( type-function-Metric-Space-WIP A B)
+      ( λ f → (is-equiv f) × (is-isometry-Metric-Space-WIP A B f))
+```
+
+## Properties
+
+### Equality of metric spaces is equivalent to the existence of an isometric equality between their carrier types
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A B : Metric-Space-WIP l1 l2)
+  where
+
+  equiv-eq-isometric-eq-Metric-Space-WIP :
+    (A ＝ B) ≃ isometric-eq-Metric-Space-WIP A B
+  equiv-eq-isometric-eq-Metric-Space-WIP =
+    ( equiv-tot
+      ( equiv-Eq-tr-Metric-Structure
+        ( type-Metric-Space-WIP A)
+        ( type-Metric-Space-WIP B)
+        ( structure-Metric-Space-WIP A)
+        ( structure-Metric-Space-WIP B))) ∘e
+    ( equiv-pair-eq-Σ A B)
+```
+
+### Isometric equality is torsorial
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A : Metric-Space-WIP l1 l2)
+  where
+
+  is-torsorial-isometric-eq-Metric-Space-WIP :
+    is-torsorial (isometric-eq-Metric-Space-WIP A)
+  is-torsorial-isometric-eq-Metric-Space-WIP =
+    is-contr-equiv'
+      ( Σ (Metric-Space-WIP l1 l2) (Id A))
+      ( equiv-tot (equiv-eq-isometric-eq-Metric-Space-WIP A))
+      ( is-torsorial-Id A)
+```
+
+### Isometric equality between the carrier types of metric spaces is equivalent to the existence of an isometric equivalence between them
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A B : Metric-Space-WIP l1 l2)
+  where
+
+  equiv-isometric-eq-equiv-Metric-Space-WIP :
+    isometric-eq-Metric-Space-WIP A B ≃ isometric-equiv-Metric-Space-WIP A B
+  equiv-isometric-eq-equiv-Metric-Space-WIP =
+    equiv-Σ
+      ( λ e → is-isometry-Metric-Space-WIP A B (map-equiv e))
+      ( equiv-univalence)
+      ( λ (e : type-Metric-Space-WIP A ＝ type-Metric-Space-WIP B) →
+        equiv-eq
+          (ap (is-isometry-Metric-Space-WIP A B) (eq-htpy (λ x → refl))))
+```
+
+### Isometric equivalence of metric spaces characterize their equalities
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A B : Metric-Space-WIP l1 l2)
+  where
+
+  equiv-eq-isometric-equiv-Metric-Space-WIP :
+    (A ＝ B) ≃ isometric-equiv-Metric-Space-WIP A B
+  equiv-eq-isometric-equiv-Metric-Space-WIP =
+    ( equiv-isometric-eq-equiv-Metric-Space-WIP A B) ∘e
+    ( equiv-eq-isometric-eq-Metric-Space-WIP A B)
+```
+
+### Isometric equivalence is torsorial
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A : Metric-Space-WIP l1 l2)
+  where
+
+  is-torsorial-isometric-equiv-Metric-Space-WIP :
+    is-torsorial (isometric-equiv-Metric-Space-WIP A)
+  is-torsorial-isometric-equiv-Metric-Space-WIP =
+    is-contr-equiv'
+      ( Σ (Metric-Space-WIP l1 l2) (Id A))
+      ( equiv-tot (equiv-eq-isometric-equiv-Metric-Space-WIP A))
+      ( is-torsorial-Id A)
+```
+
+### Two metric spaces are isometrically equivalent if and only if there is an isometric equivalence between them
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A B : Metric-Space-WIP l1 l2)
+  where
+
+  equiv-isometric-equiv-isometric-equiv-Metric-Space-WIP' :
+    isometric-equiv-Metric-Space-WIP A B ≃ isometric-equiv-Metric-Space-WIP' A B
+  equiv-isometric-equiv-isometric-equiv-Metric-Space-WIP' =
+    equiv-tot
+      ( λ f →
+        equiv-tot
+          ( λ e →
+            equiv-eq (ap (is-isometry-Metric-Space-WIP A B) refl))) ∘e
+    associative-Σ
+      ( type-function-Metric-Space-WIP A B)
+      ( is-equiv)
+      ( is-isometry-Metric-Space-WIP A B ∘ map-equiv)
+```
+
+### Isometric equivalences between metric spaces characterize their equality
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A B : Metric-Space-WIP l1 l2)
+  where
+
+  equiv-eq-isometric-equiv-Metric-Space-WIP' :
+    (A ＝ B) ≃ isometric-equiv-Metric-Space-WIP' A B
+  equiv-eq-isometric-equiv-Metric-Space-WIP' =
+    ( equiv-isometric-equiv-isometric-equiv-Metric-Space-WIP' A B) ∘e
+    ( equiv-eq-isometric-equiv-Metric-Space-WIP A B)
+```
+
+### The existence of invertibe isometries between metric spaces is torsorial
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A : Metric-Space-WIP l1 l2)
+  where
+
+  is-torsorial-isometric-equiv-Metric-Space-WIP' :
+    is-torsorial (isometric-equiv-Metric-Space-WIP' A)
+  is-torsorial-isometric-equiv-Metric-Space-WIP' =
+    is-contr-equiv'
+      ( Σ (Metric-Space-WIP l1 l2) (Id A))
+      ( equiv-tot (equiv-eq-isometric-equiv-Metric-Space-WIP' A))
+      ( is-torsorial-Id A)
+```
diff --git a/src/metric-spaces/extensional-pseudometric-spaces-WIP.lagda.md b/src/metric-spaces/extensional-pseudometric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..88e1883bee
--- /dev/null
+++ b/src/metric-spaces/extensional-pseudometric-spaces-WIP.lagda.md
@@ -0,0 +1,190 @@
+# Extensional pseudometric spaces (WIP)
+
+```agda
+module metric-spaces.extensional-pseudometric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.torsorial-type-families
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import metric-spaces.pseudometric-spaces-WIP
+open import metric-spaces.similarity-of-elements-pseudometric-spaces
+```
+
+</details>
+
+## Idea
+
+A [pseudometric space](metric-spaces.pseudometric-spaces-WIP.md) is called
+{{#concept "extensional" Disambiguation="pseudometric space" Agda=is-extensional-Pseudometric-Space-WIP}}
+if any of the following equivalent condition holds:
+
+- any [similar](metric-spaces.similarity-of-elements-pseudometric-spaces.md)
+  elements are [identical](foundation-core.identity-types.md);
+- the similarity relation has [propositional](foundation.propositions.md)
+  fibers;
+- the similarity relation is [torsorial](foundation.torsorial-type-families.md).
+
+The carrier type of an extensional pseudometric space is a
+[set](foundation.sets.md) and the
+[discrete pseudometric structure](metric-spaces.discrete-premetric-structures.md)
+over a set is extensional.
+
+## Definitions
+
+### The property of being an extensional pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  where
+
+  is-extensional-prop-Pseudometric-Space-WIP : Prop (l1 ⊔ l2)
+  is-extensional-prop-Pseudometric-Space-WIP =
+    Π-Prop
+      ( type-Pseudometric-Space-WIP A)
+      ( is-prop-Prop ∘
+        Σ (type-Pseudometric-Space-WIP A) ∘
+        sim-Pseudometric-Space-WIP A)
+
+  is-extensional-Pseudometric-Space-WIP : UU (l1 ⊔ l2)
+  is-extensional-Pseudometric-Space-WIP =
+    type-Prop is-extensional-prop-Pseudometric-Space-WIP
+
+  is-prop-is-extensional-Pseudometric-Space-WIP :
+    is-prop is-extensional-Pseudometric-Space-WIP
+  is-prop-is-extensional-Pseudometric-Space-WIP =
+    is-prop-type-Prop is-extensional-prop-Pseudometric-Space-WIP
+```
+
+### Tightness of a pseudometric space
+
+A pseudometric space is
+{{#concept "tight" Disambiguation="pseudometric" Agda=is-tight-Pseudometric-Space-WIP}}
+if any two
+[similar](metric-spaces.similarity-of-elements-pseudometric-spaces.md) elements
+are [equal](foundation-core.identity-types.md).
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  where
+
+  is-tight-Pseudometric-Space-WIP : UU (l1 ⊔ l2)
+  is-tight-Pseudometric-Space-WIP =
+    (x y : type-Pseudometric-Space-WIP A) →
+    sim-Pseudometric-Space-WIP A x y →
+    x ＝ y
+```
+
+## Properties
+
+### Any tight pseudometric space is extensional
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  (T : is-tight-Pseudometric-Space-WIP A)
+  where
+
+  is-extensional-is-tight-Pseudometric-Space :
+    is-extensional-Pseudometric-Space-WIP A
+  is-extensional-is-tight-Pseudometric-Space x =
+    is-prop-all-elements-equal
+      ( λ (u , I) (v , J) →
+        eq-type-subtype
+          ( sim-prop-Pseudometric-Space-WIP A x)
+          ( inv (T x u I) ∙ T x v J))
+```
+
+### Characterization of equality in an extensional pseudometric space
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  (E : is-extensional-Pseudometric-Space-WIP A)
+  where
+
+  is-torsorial-sim-is-extensional-Pseudometric-Space-WIP :
+    (x : type-Pseudometric-Space-WIP A) →
+    is-torsorial (sim-Pseudometric-Space-WIP A x)
+  is-torsorial-sim-is-extensional-Pseudometric-Space-WIP x =
+    is-proof-irrelevant-is-prop
+      ( E x)
+      ( x , refl-sim-Pseudometric-Space-WIP A x)
+
+  is-fiberwise-equiv-sim-eq-is-extensional-Pseudometric-Space-WIP :
+    (x y : type-Pseudometric-Space-WIP A) →
+    is-equiv (sim-eq-Pseudometric-Space-WIP A x y)
+  is-fiberwise-equiv-sim-eq-is-extensional-Pseudometric-Space-WIP x =
+    fundamental-theorem-id
+      ( is-torsorial-sim-is-extensional-Pseudometric-Space-WIP x)
+      ( sim-eq-Pseudometric-Space-WIP A x)
+
+  equiv-sim-eq-is-extensional-Pseudometric-Space-WIP :
+    (x y : type-Pseudometric-Space-WIP A) →
+    (x ＝ y) ≃ (sim-Pseudometric-Space-WIP A x y)
+  equiv-sim-eq-is-extensional-Pseudometric-Space-WIP x y =
+    ( sim-eq-Pseudometric-Space-WIP A x y) ,
+    ( is-fiberwise-equiv-sim-eq-is-extensional-Pseudometric-Space-WIP x y)
+
+  eq-sim-is-extensional-Pseudometric-Space-WIP :
+    (x y : type-Pseudometric-Space-WIP A) →
+    sim-Pseudometric-Space-WIP A x y →
+    x ＝ y
+  eq-sim-is-extensional-Pseudometric-Space-WIP x y =
+    map-inv-equiv (equiv-sim-eq-is-extensional-Pseudometric-Space-WIP x y)
+```
+
+### Any extensional pseudometric is tight
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  (E : is-extensional-Pseudometric-Space-WIP A)
+  where
+
+  is-tight-is-extensional-Pseudometric-Space-WIP :
+    is-tight-Pseudometric-Space-WIP A
+  is-tight-is-extensional-Pseudometric-Space-WIP =
+    eq-sim-is-extensional-Pseudometric-Space-WIP A E
+```
+
+### The carrier type of an extensional pseudometric space is a set
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  (E : is-extensional-Pseudometric-Space-WIP A)
+  where
+
+  is-set-type-is-extensional-Pseudometric-Space-WIP :
+    is-set (type-Pseudometric-Space-WIP A)
+  is-set-type-is-extensional-Pseudometric-Space-WIP x y =
+    is-prop-is-equiv
+      ( is-fiberwise-equiv-sim-eq-is-extensional-Pseudometric-Space-WIP
+        ( A)
+        ( E)
+        ( x)
+        ( y))
+      ( is-prop-sim-Pseudometric-Space-WIP A x y)
+```
+
+## See also
+
+- [metric spaces](metric-spaces.metric-spaces-WIP.md): the type of extensional
+  pseudometric spaces.
diff --git a/src/metric-spaces/isometries-metric-spaces-WIP.lagda.md b/src/metric-spaces/isometries-metric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..f892cc239c
--- /dev/null
+++ b/src/metric-spaces/isometries-metric-spaces-WIP.lagda.md
@@ -0,0 +1,434 @@
+# Isometries between metric spaces (WIP)
+
+```agda
+module metric-spaces.isometries-metric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.binary-transport
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.injective-maps
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.sequences
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import metric-spaces.metric-spaces-WIP
+open import metric-spaces.preimage-rational-neighborhoods
+open import metric-spaces.rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+A [function](metric-spaces.functions-metric-spaces.md) between
+[metric spaces](metric-spaces.metric-spaces.md) is an
+{{#concept "isometry" Disambiguation="between metric spaces" Agda=is-isometry-Metric-Space-WIP}}
+if the [rational neighborhood relation](metric-spaces.rational-neighborhoods.md)
+on `A` is equivalent to the
+[preimage](metric-spaces.preimage-rational-neighborhoods.md) by `f` of the
+rational neighborhood relation on `B`. I.e., upper bounds on the distance
+between two points in `A` are exactly the upper bounds of the distance between
+their images in `B`.
+
+## Definitions
+
+### The property of being a isometry between metric spaces
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  (f : type-function-Metric-Space-WIP A B)
+  where
+
+  is-isometry-prop-Metric-Space-WIP : Prop (l1 ⊔ l2 ⊔ l2')
+  is-isometry-prop-Metric-Space-WIP =
+    Eq-prop-Rational-Neighborhood-Relation
+      ( neighborhood-prop-Metric-Space-WIP A)
+      ( preimage-Rational-Neighborhood-Relation
+        ( f)
+        ( neighborhood-prop-Metric-Space-WIP B))
+
+  is-isometry-Metric-Space-WIP : UU (l1 ⊔ l2 ⊔ l2')
+  is-isometry-Metric-Space-WIP =
+    type-Prop is-isometry-prop-Metric-Space-WIP
+
+  is-prop-is-isometry-Metric-Space-WIP :
+    is-prop is-isometry-Metric-Space-WIP
+  is-prop-is-isometry-Metric-Space-WIP =
+    is-prop-type-Prop is-isometry-prop-Metric-Space-WIP
+```
+
+### The set of isometries between metric spaces
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  where
+
+  set-isometry-Metric-Space-WIP : Set (l1 ⊔ l2 ⊔ l1' ⊔ l2')
+  set-isometry-Metric-Space-WIP =
+    set-subset
+      ( set-function-Metric-Space-WIP A B)
+      ( is-isometry-prop-Metric-Space-WIP A B)
+
+  isometry-Metric-Space-WIP : UU (l1 ⊔ l2 ⊔ l1' ⊔ l2')
+  isometry-Metric-Space-WIP = type-Set set-isometry-Metric-Space-WIP
+
+  is-set-isometry-Metric-Space-WIP : is-set isometry-Metric-Space-WIP
+  is-set-isometry-Metric-Space-WIP =
+    is-set-type-Set set-isometry-Metric-Space-WIP
+
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  (f : isometry-Metric-Space-WIP A B)
+  where
+
+  map-isometry-Metric-Space-WIP : type-function-Metric-Space-WIP A B
+  map-isometry-Metric-Space-WIP = pr1 f
+
+  is-isometry-map-isometry-Metric-Space-WIP :
+    is-isometry-Metric-Space-WIP A B map-isometry-Metric-Space-WIP
+  is-isometry-map-isometry-Metric-Space-WIP = pr2 f
+```
+
+## Properties
+
+### The identity function on a metric space is an isometry
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  where
+
+  is-isometry-id-Metric-Space-WIP :
+    is-isometry-Metric-Space-WIP A A (λ x → x)
+  is-isometry-id-Metric-Space-WIP d x y = id-iff
+
+  isometry-id-Metric-Space-WIP : isometry-Metric-Space-WIP A A
+  isometry-id-Metric-Space-WIP =
+    (λ x → x) , is-isometry-id-Metric-Space-WIP
+```
+
+### Equality of isometries in metric spaces is equivalent to homotopies between their carrier maps
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  (f g : isometry-Metric-Space-WIP A B)
+  where
+
+  equiv-eq-htpy-map-isometry-Metric-Space-WIP :
+    (f ＝ g) ≃
+    (map-isometry-Metric-Space-WIP A B f ~ map-isometry-Metric-Space-WIP A B g)
+  equiv-eq-htpy-map-isometry-Metric-Space-WIP =
+    equiv-funext ∘e
+    extensionality-type-subtype'
+      ( is-isometry-prop-Metric-Space-WIP A B)
+      ( f)
+      ( g)
+
+  htpy-eq-map-isometry-Metric-Space-WIP :
+    (f ＝ g) →
+    (map-isometry-Metric-Space-WIP A B f ~ map-isometry-Metric-Space-WIP A B g)
+  htpy-eq-map-isometry-Metric-Space-WIP =
+    map-equiv equiv-eq-htpy-map-isometry-Metric-Space-WIP
+
+  eq-htpy-map-isometry-Metric-Space-WIP :
+    ( map-isometry-Metric-Space-WIP A B f ~
+      map-isometry-Metric-Space-WIP A B g) →
+    (f ＝ g)
+  eq-htpy-map-isometry-Metric-Space-WIP =
+    map-inv-equiv equiv-eq-htpy-map-isometry-Metric-Space-WIP
+```
+
+### An isometry preserves and reflects neighborhoods
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  (f : isometry-Metric-Space-WIP A B)
+  where
+
+  preserves-neighborhood-map-isometry-Metric-Space-WIP :
+    (d : ℚ⁺) (x y : type-Metric-Space-WIP A) →
+    neighborhood-Metric-Space-WIP A d x y →
+    neighborhood-Metric-Space-WIP
+      ( B)
+      ( d)
+      ( map-isometry-Metric-Space-WIP A B f x)
+      ( map-isometry-Metric-Space-WIP A B f y)
+  preserves-neighborhood-map-isometry-Metric-Space-WIP d x y =
+    forward-implication
+      ( is-isometry-map-isometry-Metric-Space-WIP A B f d x y)
+
+  reflects-neighborhood-map-isometry-Metric-Space-WIP :
+    (d : ℚ⁺) (x y : type-Metric-Space-WIP A) →
+    neighborhood-Metric-Space-WIP
+      ( B)
+      ( d)
+      ( map-isometry-Metric-Space-WIP A B f x)
+      ( map-isometry-Metric-Space-WIP A B f y) →
+    neighborhood-Metric-Space-WIP A d x y
+  reflects-neighborhood-map-isometry-Metric-Space-WIP d x y =
+    backward-implication
+      ( is-isometry-map-isometry-Metric-Space-WIP A B f d x y)
+```
+
+### Composition of isometries
+
+```agda
+module _
+  {l1a l2a l1b l2b l1c l2c : Level}
+  (A : Metric-Space-WIP l1a l2a)
+  (B : Metric-Space-WIP l1b l2b)
+  (C : Metric-Space-WIP l1c l2c)
+  where
+
+  is-isometry-comp-is-isometry-Metric-Space-WIP :
+    (g : type-function-Metric-Space-WIP B C) →
+    (f : type-function-Metric-Space-WIP A B) →
+    is-isometry-Metric-Space-WIP B C g →
+    is-isometry-Metric-Space-WIP A B f →
+    is-isometry-Metric-Space-WIP A C (g ∘ f)
+  is-isometry-comp-is-isometry-Metric-Space-WIP g f H K d x y =
+    H d (f x) (f y) ∘iff K d x y
+
+  comp-isometry-Metric-Space-WIP :
+    isometry-Metric-Space-WIP B C →
+    isometry-Metric-Space-WIP A B →
+    isometry-Metric-Space-WIP A C
+  comp-isometry-Metric-Space-WIP g f =
+    ( map-isometry-Metric-Space-WIP B C g ∘
+      map-isometry-Metric-Space-WIP A B f) ,
+    ( is-isometry-comp-is-isometry-Metric-Space-WIP
+      ( map-isometry-Metric-Space-WIP B C g)
+      ( map-isometry-Metric-Space-WIP A B f)
+      ( is-isometry-map-isometry-Metric-Space-WIP B C g)
+      ( is-isometry-map-isometry-Metric-Space-WIP A B f))
+```
+
+### Unit laws for composition of isometries between metric spaces
+
+```agda
+module _
+  {l1a l2a l1b l2b : Level}
+  (A : Metric-Space-WIP l1a l2a)
+  (B : Metric-Space-WIP l1b l2b)
+  (f : isometry-Metric-Space-WIP A B)
+  where
+
+  left-unit-law-comp-isometry-Metric-Space-WIP :
+    ( comp-isometry-Metric-Space-WIP A B B
+      (isometry-id-Metric-Space-WIP B)
+      ( f)) ＝
+    ( f)
+  left-unit-law-comp-isometry-Metric-Space-WIP =
+    eq-htpy-map-isometry-Metric-Space-WIP
+      ( A)
+      ( B)
+      ( comp-isometry-Metric-Space-WIP
+        ( A)
+        ( B)
+        ( B)
+        (isometry-id-Metric-Space-WIP B)
+        ( f))
+      ( f)
+      ( λ x → refl)
+
+  right-unit-law-comp-isometry-Metric-Space-WIP :
+    ( comp-isometry-Metric-Space-WIP A A B
+      ( f)
+      ( isometry-id-Metric-Space-WIP A)) ＝
+    ( f)
+  right-unit-law-comp-isometry-Metric-Space-WIP =
+    eq-htpy-map-isometry-Metric-Space-WIP
+      ( A)
+      ( B)
+      ( f)
+      ( comp-isometry-Metric-Space-WIP
+        ( A)
+        ( A)
+        ( B)
+        ( f)
+        ( isometry-id-Metric-Space-WIP A))
+      ( λ x → refl)
+```
+
+### Associativity of composition of isometries between metric spaces
+
+```agda
+module _
+  {l1a l2a l1b l2b l1c l2c l1d l2d : Level}
+  (A : Metric-Space-WIP l1a l2a)
+  (B : Metric-Space-WIP l1b l2b)
+  (C : Metric-Space-WIP l1c l2c)
+  (D : Metric-Space-WIP l1d l2d)
+  (h : isometry-Metric-Space-WIP C D)
+  (g : isometry-Metric-Space-WIP B C)
+  (f : isometry-Metric-Space-WIP A B)
+  where
+
+  associative-comp-isometry-Metric-Space-WIP :
+    ( comp-isometry-Metric-Space-WIP A B D
+      ( comp-isometry-Metric-Space-WIP B C D h g)
+      ( f)) ＝
+    ( comp-isometry-Metric-Space-WIP A C D
+      ( h)
+      ( comp-isometry-Metric-Space-WIP A B C g f))
+  associative-comp-isometry-Metric-Space-WIP =
+    eq-htpy-map-isometry-Metric-Space-WIP
+      ( A)
+      ( D)
+      ( comp-isometry-Metric-Space-WIP A B D
+        ( comp-isometry-Metric-Space-WIP B C D h g)
+        ( f))
+      ( comp-isometry-Metric-Space-WIP A C D
+        ( h)
+        ( comp-isometry-Metric-Space-WIP A B C g f))
+      ( λ x → refl)
+```
+
+### The inverse of an isometric equivalence is an isometry
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  where
+
+  is-isometry-map-inv-is-equiv-is-isometry-Metric-Space-WIP :
+    (f : type-function-Metric-Space-WIP A B) →
+    is-isometry-Metric-Space-WIP A B f →
+    (E : is-equiv f) →
+    is-isometry-Metric-Space-WIP B A (map-inv-is-equiv E)
+  is-isometry-map-inv-is-equiv-is-isometry-Metric-Space-WIP f I E d x y =
+    logical-equivalence-reasoning
+      ( neighborhood-Metric-Space-WIP B d x y)
+      ↔ ( neighborhood-Metric-Space-WIP B d
+          ( f (map-inv-is-equiv E x))
+          ( f (map-inv-is-equiv E y)))
+        by
+          binary-tr
+            ( λ u v →
+              ( neighborhood-Metric-Space-WIP B d x y) ↔
+              ( neighborhood-Metric-Space-WIP B d u v))
+            ( inv (is-section-map-inv-is-equiv E x))
+            ( inv (is-section-map-inv-is-equiv E y))
+            ( id-iff)
+      ↔ ( neighborhood-Metric-Space-WIP A d
+          ( map-inv-is-equiv E x)
+          ( map-inv-is-equiv E y))
+        by
+          inv-iff
+            ( I d (map-inv-is-equiv E x) (map-inv-is-equiv E y))
+
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  (f : isometry-Metric-Space-WIP A B)
+  (E : is-equiv (map-isometry-Metric-Space-WIP A B f))
+  where
+
+  isometry-inv-is-equiv-isometry-Metric-Space-WIP :
+    isometry-Metric-Space-WIP B A
+  isometry-inv-is-equiv-isometry-Metric-Space-WIP =
+    ( map-inv-is-equiv E) ,
+    ( is-isometry-map-inv-is-equiv-is-isometry-Metric-Space-WIP
+      ( A)
+      ( B)
+      ( map-isometry-Metric-Space-WIP A B f)
+      ( is-isometry-map-isometry-Metric-Space-WIP A B f)
+      ( E))
+
+  is-section-isometry-inv-is-equiv-isometry-Metric-Space-WIP :
+    ( comp-isometry-Metric-Space-WIP
+      B
+      A
+      B
+      f
+      isometry-inv-is-equiv-isometry-Metric-Space-WIP) ＝
+    ( isometry-id-Metric-Space-WIP B)
+  is-section-isometry-inv-is-equiv-isometry-Metric-Space-WIP =
+    eq-htpy-map-isometry-Metric-Space-WIP
+      ( B)
+      ( B)
+      ( comp-isometry-Metric-Space-WIP
+        B
+        A
+        B
+        f
+        isometry-inv-is-equiv-isometry-Metric-Space-WIP)
+      ( isometry-id-Metric-Space-WIP B)
+      ( is-section-map-inv-is-equiv E)
+
+  is-retraction-isometry-inv-is-equiv-isometry-Metric-Space-WIP :
+    ( comp-isometry-Metric-Space-WIP
+      A
+      B
+      A
+      isometry-inv-is-equiv-isometry-Metric-Space-WIP
+      f) ＝
+    ( isometry-id-Metric-Space-WIP A)
+  is-retraction-isometry-inv-is-equiv-isometry-Metric-Space-WIP =
+    eq-htpy-map-isometry-Metric-Space-WIP
+      ( A)
+      ( A)
+      ( comp-isometry-Metric-Space-WIP
+        A
+        B
+        A
+        isometry-inv-is-equiv-isometry-Metric-Space-WIP
+        f)
+      ( isometry-id-Metric-Space-WIP A)
+      ( is-retraction-map-inv-is-equiv E)
+```
+
+### Any isometry between metric spaces is an embedding
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  (f : isometry-Metric-Space-WIP A B)
+  where
+
+  is-injective-map-isometry-Metric-Space-WIP :
+    is-injective (map-isometry-Metric-Space-WIP A B f)
+  is-injective-map-isometry-Metric-Space-WIP H =
+    eq-sim-Metric-Space-WIP
+      ( A)
+      ( _)
+      ( _)
+      ( λ d →
+        backward-implication
+          ( is-isometry-map-isometry-Metric-Space-WIP A B f d _ _)
+          ( sim-eq-Metric-Space-WIP B _ _ H d))
+
+  is-emb-map-isometry-Metric-Space-WIP :
+    is-emb (map-isometry-Metric-Space-WIP A B f)
+  is-emb-map-isometry-Metric-Space-WIP =
+    is-emb-is-injective
+      ( is-set-type-Metric-Space-WIP B)
+      ( is-injective-map-isometry-Metric-Space-WIP)
+```
diff --git a/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces-WIP.lagda.md b/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..d98457829f
--- /dev/null
+++ b/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces-WIP.lagda.md
@@ -0,0 +1,144 @@
+# Limits of Cauchy approximations in metric spaces (WIP)
+
+```agda
+module metric-spaces.limits-of-cauchy-approximations-metric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import metric-spaces.cauchy-approximations-metric-spaces-WIP
+open import metric-spaces.metric-spaces-WIP
+```
+
+</details>
+
+## Idea
+
+A [Cauchy approximation](metric-spaces.cauchy-approximations-metric-spaces.md)
+`f : ℚ⁺ → A` in a [metric space](metric-spaces.metric-spaces.md) `A` has a
+{{#concept "limit" Disambiguation="of a Cauchy approximation in a metric space Agda=is-limit-cauchy-approximation-Metric-Space-WIP}}
+`x : A` if `f ε` is near `x` for small `ε : ℚ⁺`; more precisely, if `f ε` is in
+a `ε + δ`-[neighborhood](metric-spaces.rational-neighborhoods.md) of `x` for all
+`ε δ : ℚ⁺`.
+
+## Definitions
+
+### The property of having a limit in a metric space
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  (f : cauchy-approximation-Metric-Space-WIP A)
+  where
+
+  is-limit-cauchy-approximation-prop-Metric-Space-WIP :
+    type-Metric-Space-WIP A → Prop l2
+  is-limit-cauchy-approximation-prop-Metric-Space-WIP lim =
+    Π-Prop
+      ( ℚ⁺)
+      ( λ ε →
+        Π-Prop
+          ( ℚ⁺)
+          ( λ δ →
+            neighborhood-prop-Metric-Space-WIP
+              ( A)
+              ( ε +ℚ⁺ δ)
+              ( map-cauchy-approximation-Metric-Space-WIP A f ε)
+              ( lim)))
+
+  is-limit-cauchy-approximation-Metric-Space-WIP :
+    type-Metric-Space-WIP A → UU l2
+  is-limit-cauchy-approximation-Metric-Space-WIP =
+    type-Prop ∘ is-limit-cauchy-approximation-prop-Metric-Space-WIP
+```
+
+## Properties
+
+### Limits in a metric space are unique
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  (f : cauchy-approximation-Metric-Space-WIP A)
+  (x y : type-Metric-Space-WIP A)
+  where
+
+  all-sim-is-limit-cauchy-approximation-Metric-Space-WIP :
+    is-limit-cauchy-approximation-Metric-Space-WIP A f x →
+    is-limit-cauchy-approximation-Metric-Space-WIP A f y →
+    sim-Metric-Space-WIP A x y
+  all-sim-is-limit-cauchy-approximation-Metric-Space-WIP lim-x lim-y d =
+    let
+      (ε , δ , ε+δ=d) = split-ℚ⁺ d
+      θ = mediant-zero-min-ℚ⁺ ε δ
+      θ<ε = le-left-mediant-zero-min-ℚ⁺ ε δ
+      θ<δ = le-right-mediant-zero-min-ℚ⁺ ε δ
+      ε' = le-diff-ℚ⁺ θ ε θ<ε
+      δ' = le-diff-ℚ⁺ θ δ θ<δ
+      fθ = map-cauchy-approximation-Metric-Space-WIP A f θ
+
+      Nεx : neighborhood-Metric-Space-WIP A ε fθ x
+      Nεx =
+        tr
+          ( is-upper-bound-dist-Metric-Space-WIP A fθ x)
+          ( right-diff-law-add-ℚ⁺ θ ε θ<ε)
+          ( lim-x θ ε')
+
+      Nδy : neighborhood-Metric-Space-WIP A δ fθ y
+      Nδy =
+        tr
+          ( is-upper-bound-dist-Metric-Space-WIP A fθ y)
+          ( right-diff-law-add-ℚ⁺ θ δ θ<δ)
+          ( lim-y θ δ')
+
+      Nxy : neighborhood-Metric-Space-WIP A (ε +ℚ⁺ δ) x y
+      Nxy =
+        triangular-neighborhood-Metric-Space-WIP
+          ( A)
+          ( x)
+          ( fθ)
+          ( y)
+          ( ε)
+          ( δ)
+          ( Nδy)
+          ( symmetric-neighborhood-Metric-Space-WIP A ε fθ x Nεx)
+    in
+      tr
+        ( is-upper-bound-dist-Metric-Space-WIP A x y)
+        ( ε+δ=d)
+        ( Nxy)
+
+  all-eq-is-limit-cauchy-approximation-Metric-Space-WIP :
+    is-limit-cauchy-approximation-Metric-Space-WIP A f x →
+    is-limit-cauchy-approximation-Metric-Space-WIP A f y →
+    x ＝ y
+  all-eq-is-limit-cauchy-approximation-Metric-Space-WIP lim-x lim-y =
+    eq-sim-Metric-Space-WIP
+      ( A)
+      ( x)
+      ( y)
+      ( all-sim-is-limit-cauchy-approximation-Metric-Space-WIP lim-x lim-y)
+```
+
+## See also
+
+- [convergent cauchy approximations](metric-spaces.convergent-cauchy-approximations-metric-spaces-WIP.md):
+  the type of Cauchy approximations with a limit.
+
+## References
+
+Our definition of limit of Cauchy approximation follows Definition 11.2.10 of
+{{#cite UF13}}.
+
+{{#bibliography}}
diff --git a/src/metric-spaces/limits-of-functions-metric-spaces.lagda.md b/src/metric-spaces/limits-of-functions-metric-spaces.lagda.md
new file mode 100644
index 0000000000..af4cc8d527
--- /dev/null
+++ b/src/metric-spaces/limits-of-functions-metric-spaces.lagda.md
@@ -0,0 +1,71 @@
+# Limits of functions between metric spaces
+
+```agda
+module metric-spaces.limits-of-functions-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.existential-quantification
+open import foundation.inhabited-subtypes
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import metric-spaces.metric-spaces-WIP
+```
+
+</details>
+
+## Idea
+
+A [function](metric-spaces.functions-metric-spaces.md) `f` between
+[metric spaces](metric-spaces.metric-spaces.md) `X` and `Y` has a
+{{#concept "limit" Disambiguation="of function between metric spaces at a point" Agda=is-pt-limit-function-Metric-Space-WIP}}
+`y : Y` at a point `x : X` if there exists a function `m : ℚ⁺ → ℚ⁺` such that
+whenever `x'` is in an `m ε`-neighborhood of `x`, `f x'` is in an
+`ε`-neighborhood of `y`. `m` is called a limit modulus of `f` at `x`.
+
+## Definitions
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (X : Metric-Space-WIP l1 l2)
+  (Y : Metric-Space-WIP l3 l4)
+  (f : type-function-Metric-Space-WIP X Y)
+  (x : type-Metric-Space-WIP X)
+  (y : type-Metric-Space-WIP Y)
+  where
+
+  is-modulus-of-pt-limit-prop-function-Metric-Space-WIP :
+    (ℚ⁺ → ℚ⁺) → Prop (l1 ⊔ l2 ⊔ l4)
+  is-modulus-of-pt-limit-prop-function-Metric-Space-WIP m =
+    Π-Prop
+      ( ℚ⁺)
+      ( λ ε →
+        Π-Prop
+        ( type-Metric-Space-WIP X)
+        ( λ x' →
+          neighborhood-prop-Metric-Space-WIP X (m ε) x x' ⇒
+          neighborhood-prop-Metric-Space-WIP Y ε y (f x')))
+
+  is-modulus-of-pt-limit-function-Metric-Space-WIP :
+    (ℚ⁺ → ℚ⁺) → UU (l1 ⊔ l2 ⊔ l4)
+  is-modulus-of-pt-limit-function-Metric-Space-WIP m =
+    type-Prop (is-modulus-of-pt-limit-prop-function-Metric-Space-WIP m)
+
+  is-pt-limit-prop-function-Metric-Space-WIP : Prop (l1 ⊔ l2 ⊔ l4)
+  is-pt-limit-prop-function-Metric-Space-WIP =
+    is-inhabited-subtype-Prop
+      is-modulus-of-pt-limit-prop-function-Metric-Space-WIP
+
+  is-pt-limit-function-Metric-Space-WIP : UU (l1 ⊔ l2 ⊔ l4)
+  is-pt-limit-function-Metric-Space-WIP =
+    type-Prop is-pt-limit-prop-function-Metric-Space-WIP
+```
diff --git a/src/metric-spaces/metric-space-of-rational-numbers-WIP.lagda.md b/src/metric-spaces/metric-space-of-rational-numbers-WIP.lagda.md
new file mode 100644
index 0000000000..506eecbe30
--- /dev/null
+++ b/src/metric-spaces/metric-space-of-rational-numbers-WIP.lagda.md
@@ -0,0 +1,459 @@
+# The standard metric space of the rational numbers (WIP)
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module metric-spaces.metric-space-of-rational-numbers-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.absolute-value-rational-numbers
+open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.difference-rational-numbers
+open import elementary-number-theory.distance-rational-numbers
+open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.nonnegative-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.diagonal-maps-cartesian-products-of-types
+open import foundation.empty-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.functoriality-cartesian-product-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import metric-spaces.cauchy-approximations-metric-spaces-WIP
+open import metric-spaces.convergent-cauchy-approximations-metric-spaces-WIP
+open import metric-spaces.extensional-pseudometric-spaces-WIP
+open import metric-spaces.isometries-metric-spaces-WIP
+open import metric-spaces.limits-of-cauchy-approximations-metric-spaces-WIP
+open import metric-spaces.metric-spaces-WIP
+open import metric-spaces.monotonic-rational-neighborhoods
+open import metric-spaces.pseudometric-spaces-WIP
+open import metric-spaces.rational-neighborhoods
+open import metric-spaces.reflexive-rational-neighborhoods
+open import metric-spaces.saturated-rational-neighborhoods
+open import metric-spaces.short-functions-metric-spaces-WIP
+open import metric-spaces.symmetric-rational-neighborhoods
+open import metric-spaces.triangular-rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+[Inequality](elementary-number-theory.inequality-rational-numbers.md) on the
+[rational numbers](elementary-number-theory.rational-numbers.md) induces a
+[premetric](metric-spaces.premetric-structures.md) on `ℚ` where `x y : ℚ` are in
+a `d`-neighborhood when `y ≤ x + d` and `x ≤ y + d`, i.e. upper bounds on the
+distance between `x` and `y` are upper bounds of both `y - x` and `x - y`. This
+is a [metric structure](metric-spaces.metric-structures.md) on `ℚ` that defines
+the
+{{#concept "standard metric space of rational numbers" Agda=metric-space-ℚ}}.
+
+## Definitions
+
+### The standard saturated saturated neighborhood relation on the rational numbers
+
+```agda
+lower-neighborhood-prop-ℚ : (d : ℚ⁺) (x y : ℚ) → Prop lzero
+lower-neighborhood-prop-ℚ d x y =
+  leq-ℚ-Prop y (x +ℚ (rational-ℚ⁺ d))
+
+lower-neighborhood-ℚ : (d : ℚ⁺) (x y : ℚ) → UU lzero
+lower-neighborhood-ℚ d x y = type-Prop (lower-neighborhood-prop-ℚ d x y)
+
+is-prop-lower-neighborhood-ℚ :
+  (d : ℚ⁺) (x y : ℚ) → is-prop (lower-neighborhood-ℚ d x y)
+is-prop-lower-neighborhood-ℚ d x y =
+  is-prop-type-Prop (lower-neighborhood-prop-ℚ d x y)
+
+neighborhood-prop-ℚ : Rational-Neighborhood-Relation lzero ℚ
+neighborhood-prop-ℚ d x y =
+  product-Prop
+    ( lower-neighborhood-prop-ℚ d x y)
+    ( lower-neighborhood-prop-ℚ d y x)
+
+neighborhood-ℚ : (d : ℚ⁺) (x y : ℚ) → UU lzero
+neighborhood-ℚ d x y = type-Prop (neighborhood-prop-ℚ d x y)
+```
+
+## Properties
+
+### The standard premetric on the rational numbers is a metric
+
+```agda
+is-reflexive-neighborhood-ℚ :
+  is-reflexive-Rational-Neighborhood-Relation neighborhood-prop-ℚ
+is-reflexive-neighborhood-ℚ d x =
+  diagonal-product
+    ( leq-ℚ x (x +ℚ (rational-ℚ⁺ d)))
+    ( leq-le-ℚ {x} {x +ℚ (rational-ℚ⁺ d)} (le-right-add-rational-ℚ⁺ x d))
+
+is-symmetric-neighborhood-ℚ :
+  is-symmetric-Rational-Neighborhood-Relation neighborhood-prop-ℚ
+is-symmetric-neighborhood-ℚ d x y (H , K) = (K , H)
+
+is-triangular-neighborhood-ℚ :
+  is-triangular-Rational-Neighborhood-Relation neighborhood-prop-ℚ
+pr1 (is-triangular-neighborhood-ℚ x y z d₁ d₂ Hyz Hxy) =
+  tr
+    ( leq-ℚ z)
+    ( associative-add-ℚ x (rational-ℚ⁺ d₁) (rational-ℚ⁺ d₂))
+    ( transitive-leq-ℚ
+      ( z)
+      ( y +ℚ ( rational-ℚ⁺ d₂))
+      ( x +ℚ (rational-ℚ⁺ d₁) +ℚ (rational-ℚ⁺ d₂))
+      ( preserves-leq-left-add-ℚ
+        ( rational-ℚ⁺ d₂)
+        ( y)
+        ( x +ℚ (rational-ℚ⁺ d₁))
+        ( pr1 Hxy))
+      ( pr1 Hyz))
+pr2 (is-triangular-neighborhood-ℚ x y z d₁ d₂ Hyz Hxy) =
+  tr
+    ( leq-ℚ x)
+    ( ap (z +ℚ_) (commutative-add-ℚ (rational-ℚ⁺ d₂) (rational-ℚ⁺ d₁)))
+    ( tr
+      ( leq-ℚ x)
+      ( associative-add-ℚ z (rational-ℚ⁺ d₂) (rational-ℚ⁺ d₁))
+      ( transitive-leq-ℚ
+        ( x)
+        ( y +ℚ (rational-ℚ⁺ d₁))
+        ( z +ℚ (rational-ℚ⁺ d₂) +ℚ (rational-ℚ⁺ d₁))
+        ( ( preserves-leq-left-add-ℚ
+          ( rational-ℚ⁺ d₁)
+          ( y)
+          ( z +ℚ (rational-ℚ⁺ d₂))
+          ( pr2 Hyz)))
+        ( pr2 Hxy)))
+
+is-saturated-neighborhood-ℚ :
+  is-saturated-Rational-Neighborhood-Relation neighborhood-prop-ℚ
+is-saturated-neighborhood-ℚ ε x y H =
+  map-inv-equiv
+    ( equiv-leq-leq-add-positive-ℚ y (x +ℚ rational-ℚ⁺ ε))
+    ( λ δ →
+      inv-tr
+        ( leq-ℚ y)
+        ( associative-add-ℚ x (rational-ℚ⁺ ε) (rational-ℚ⁺ δ))
+        ( pr1 (H δ))) ,
+  map-inv-equiv
+    ( equiv-leq-leq-add-positive-ℚ x (y +ℚ rational-ℚ⁺ ε))
+    ( λ δ →
+      inv-tr
+        ( leq-ℚ x)
+        ( associative-add-ℚ y (rational-ℚ⁺ ε) (rational-ℚ⁺ δ))
+        ( pr2 (H δ)))
+
+pseudometric-space-ℚ : Pseudometric-Space-WIP lzero lzero
+pr1 pseudometric-space-ℚ = ℚ
+pr2 pseudometric-space-ℚ =
+  neighborhood-prop-ℚ ,
+  is-reflexive-neighborhood-ℚ ,
+  is-symmetric-neighborhood-ℚ ,
+  is-triangular-neighborhood-ℚ ,
+  is-saturated-neighborhood-ℚ
+
+is-tight-pseudometric-space-ℚ :
+  is-tight-Pseudometric-Space-WIP pseudometric-space-ℚ
+is-tight-pseudometric-space-ℚ x y H =
+  antisymmetric-leq-ℚ
+    ( x)
+    ( y)
+    ( map-inv-equiv (equiv-leq-leq-add-positive-ℚ x y) (pr2 ∘ H))
+    ( map-inv-equiv (equiv-leq-leq-add-positive-ℚ y x) (pr1 ∘ H))
+
+is-extensional-pseudometric-space-ℚ :
+  is-extensional-Pseudometric-Space-WIP pseudometric-space-ℚ
+is-extensional-pseudometric-space-ℚ =
+  is-extensional-is-tight-Pseudometric-Space
+    pseudometric-space-ℚ
+    is-tight-pseudometric-space-ℚ
+```
+
+### The standard metric space of rational numbers
+
+```agda
+metric-space-ℚ : Metric-Space-WIP lzero lzero
+metric-space-ℚ =
+  make-Metric-Space-WIP
+    ℚ
+    neighborhood-prop-ℚ
+    is-reflexive-neighborhood-ℚ
+    is-symmetric-neighborhood-ℚ
+    is-triangular-neighborhood-ℚ
+    is-saturated-neighborhood-ℚ
+    is-extensional-pseudometric-space-ℚ
+```
+
+## Properties
+
+### Relationship to the distance on rational numbers
+
+```agda
+abstract
+  leq-dist-neighborhood-ℚ :
+    (ε : ℚ⁺) (p q : ℚ) →
+    neighborhood-ℚ ε p q →
+    leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε)
+  leq-dist-neighborhood-ℚ ε⁺@(ε , _) p q (H , K) =
+    leq-dist-leq-diff-ℚ
+      ( p)
+      ( q)
+      ( ε)
+      ( swap-right-diff-leq-ℚ p ε q (leq-transpose-right-add-ℚ p q ε K))
+      ( swap-right-diff-leq-ℚ q ε p (leq-transpose-right-add-ℚ q p ε H))
+
+  neighborhood-leq-dist-ℚ :
+    (ε : ℚ⁺) (p q : ℚ) →
+    leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) →
+    neighborhood-ℚ ε p q
+  neighborhood-leq-dist-ℚ ε⁺@(ε , _) p q |p-q|≤ε =
+    ( leq-transpose-left-diff-ℚ
+      ( q)
+      ( ε)
+      ( p)
+      ( swap-right-diff-leq-ℚ
+        ( q)
+        ( p)
+        ( ε)
+        ( transitive-leq-ℚ
+          ( q -ℚ p)
+          ( rational-dist-ℚ p q)
+          ( ε)
+          ( |p-q|≤ε)
+          ( leq-reversed-diff-dist-ℚ p q)))) ,
+    ( leq-transpose-left-diff-ℚ
+      ( p)
+      ( ε)
+      ( q)
+      ( swap-right-diff-leq-ℚ
+        ( p)
+        ( q)
+        ( ε)
+        ( transitive-leq-ℚ
+          ( p -ℚ q)
+          ( rational-dist-ℚ p q)
+          ( ε)
+          ( |p-q|≤ε)
+          ( leq-diff-dist-ℚ p q))))
+
+leq-dist-iff-neighborhood-ℚ :
+  (ε : ℚ⁺) (p q : ℚ) →
+  leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) ↔
+  neighborhood-ℚ ε p q
+pr1 (leq-dist-iff-neighborhood-ℚ ε p q) = neighborhood-leq-dist-ℚ ε p q
+pr2 (leq-dist-iff-neighborhood-ℚ ε p q) = leq-dist-neighborhood-ℚ ε p q
+```
+
+### Addition of rational numbers is an isometry
+
+```agda
+module _
+  (x u v : ℚ) (d : ℚ⁺)
+  where
+
+  -- preserves-lower-neighborhood-add-ℚ :
+  --   lower-neighborhood-ℚ d u v →
+  --   lower-neighborhood-ℚ d (x +ℚ u) (x +ℚ v)
+  -- preserves-lower-neighborhood-add-ℚ H =
+  --   inv-tr
+  --     ( leq-ℚ (x +ℚ v))
+  --     ( associative-add-ℚ x u (rational-ℚ⁺ d))
+  --     ( preserves-leq-right-add-ℚ
+  --       ( x)
+  --       ( v)
+  --       ( u +ℚ rational-ℚ⁺ d)
+  --       ( H))
+
+  -- reflects-lower-neighborhood-add-ℚ :
+  --   lower-neighborhood-ℚ d (x +ℚ u) (x +ℚ v) →
+  --   lower-neighborhood-ℚ d u v
+  -- reflects-lower-neighborhood-add-ℚ =
+  --   ( reflects-leq-right-add-ℚ x v (u +ℚ rational-ℚ⁺ d)) ∘
+  --   ( tr (leq-ℚ (x +ℚ v)) (associative-add-ℚ x u (rational-ℚ⁺ d)))
+```
+
+```agda
+module _
+  (x : ℚ)
+  where
+
+  -- is-isometry-add-ℚ :
+  --   is-isometry-Metric-Space-WIP
+  --     ( metric-space-ℚ)
+  --     ( metric-space-ℚ)
+  --     ( add-ℚ x)
+  -- is-isometry-add-ℚ d y z =
+  --   pair
+  --     ( map-product
+  --       ( preserves-lower-neighborhood-add-ℚ x y z d)
+  --       ( preserves-lower-neighborhood-add-ℚ x z y d))
+  --     ( map-product
+  --       ( reflects-lower-neighborhood-add-ℚ x y z d)
+  --       ( reflects-lower-neighborhood-add-ℚ x z y d))
+
+  -- is-isometry-add-ℚ' :
+  --   is-isometry-Metric-Space-WIP
+  --     ( metric-space-ℚ)
+  --     ( metric-space-ℚ)
+  --     ( add-ℚ' x)
+  -- is-isometry-add-ℚ' d y z =
+  --   binary-tr
+  --     ( λ u v → neighborhood-ℚ d y z ↔ neighborhood-ℚ d u v)
+  --     ( commutative-add-ℚ x y)
+  --     ( commutative-add-ℚ x z)
+  --     ( is-isometry-add-ℚ d y z)
+```
+
+### Multiplication of rational numbers is Lipschitz
+
+```agda
+module _
+  (x : ℚ)
+  where
+
+  -- abstract
+  --   is-lipschitz-constant-succ-abs-mul-ℚ :
+  --     is-lipschitz-constant-function-Metric-Space
+  --       ( metric-space-leq-ℚ)
+  --       ( metric-space-leq-ℚ)
+  --       ( mul-ℚ x)
+  --       ( positive-succ-ℚ⁰⁺ (abs-ℚ x))
+  --   is-lipschitz-constant-succ-abs-mul-ℚ d y z H =
+  --     neighborhood-leq-leq-dist-ℚ
+  --       ( positive-succ-ℚ⁰⁺ (abs-ℚ x) *ℚ⁺ d)
+  --       ( x *ℚ y)
+  --       ( x *ℚ z)
+  --       ( tr
+  --         ( λ q →
+  --           leq-ℚ
+  --             ( rational-ℚ⁰⁺ q)
+  --             ( rational-ℚ⁺ (positive-succ-ℚ⁰⁺ (abs-ℚ x) *ℚ⁺ d)))
+  --         ( left-distributive-abs-mul-dist-ℚ x y z)
+  --         ( transitive-leq-ℚ
+  --           ( rational-ℚ⁰⁺ (abs-ℚ x *ℚ⁰⁺ dist-ℚ y z))
+  --           ( (succ-ℚ (rational-abs-ℚ x)) *ℚ (rational-dist-ℚ y z))
+  --           ( rational-ℚ⁺ (positive-succ-ℚ⁰⁺ (abs-ℚ x) *ℚ⁺ d))
+  --           ( preserves-leq-left-mul-ℚ⁺
+  --             ( positive-succ-ℚ⁰⁺ (abs-ℚ x))
+  --             ( rational-dist-ℚ y z)
+  --             ( rational-ℚ⁺ d)
+  --             ( leq-dist-neighborhood-leq-ℚ d y z H))
+  --           ( preserves-leq-right-mul-ℚ⁰⁺
+  --             ( dist-ℚ y z)
+  --             ( rational-abs-ℚ x)
+  --             ( succ-ℚ (rational-abs-ℚ x))
+  --             ( succ-leq-ℚ (rational-abs-ℚ x)))))
+
+  --   lipschitz-constant-succ-abs-mul-ℚ :
+  --     lipschitz-constant-function-Metric-Space
+  --       ( metric-space-leq-ℚ)
+  --       ( metric-space-leq-ℚ)
+  --       ( mul-ℚ x)
+  --   lipschitz-constant-succ-abs-mul-ℚ =
+  --     ( positive-succ-ℚ⁰⁺ (abs-ℚ x)) ,
+  --     ( is-lipschitz-constant-succ-abs-mul-ℚ)
+
+  --   is-lipschitz-left-mul-ℚ :
+  --     ( is-lipschitz-function-Metric-Space
+  --       ( metric-space-leq-ℚ)
+  --       ( metric-space-leq-ℚ)
+  --       ( mul-ℚ x))
+  --   is-lipschitz-left-mul-ℚ =
+  --     unit-trunc-Prop lipschitz-constant-succ-abs-mul-ℚ
+
+  --   is-lipschitz-right-mul-ℚ :
+  --     ( is-lipschitz-function-Metric-Space
+  --       ( metric-space-leq-ℚ)
+  --       ( metric-space-leq-ℚ)
+  --       ( mul-ℚ' x))
+  --   is-lipschitz-right-mul-ℚ =
+  --     is-lipschitz-htpy-function-Metric-Space
+  --       ( metric-space-leq-ℚ)
+  --       ( metric-space-leq-ℚ)
+  --       ( mul-ℚ x)
+  --       ( mul-ℚ' x)
+  --       ( commutative-mul-ℚ x)
+  --       ( is-lipschitz-left-mul-ℚ)
+```
+
+### The convergent Cauchy approximation of the canonical inclusion of positive rational numbers into the rational numbers
+
+```agda
+-- is-cauchy-approximation-rational-ℚ⁺ :
+--   is-cauchy-approximation-Metric-Space-WIP
+--     metric-space-ℚ
+--     rational-ℚ⁺
+-- is-cauchy-approximation-rational-ℚ⁺ ε δ =
+--   ( leq-le-ℚ
+--     { rational-ℚ⁺ δ}
+--     { rational-ℚ⁺ ε +ℚ (rational-ℚ⁺ (ε +ℚ⁺ δ))}
+--     ( transitive-le-ℚ
+--       ( rational-ℚ⁺ δ)
+--       ( rational-ℚ⁺ (ε +ℚ⁺ δ))
+--       ( rational-ℚ⁺ ε +ℚ (rational-ℚ⁺ (ε +ℚ⁺ δ)))
+--       ( le-right-add-ℚ⁺
+--         ( ε)
+--         ( ε +ℚ⁺ δ))
+--       ( le-right-add-ℚ⁺ ε δ))) ,
+--   ( leq-le-ℚ
+--     { rational-ℚ⁺ ε}
+--     { rational-ℚ⁺ δ +ℚ (rational-ℚ⁺ (ε +ℚ⁺ δ))}
+--     ( transitive-le-ℚ
+--       ( rational-ℚ⁺ ε)
+--       ( rational-ℚ⁺ (ε +ℚ⁺ δ))
+--       ( rational-ℚ⁺ δ +ℚ (rational-ℚ⁺ (ε +ℚ⁺ δ)))
+--       ( le-right-add-ℚ⁺
+--         ( δ)
+--         ( ε +ℚ⁺ δ))
+--       ( le-left-add-ℚ⁺ ε δ)))
+
+-- cauchy-approximation-rational-ℚ⁺ :
+--   cauchy-approximation-Metric-Space-WIP metric-space-ℚ
+-- cauchy-approximation-rational-ℚ⁺ =
+--   rational-ℚ⁺ , is-cauchy-approximation-rational-ℚ⁺
+
+-- is-zero-limit-rational-ℚ⁺ :
+--   is-limit-cauchy-approximation-Metric-Space-WIP
+--     ( metric-space-ℚ)
+--     ( cauchy-approximation-rational-ℚ⁺)
+--     ( zero-ℚ)
+-- is-zero-limit-rational-ℚ⁺ ε δ =
+--   ( leq-le-ℚ
+--     { zero-ℚ}
+--     { rational-ℚ⁺ (ε +ℚ⁺ (ε +ℚ⁺ δ))}
+--     ( le-zero-is-positive-ℚ
+--       ( rational-ℚ⁺ (ε +ℚ⁺ (ε +ℚ⁺ δ)))
+--       ( is-positive-rational-ℚ⁺
+--         (ε +ℚ⁺ (ε +ℚ⁺ δ))))) ,
+--   ( leq-le-ℚ
+--     { rational-ℚ⁺ ε}
+--     { zero-ℚ +ℚ rational-ℚ⁺ (ε +ℚ⁺ δ)}
+--     ( inv-tr
+--       ( le-ℚ (rational-ℚ⁺ ε))
+--       ( left-unit-law-add-ℚ (rational-ℚ⁺ (ε +ℚ⁺ δ)))
+--       ( le-left-add-ℚ⁺ ε δ)))
+
+-- convergent-rational-ℚ⁺ :
+--   convergent-cauchy-approximation-Metric-Space-WIP metric-space-ℚ
+-- convergent-rational-ℚ⁺ =
+--   cauchy-approximation-rational-ℚ⁺ ,
+--   zero-ℚ ,
+--   is-zero-limit-rational-ℚ⁺
+```
diff --git a/src/metric-spaces/metric-spaces-WIP.lagda.md b/src/metric-spaces/metric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..e56db06a47
--- /dev/null
+++ b/src/metric-spaces/metric-spaces-WIP.lagda.md
@@ -0,0 +1,411 @@
+# Metric spaces (WIP)
+
+```agda
+module metric-spaces.metric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.binary-relations
+open import foundation.dependent-pair-types
+open import foundation.equivalence-relations
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import metric-spaces.extensional-pseudometric-spaces-WIP
+open import metric-spaces.preimage-rational-neighborhoods
+open import metric-spaces.pseudometric-spaces-WIP
+open import metric-spaces.rational-neighborhoods
+open import metric-spaces.reflexive-rational-neighborhoods
+open import metric-spaces.saturated-rational-neighborhoods
+open import metric-spaces.similarity-of-elements-pseudometric-spaces
+open import metric-spaces.symmetric-rational-neighborhoods
+open import metric-spaces.triangular-rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "metric space" Agda=Metric-Space-WIP WD="metric space" WDID=Q180953}}
+is a type [structured](foundation.structure.md) with a concept of distance on
+its elements.
+
+Since we operate in a constructive setting, the concept of distance is captured
+by considering upper bounds on the distance between points, rather than by a
+distance function as in the classical approach. Thus, a metric space `A` is
+defined by a family of _neighborhood_
+[relations](foundation.binary-relations.md) on it indexed by the
+[positive rational numbers](elementary-number-theory.positive-rational-numbers.md)
+`ℚ⁺`, a
+[rational neighborhood relation](metric-spaces.rational-neighborhoods.md):
+
+```text
+  N : ℚ⁺ → A → A → Prop l
+```
+
+that satisfies certain axioms. Constructing a proof of `N d x y` amounts to
+saying that _`d` is an upper bound on the distance from `x` to `y`_.
+
+The neighborhood relation on a metric space must satisfy the following axioms:
+
+- [**Reflexivity.**](metric-spaces.reflexive-rational-neighborhoods.md) Every
+  positive rational `d` is an upper bound on the distance from `x` to itself.
+- [**Symmetry.**](metric-spaces.symmetric-rational-neighborhoods.md) Any upper
+  bound on the distance from `x` to `y` is an upper bound on the distance from
+  `y` to `x`.
+- [**Triangularity.**](metric-spaces.triangular-rational-neighborhoods.md) If
+  `d` is an upper bound on the distance from `x` to `y`, and `d'` is an upper
+  bound on the distance from `y` to `z`, then `d + d'` is an upper bound on the
+  distance from `x` to `z`.
+- [**Saturation.**](metric-spaces.saturated-rational-neighborhoods.md): any
+  neighborhood `N d x y` contains the intersection of all `N d' x y` for
+  `d < d'`.
+
+This gives `A` the structure of a
+[**pseudometric space**](metric-spaces.pseudometric-spaces-WIP.md); finally, we
+ask that our metric spaces are
+[**extensional**](metric-spaces.extensional-pseudometric-spaces-WIP.md):
+[similar](metric-spaces.similarity-of-elements-pseudometric-spaces.md) elements
+are [equal](foundation-core.identity-types.md):
+
+- If every positive rational `d` is an upper bound on the distance from `x` to
+  `y`, then `x ＝ y`.
+
+Similarity of elements in a metric space characterizes their equality so any
+metric space is a [set](foundation.sets.md).
+
+NB: When working with actual distance functions, the _saturation_ condition
+always holds, defining `N d x y` as `dist(x , y) ≤ d`. Since we're working with
+_upper bounds on distances_, we add this axiom to ensure that the subsets of
+upper bounds on distances between elements is closed on the left.
+
+## Definitions
+
+### Metric Structures on a type
+
+```agda
+module _
+  {l1 : Level} (A : UU l1) {l2 : Level}
+  (B : Rational-Neighborhood-Relation l2 A)
+  where
+
+  is-metric-prop-Rational-Neighborhood-Relation : Prop (l1 ⊔ l2)
+  is-metric-prop-Rational-Neighborhood-Relation =
+    Σ-Prop
+      ( is-pseudometric-prop-Rational-Neighborhood-Relation A B)
+      ( λ H →
+        is-extensional-prop-Pseudometric-Space-WIP (A , B , H))
+
+  is-metric-Rational-Neighborhood-Relation : UU (l1 ⊔ l2)
+  is-metric-Rational-Neighborhood-Relation =
+    type-Prop is-metric-prop-Rational-Neighborhood-Relation
+
+  is-prop-is-metric-Rational-Neighborhood-Relation :
+    is-prop is-metric-Rational-Neighborhood-Relation
+  is-prop-is-metric-Rational-Neighborhood-Relation =
+    is-prop-type-Prop (is-metric-prop-Rational-Neighborhood-Relation)
+
+Metric-Structure-WIP :
+  {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2)
+Metric-Structure-WIP l2 A =
+  type-subtype (is-metric-prop-Rational-Neighborhood-Relation A {l2})
+```
+
+### The type of metric spaces
+
+```agda
+Metric-Space-WIP : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Metric-Space-WIP l1 l2 =
+  Σ (UU l1) (Metric-Structure-WIP l2)
+
+make-Metric-Space-WIP :
+  { l1 l2 : Level} →
+  ( A : UU l1) →
+  ( B : Rational-Neighborhood-Relation l2 A) →
+  ( refl-B : is-reflexive-Rational-Neighborhood-Relation B) →
+  ( symmetric-B : is-symmetric-Rational-Neighborhood-Relation B) →
+  ( triangular-B : is-triangular-Rational-Neighborhood-Relation B) →
+  ( saturated-B : is-saturated-Rational-Neighborhood-Relation B) →
+  ( extensional-B :
+    is-extensional-Pseudometric-Space-WIP
+      (A , B , refl-B , symmetric-B , triangular-B , saturated-B)) →
+  Metric-Space-WIP l1 l2
+make-Metric-Space-WIP
+  A B refl-B symmetric-B triangular-B saturated-B extensional-B =
+  ( A) ,
+  ( ( B) ,
+    ( refl-B , symmetric-B , triangular-B , saturated-B) ,
+    ( extensional-B))
+
+module _
+  {l1 l2 : Level} (M : Metric-Space-WIP l1 l2)
+  where
+
+  type-Metric-Space-WIP : UU l1
+  type-Metric-Space-WIP =
+    pr1 M
+
+  structure-Metric-Space-WIP : Metric-Structure-WIP l2 type-Metric-Space-WIP
+  structure-Metric-Space-WIP = pr2 M
+
+  pseudometric-Metric-Space-WIP : Pseudometric-Space-WIP l1 l2
+  pseudometric-Metric-Space-WIP =
+    ( type-Metric-Space-WIP) ,
+    ( pr1 structure-Metric-Space-WIP) ,
+    ( pr1 (pr2 structure-Metric-Space-WIP))
+
+  is-extensional-pseudometric-Metric-Space-WIP :
+    is-extensional-Pseudometric-Space-WIP pseudometric-Metric-Space-WIP
+  is-extensional-pseudometric-Metric-Space-WIP =
+    pr2 (pr2 structure-Metric-Space-WIP)
+
+  pseudometric-structure-Metric-Space-WIP :
+    Pseudometric-Structure l2 type-Metric-Space-WIP
+  pseudometric-structure-Metric-Space-WIP =
+    structure-Pseudometric-Space-WIP pseudometric-Metric-Space-WIP
+
+  neighborhood-prop-Metric-Space-WIP :
+    ℚ⁺ → Relation-Prop l2 type-Metric-Space-WIP
+  neighborhood-prop-Metric-Space-WIP =
+    neighborhood-prop-Pseudometric-Space-WIP pseudometric-Metric-Space-WIP
+
+  neighborhood-Metric-Space-WIP : ℚ⁺ → Relation l2 type-Metric-Space-WIP
+  neighborhood-Metric-Space-WIP =
+    neighborhood-Pseudometric-Space-WIP pseudometric-Metric-Space-WIP
+
+  is-prop-neighborhood-Metric-Space-WIP :
+    (d : ℚ⁺) (x y : type-Metric-Space-WIP) →
+    is-prop (neighborhood-Metric-Space-WIP d x y)
+  is-prop-neighborhood-Metric-Space-WIP =
+    is-prop-neighborhood-Pseudometric-Space-WIP pseudometric-Metric-Space-WIP
+
+  is-upper-bound-dist-prop-Metric-Space-WIP :
+    (x y : type-Metric-Space-WIP) → ℚ⁺ → Prop l2
+  is-upper-bound-dist-prop-Metric-Space-WIP x y d =
+    neighborhood-prop-Metric-Space-WIP d x y
+
+  is-upper-bound-dist-Metric-Space-WIP :
+    (x y : type-Metric-Space-WIP) → ℚ⁺ → UU l2
+  is-upper-bound-dist-Metric-Space-WIP x y d =
+    neighborhood-Metric-Space-WIP d x y
+
+  is-prop-is-upper-bound-dist-Metric-Space-WIP :
+    (x y : type-Metric-Space-WIP) (d : ℚ⁺) →
+    is-prop (is-upper-bound-dist-Metric-Space-WIP x y d)
+  is-prop-is-upper-bound-dist-Metric-Space-WIP x y d =
+    is-prop-neighborhood-Metric-Space-WIP d x y
+
+  is-pseudometric-neighborhood-Metric-Space-WIP :
+    is-pseudometric-Rational-Neighborhood-Relation
+      type-Metric-Space-WIP
+      neighborhood-prop-Metric-Space-WIP
+  is-pseudometric-neighborhood-Metric-Space-WIP =
+    is-pseudometric-neighborhood-Pseudometric-Space-WIP
+      pseudometric-Metric-Space-WIP
+
+  refl-neighborhood-Metric-Space-WIP :
+    (d : ℚ⁺) (x : type-Metric-Space-WIP) →
+    neighborhood-Metric-Space-WIP d x x
+  refl-neighborhood-Metric-Space-WIP =
+    refl-neighborhood-Pseudometric-Space-WIP pseudometric-Metric-Space-WIP
+
+  symmetric-neighborhood-Metric-Space-WIP :
+    (d : ℚ⁺) (x y : type-Metric-Space-WIP) →
+    neighborhood-Metric-Space-WIP d x y →
+    neighborhood-Metric-Space-WIP d y x
+  symmetric-neighborhood-Metric-Space-WIP =
+    symmetric-neighborhood-Pseudometric-Space-WIP pseudometric-Metric-Space-WIP
+
+  inv-neighborhood-Metric-Space-WIP :
+    {d : ℚ⁺} {x y : type-Metric-Space-WIP} →
+    neighborhood-Metric-Space-WIP d x y →
+    neighborhood-Metric-Space-WIP d y x
+  inv-neighborhood-Metric-Space-WIP =
+    inv-neighborhood-Pseudometric-Space-WIP pseudometric-Metric-Space-WIP
+
+  triangular-neighborhood-Metric-Space-WIP :
+    (x y z : type-Metric-Space-WIP) (d₁ d₂ : ℚ⁺) →
+    neighborhood-Metric-Space-WIP d₂ y z →
+    neighborhood-Metric-Space-WIP d₁ x y →
+    neighborhood-Metric-Space-WIP (d₁ +ℚ⁺ d₂) x z
+  triangular-neighborhood-Metric-Space-WIP =
+    triangular-neighborhood-Pseudometric-Space-WIP pseudometric-Metric-Space-WIP
+
+  monotonic-neighborhood-Metric-Space-WIP :
+    (x y : type-Metric-Space-WIP) (d₁ d₂ : ℚ⁺) →
+    le-ℚ⁺ d₁ d₂ →
+    neighborhood-Metric-Space-WIP d₁ x y →
+    neighborhood-Metric-Space-WIP d₂ x y
+  monotonic-neighborhood-Metric-Space-WIP =
+    monotonic-neighborhood-Pseudometric-Space-WIP pseudometric-Metric-Space-WIP
+
+  saturated-neighborhood-Metric-Space-WIP :
+    (ε : ℚ⁺) (x y : type-Metric-Space-WIP) →
+    ((δ : ℚ⁺) → neighborhood-Metric-Space-WIP (ε +ℚ⁺ δ) x y) →
+    neighborhood-Metric-Space-WIP ε x y
+  saturated-neighborhood-Metric-Space-WIP =
+    saturated-neighborhood-Pseudometric-Space-WIP pseudometric-Metric-Space-WIP
+```
+
+### Similarity of elements in a metric space
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  where
+
+  sim-prop-Metric-Space-WIP : Relation-Prop l2 (type-Metric-Space-WIP A)
+  sim-prop-Metric-Space-WIP =
+    sim-prop-Pseudometric-Space-WIP (pseudometric-Metric-Space-WIP A)
+
+  sim-Metric-Space-WIP : Relation l2 (type-Metric-Space-WIP A)
+  sim-Metric-Space-WIP =
+    sim-Pseudometric-Space-WIP (pseudometric-Metric-Space-WIP A)
+
+  is-prop-sim-Metric-Space-WIP :
+    (x y : type-Metric-Space-WIP A) →
+    is-prop (sim-Metric-Space-WIP x y)
+  is-prop-sim-Metric-Space-WIP =
+    is-prop-sim-Pseudometric-Space-WIP (pseudometric-Metric-Space-WIP A)
+
+  refl-sim-Metric-Space-WIP :
+    (x : type-Metric-Space-WIP A) →
+    sim-Metric-Space-WIP x x
+  refl-sim-Metric-Space-WIP =
+    refl-sim-Pseudometric-Space-WIP (pseudometric-Metric-Space-WIP A)
+
+  sim-eq-Metric-Space-WIP :
+    (x y : type-Metric-Space-WIP A) →
+    x ＝ y →
+    sim-Metric-Space-WIP x y
+  sim-eq-Metric-Space-WIP =
+    sim-eq-Pseudometric-Space-WIP (pseudometric-Metric-Space-WIP A)
+
+  symmetric-sim-Metric-Space-WIP :
+    (x y : type-Metric-Space-WIP A) →
+    sim-Metric-Space-WIP x y →
+    sim-Metric-Space-WIP y x
+  symmetric-sim-Metric-Space-WIP =
+    symmetric-sim-Pseudometric-Space-WIP (pseudometric-Metric-Space-WIP A)
+
+  inv-sim-Metric-Space-WIP :
+    {x y : type-Metric-Space-WIP A} →
+    sim-Metric-Space-WIP x y →
+    sim-Metric-Space-WIP y x
+  inv-sim-Metric-Space-WIP {x} {y} =
+    inv-sim-Pseudometric-Space-WIP (pseudometric-Metric-Space-WIP A)
+
+  transitive-sim-Metric-Space-WIP :
+    (x y z : type-Metric-Space-WIP A) →
+    sim-Metric-Space-WIP y z →
+    sim-Metric-Space-WIP x y →
+    sim-Metric-Space-WIP x z
+  transitive-sim-Metric-Space-WIP =
+    transitive-sim-Pseudometric-Space-WIP (pseudometric-Metric-Space-WIP A)
+
+  equivalence-sim-Metric-Space-WIP :
+    equivalence-relation l2 (type-Metric-Space-WIP A)
+  equivalence-sim-Metric-Space-WIP =
+    equivalence-sim-Pseudometric-Space-WIP (pseudometric-Metric-Space-WIP A)
+```
+
+## Properties
+
+### The carrier type of a metric space is a set
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  where
+
+  is-set-type-Metric-Space-WIP : is-set (type-Metric-Space-WIP A)
+  is-set-type-Metric-Space-WIP =
+    is-set-type-is-extensional-Pseudometric-Space-WIP
+      ( pseudometric-Metric-Space-WIP A)
+      ( is-extensional-pseudometric-Metric-Space-WIP A)
+
+  set-Metric-Space-WIP : Set l1
+  set-Metric-Space-WIP =
+    (type-Metric-Space-WIP A , is-set-type-Metric-Space-WIP)
+```
+
+### The set of functions between metric spaces
+
+```agda
+module _
+  {lx lx' ly ly' : Level}
+  (X : Metric-Space-WIP lx lx') (Y : Metric-Space-WIP ly ly')
+  where
+
+  set-function-Metric-Space-WIP : Set (lx ⊔ ly)
+  set-function-Metric-Space-WIP =
+    hom-set-Set (set-Metric-Space-WIP X) (set-Metric-Space-WIP Y)
+
+  type-function-Metric-Space-WIP : UU (lx ⊔ ly)
+  type-function-Metric-Space-WIP =
+    type-Metric-Space-WIP X → type-Metric-Space-WIP Y
+```
+
+### Similarity of elements in a metric space is equivalent to equality
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  where
+
+  equiv-sim-eq-Metric-Space-WIP :
+    (x y : type-Metric-Space-WIP A) →
+    (x ＝ y) ≃ sim-Metric-Space-WIP A x y
+  equiv-sim-eq-Metric-Space-WIP =
+    equiv-sim-eq-is-extensional-Pseudometric-Space-WIP
+      ( pseudometric-Metric-Space-WIP A)
+      ( is-extensional-pseudometric-Metric-Space-WIP A)
+
+  eq-sim-Metric-Space-WIP :
+    (x y : type-Metric-Space-WIP A) →
+    sim-Metric-Space-WIP A x y →
+    x ＝ y
+  eq-sim-Metric-Space-WIP x y =
+    map-inv-equiv (equiv-sim-eq-Metric-Space-WIP x y)
+```
+
+### Characterization of the transport of metric structures along equalities
+
+```agda
+equiv-Eq-tr-Metric-Structure :
+  {l1 l2 : Level} (A B : UU l1) →
+  (P : Metric-Structure-WIP l2 A) →
+  (Q : Metric-Structure-WIP l2 B) →
+  (e : A ＝ B) →
+  (tr (Metric-Structure-WIP l2) e P ＝ Q) ≃
+  (Eq-Rational-Neighborhood-Relation
+    ( pr1 P)
+    ( preimage-Rational-Neighborhood-Relation (map-eq e) (pr1 Q)))
+equiv-Eq-tr-Metric-Structure A .A P Q refl =
+  ( equiv-Eq-eq-Rational-Neighborhood-Relation (pr1 P) (pr1 Q)) ∘e
+  ( extensionality-type-subtype'
+    ( is-metric-prop-Rational-Neighborhood-Relation A)
+    ( P)
+    ( Q))
+```
+
+## External links
+
+- [`MetricSpaces.Type`](https://www.cs.bham.ac.uk/~mhe/TypeTopology/MetricSpaces.Type.html)
+  at TypeTopology
+- [metric space](https://ncatlab.org/nlab/show/metric+space) at $n$Lab
+- [Metric spaces](https://en.wikipedia.org/wiki/Metric_space) at Wikipedia
diff --git a/src/metric-spaces/monotonic-rational-neighborhoods.lagda.md b/src/metric-spaces/monotonic-rational-neighborhoods.lagda.md
new file mode 100644
index 0000000000..ab7117e855
--- /dev/null
+++ b/src/metric-spaces/monotonic-rational-neighborhoods.lagda.md
@@ -0,0 +1,62 @@
+# Monotonic rational neighborhoods on types
+
+```agda
+module metric-spaces.monotonic-rational-neighborhoods where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import metric-spaces.rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+A [rational neighborhood relation](metric-spaces.rational-neighborhoods.md) is
+{{#concept "monotonic" Disambiguation="rational neighborhood relation" Agda=is-monotonic-Rational-Neighborhood-Relation}}
+if any `d₁`-neighborhoods are `d₂`-neighborhoods for `d₁ < d₂`.
+
+## Definitions
+
+### The property of being a monotonic rational neighborhood relation
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (B : Rational-Neighborhood-Relation l2 A)
+  where
+
+  is-monotonic-prop-Rational-Neighborhood-Relation : Prop (l1 ⊔ l2)
+  is-monotonic-prop-Rational-Neighborhood-Relation =
+    Π-Prop
+      ( A)
+      ( λ x →
+        ( Π-Prop
+          ( A)
+          ( λ y →
+            ( Π-Prop
+              ( ℚ⁺)
+              ( λ d₁ →
+                ( Π-Prop
+                  ( ℚ⁺)
+                  ( λ d₂ →
+                    ( Π-Prop
+                      ( le-ℚ⁺ d₁ d₂)
+                      ( λ H →
+                        hom-Prop (B d₁ x y) (B d₂ x y))))))))))
+
+  is-monotonic-Rational-Neighborhood-Relation : UU (l1 ⊔ l2)
+  is-monotonic-Rational-Neighborhood-Relation =
+    type-Prop is-monotonic-prop-Rational-Neighborhood-Relation
+
+  is-prop-is-monotonic-Rational-Neighborhood-Relation :
+    is-prop is-monotonic-Rational-Neighborhood-Relation
+  is-prop-is-monotonic-Rational-Neighborhood-Relation =
+    is-prop-type-Prop is-monotonic-prop-Rational-Neighborhood-Relation
+```
diff --git a/src/metric-spaces/ordering-rational-neighborhoods.lagda.md b/src/metric-spaces/ordering-rational-neighborhoods.lagda.md
new file mode 100644
index 0000000000..77213c10b8
--- /dev/null
+++ b/src/metric-spaces/ordering-rational-neighborhoods.lagda.md
@@ -0,0 +1,145 @@
+# The poset of rational neighborhood relations on a type
+
+```agda
+module metric-spaces.ordering-rational-neighborhoods where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+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.universe-levels
+
+open import metric-spaces.rational-neighborhoods
+
+open import order-theory.posets
+open import order-theory.preorders
+```
+
+</details>
+
+## Idea
+
+A [rational neighborhood relation](metric-spaces.rational-neighborhoods.md) `U`
+on a type `A` is
+{{#concept "finer" Disambiguation="rational neighborhood relation on a type" Agda=leq-Rational-Neighborhood-Relation}}
+than another rational neighborhood relation `V` if `(U d)`-neighborhoods are
+`(V d)`-neighborhoods for any
+[positive rational](elementary-number-theory.positive-rational-numbers.md) `d`,
+i.e., if any upper bound on the distance between two points in `U` also bounds
+their distance in `V`. This is a [partial order](order-theory.posets.md) on the
+type of rational neighborhood relations on `A`.
+
+## Definitions
+
+```agda
+module _
+  {l1 l2 l2' : Level} {A : UU l1}
+  (U : Rational-Neighborhood-Relation l2 A)
+  (V : Rational-Neighborhood-Relation l2' A)
+  where
+
+  leq-prop-Rational-Neighborhood-Relation : Prop (l1 ⊔ l2 ⊔ l2')
+  leq-prop-Rational-Neighborhood-Relation =
+    Π-Prop
+      ( ℚ⁺)
+      ( λ d →
+        Π-Prop
+          ( A)
+          ( λ x →
+            Π-Prop
+              ( A)
+              ( λ y → hom-Prop (U d x y) (V d x y))))
+
+  leq-Rational-Neighborhood-Relation : UU (l1 ⊔ l2 ⊔ l2')
+  leq-Rational-Neighborhood-Relation =
+    type-Prop leq-prop-Rational-Neighborhood-Relation
+
+  is-prop-leq-Rational-Neighborhood-Relation :
+    is-prop leq-Rational-Neighborhood-Relation
+  is-prop-leq-Rational-Neighborhood-Relation =
+    is-prop-type-Prop leq-prop-Rational-Neighborhood-Relation
+```
+
+## Properties
+
+### The ordering on rational neighborhood relations is reflexive
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (U : Rational-Neighborhood-Relation l2 A)
+  where
+
+  refl-leq-Rational-Neighborhood-Relation :
+    leq-Rational-Neighborhood-Relation U U
+  refl-leq-Rational-Neighborhood-Relation d x y H = H
+
+  leq-eq-Rational-Neighborhood-Relation :
+    (V : Rational-Neighborhood-Relation l2 A) →
+    (U ＝ V) →
+    leq-Rational-Neighborhood-Relation U V
+  leq-eq-Rational-Neighborhood-Relation .U refl =
+    refl-leq-Rational-Neighborhood-Relation
+```
+
+### The ordering on rational neighborhood relations is transitive
+
+```agda
+module _
+  {l lu lv lw : Level} {A : UU l}
+  (U : Rational-Neighborhood-Relation lu A)
+  (V : Rational-Neighborhood-Relation lv A)
+  (W : Rational-Neighborhood-Relation lw A)
+  where
+
+  transitive-leq-Rational-Neighborhood-Relation :
+    leq-Rational-Neighborhood-Relation V W →
+    leq-Rational-Neighborhood-Relation U V →
+    leq-Rational-Neighborhood-Relation U W
+  transitive-leq-Rational-Neighborhood-Relation H K d x y = H d x y ∘ K d x y
+```
+
+### The ordering on rational neighborhood relations is antisymmetric
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (U V : Rational-Neighborhood-Relation l2 A)
+  where
+
+  antisymmetric-leq-Rational-Neighborhood-Relation :
+    leq-Rational-Neighborhood-Relation U V →
+    leq-Rational-Neighborhood-Relation V U →
+    U ＝ V
+  antisymmetric-leq-Rational-Neighborhood-Relation I J =
+    eq-Eq-Rational-Neighborhood-Relation
+      ( U)
+      ( V)
+      ( λ d x y → (I d x y , J d x y))
+```
+
+### The poset of rational neighborhood relations on a type
+
+```agda
+module _
+  {l1 l2 : Level} (A : UU l1)
+  where
+
+  preorder-Rational-Neighborhood-Relation : Preorder (l1 ⊔ lsuc l2) (l1 ⊔ l2)
+  pr1 preorder-Rational-Neighborhood-Relation =
+    Rational-Neighborhood-Relation l2 A
+  pr2 preorder-Rational-Neighborhood-Relation =
+    leq-prop-Rational-Neighborhood-Relation ,
+    refl-leq-Rational-Neighborhood-Relation ,
+    transitive-leq-Rational-Neighborhood-Relation
+
+  poset-Rational-Neighborhood-Relation : Poset (l1 ⊔ lsuc l2) (l1 ⊔ l2)
+  poset-Rational-Neighborhood-Relation =
+    preorder-Rational-Neighborhood-Relation ,
+    antisymmetric-leq-Rational-Neighborhood-Relation
+```
diff --git a/src/metric-spaces/preimage-rational-neighborhoods.lagda.md b/src/metric-spaces/preimage-rational-neighborhoods.lagda.md
new file mode 100644
index 0000000000..5958af3217
--- /dev/null
+++ b/src/metric-spaces/preimage-rational-neighborhoods.lagda.md
@@ -0,0 +1,139 @@
+# Preimage of rational neighborhood relations along maps
+
+```agda
+module metric-spaces.preimage-rational-neighborhoods where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.injective-maps
+open import foundation.universe-levels
+
+open import metric-spaces.monotonic-rational-neighborhoods
+open import metric-spaces.rational-neighborhoods
+open import metric-spaces.reflexive-rational-neighborhoods
+open import metric-spaces.symmetric-rational-neighborhoods
+open import metric-spaces.triangular-rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+Any [rational neighborhood relation](metric-spaces.rational-neighborhoods.md)
+`U` on a type `B` and map `f : A → B` defines a rational neighborhood relation
+on `A` where `x y : A` are `d`-neighbors if `f x` and `f y` are `d`-neighbors in
+`U`. This is the
+{{#concept "preimage" Disambiguation="rational neighborhood relation" Agda=preimage-Rational-Neighborhood-Relation}}
+of `U` by `f`.
+
+## Definitions
+
+### The induced rational neighborhood relation on the preimage of a map
+
+```agda
+module _
+  {l1 l1' l2 : Level} {A : UU l1} {B : UU l1'} (f : A → B)
+  (V : Rational-Neighborhood-Relation l2 B)
+  where
+
+  preimage-Rational-Neighborhood-Relation : Rational-Neighborhood-Relation l2 A
+  preimage-Rational-Neighborhood-Relation d x y = V d (f x) (f y)
+```
+
+## Properties
+
+### The preimage of a reflexive rational neighborhood relation is reflexive
+
+```agda
+module _
+  {l1 l1' l2 : Level} {A : UU l1} {B : UU l1'} (f : A → B)
+  (V : Rational-Neighborhood-Relation l2 B)
+  (R : is-reflexive-Rational-Neighborhood-Relation V)
+  where
+
+  preserves-reflexive-preimage-Rational-Neighborhood-Relation :
+    is-reflexive-Rational-Neighborhood-Relation
+      (preimage-Rational-Neighborhood-Relation f V)
+  preserves-reflexive-preimage-Rational-Neighborhood-Relation d x = R d (f x)
+```
+
+### The preimage of a symmetric rational neighborhood relation is symmetric
+
+```agda
+module _
+  {l1 l1' l2 : Level} {A : UU l1} {B : UU l1'} (f : A → B)
+  (V : Rational-Neighborhood-Relation l2 B)
+  (S : is-symmetric-Rational-Neighborhood-Relation V)
+  where
+
+  preserves-symmetric-preimage-Rational-Neighborhood-Relation :
+    is-symmetric-Rational-Neighborhood-Relation
+      (preimage-Rational-Neighborhood-Relation f V)
+  preserves-symmetric-preimage-Rational-Neighborhood-Relation d x y =
+    S d (f x) (f y)
+```
+
+### The preimage of a monotonic rational neighborhood relation is monotonic
+
+```agda
+module _
+  {l1 l1' l2 : Level} {A : UU l1} {B : UU l1'} (f : A → B)
+  (V : Rational-Neighborhood-Relation l2 B)
+  (I : is-monotonic-Rational-Neighborhood-Relation V)
+  where
+
+  preserves-monotonic-preimage-Rational-Neighborhood-Relation :
+    is-monotonic-Rational-Neighborhood-Relation
+      (preimage-Rational-Neighborhood-Relation f V)
+  preserves-monotonic-preimage-Rational-Neighborhood-Relation x y =
+    I (f x) (f y)
+```
+
+### The preimage of a triangular rational neighborhood relation is triangular
+
+```agda
+module _
+  {l1 l1' l2 : Level} {A : UU l1} {B : UU l1'} (f : A → B)
+  (V : Rational-Neighborhood-Relation l2 B)
+  (T : is-triangular-Rational-Neighborhood-Relation V)
+  where
+
+  preserves-triangular-preimage-Rational-Neighborhood-Relation :
+    is-triangular-Rational-Neighborhood-Relation
+      (preimage-Rational-Neighborhood-Relation f V)
+  preserves-triangular-preimage-Rational-Neighborhood-Relation x y z =
+    T (f x) (f y) (f z)
+```
+
+### The preimage along the identity is the identity
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (U : Rational-Neighborhood-Relation l2 A)
+  where
+
+  eq-preimage-id-Rational-Neighborhood-Relation :
+    preimage-Rational-Neighborhood-Relation id U ＝ U
+  eq-preimage-id-Rational-Neighborhood-Relation = refl
+```
+
+### The preimage of rational neighborhood relations is contravariant
+
+```agda
+module _
+  {la lb lc l : Level} {A : UU la} {B : UU lb} {C : UU lc}
+  (g : B → C) (f : A → B) (W : Rational-Neighborhood-Relation l C)
+  where
+
+  eq-preimage-comp-Rational-Neighborhood-Relation :
+    ( preimage-Rational-Neighborhood-Relation f
+      (preimage-Rational-Neighborhood-Relation g W)) ＝
+    ( preimage-Rational-Neighborhood-Relation (g ∘ f) W)
+  eq-preimage-comp-Rational-Neighborhood-Relation = refl
+```
diff --git a/src/metric-spaces/pseudometric-spaces-WIP.lagda.md b/src/metric-spaces/pseudometric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..ee31c0264b
--- /dev/null
+++ b/src/metric-spaces/pseudometric-spaces-WIP.lagda.md
@@ -0,0 +1,213 @@
+# Pseudometric spaces (WIP)
+
+```agda
+module metric-spaces.pseudometric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.binary-relations
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.equivalences
+open import foundation.existential-quantification
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.negation
+open import foundation.propositional-extensionality
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.torsorial-type-families
+open import foundation.transport-along-identifications
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import metric-spaces.monotonic-rational-neighborhoods
+open import metric-spaces.rational-neighborhoods
+open import metric-spaces.reflexive-rational-neighborhoods
+open import metric-spaces.saturated-rational-neighborhoods
+open import metric-spaces.symmetric-rational-neighborhoods
+open import metric-spaces.triangular-rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+A {{#concept "pseudometric space" Agda=Pseudometric-Space-WIP}} is a type
+equipped with a
+{{concept "pseudometric structure" Agda=Pseudometric-Structure}}: a
+[reflexive](metric-spaces.reflexive-rational-neighborhoods.md),
+[symmetric](metric-spaces.symmetric-rational-neighborhoods.md),
+[triangular](metric-spaces.triangular-rational-neighborhoods.md) and
+[saturated](metric-spaces.saturated-rational-neighborhoods.md)
+[rational neighborhood relation](metric-spaces.rational-neighborhoods.md)
+
+Given a pseudometric structure `B` on `A` and some positive rational number
+`d : ℚ⁺` such that `B d x y` holds for some pair of points `x y : A`, we
+interpret `d` as an
+{{#concept "upper bound" Disambiguation="on distance in a pseudometric space" Agda=is-upper-bound-dist-Pseudometric-Space-WIP}}
+on the distance between `x` and `y` in the pseudometric space.
+
+## Definitions
+
+### The property of being a premetric structure
+
+```agda
+module _
+  {l1 : Level} (A : UU l1) {l2 : Level}
+  (B : Rational-Neighborhood-Relation l2 A)
+  where
+
+  is-pseudometric-prop-Rational-Neighborhood-Relation : Prop (l1 ⊔ l2)
+  is-pseudometric-prop-Rational-Neighborhood-Relation =
+    product-Prop
+      ( is-reflexive-prop-Rational-Neighborhood-Relation B)
+      ( product-Prop
+        ( is-symmetric-prop-Rational-Neighborhood-Relation B)
+        ( product-Prop
+          ( is-triangular-prop-Rational-Neighborhood-Relation B)
+          ( is-saturated-prop-Rational-Neighborhood-Relation B)))
+
+  is-pseudometric-Rational-Neighborhood-Relation : UU (l1 ⊔ l2)
+  is-pseudometric-Rational-Neighborhood-Relation =
+    type-Prop is-pseudometric-prop-Rational-Neighborhood-Relation
+
+  is-prop-is-pseudometric-Rational-Neighborhood-Relation :
+    is-prop is-pseudometric-Rational-Neighborhood-Relation
+  is-prop-is-pseudometric-Rational-Neighborhood-Relation =
+    is-prop-type-Prop (is-pseudometric-prop-Rational-Neighborhood-Relation)
+
+Pseudometric-Structure :
+  {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2)
+Pseudometric-Structure l2 A =
+  type-subtype (is-pseudometric-prop-Rational-Neighborhood-Relation A {l2})
+```
+
+### Pseudometric spaces
+
+```agda
+Pseudometric-Space-WIP : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Pseudometric-Space-WIP l1 l2 = Σ (UU l1) (Pseudometric-Structure l2)
+
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  where
+
+  type-Pseudometric-Space-WIP : UU l1
+  type-Pseudometric-Space-WIP = pr1 A
+
+  structure-Pseudometric-Space-WIP :
+    Pseudometric-Structure l2 type-Pseudometric-Space-WIP
+  structure-Pseudometric-Space-WIP = pr2 A
+
+  neighborhood-prop-Pseudometric-Space-WIP :
+    ℚ⁺ → Relation-Prop l2 type-Pseudometric-Space-WIP
+  neighborhood-prop-Pseudometric-Space-WIP =
+    pr1 structure-Pseudometric-Space-WIP
+
+  neighborhood-Pseudometric-Space-WIP :
+    ℚ⁺ → Relation l2 type-Pseudometric-Space-WIP
+  neighborhood-Pseudometric-Space-WIP =
+    neighborhood-Rational-Neighborhood-Relation
+      neighborhood-prop-Pseudometric-Space-WIP
+
+  is-prop-neighborhood-Pseudometric-Space-WIP :
+    (d : ℚ⁺) (x y : type-Pseudometric-Space-WIP) →
+    is-prop (neighborhood-Pseudometric-Space-WIP d x y)
+  is-prop-neighborhood-Pseudometric-Space-WIP =
+    is-prop-neighborhood-Rational-Neighborhood-Relation
+      neighborhood-prop-Pseudometric-Space-WIP
+
+  is-upper-bound-dist-prop-Pseudometric-Space-WIP :
+    (x y : type-Pseudometric-Space-WIP) → ℚ⁺ → Prop l2
+  is-upper-bound-dist-prop-Pseudometric-Space-WIP x y d =
+    neighborhood-prop-Pseudometric-Space-WIP d x y
+
+  is-upper-bound-dist-Pseudometric-Space-WIP :
+    (x y : type-Pseudometric-Space-WIP) → ℚ⁺ → UU l2
+  is-upper-bound-dist-Pseudometric-Space-WIP x y d =
+    neighborhood-Pseudometric-Space-WIP d x y
+
+  is-prop-is-upper-bound-dist-Pseudometric-Space-WIP :
+    (x y : type-Pseudometric-Space-WIP) (d : ℚ⁺) →
+    is-prop (is-upper-bound-dist-Pseudometric-Space-WIP x y d)
+  is-prop-is-upper-bound-dist-Pseudometric-Space-WIP x y d =
+    is-prop-neighborhood-Pseudometric-Space-WIP d x y
+
+  is-pseudometric-neighborhood-Pseudometric-Space-WIP :
+    is-pseudometric-Rational-Neighborhood-Relation
+      type-Pseudometric-Space-WIP
+      neighborhood-prop-Pseudometric-Space-WIP
+  is-pseudometric-neighborhood-Pseudometric-Space-WIP =
+    pr2 structure-Pseudometric-Space-WIP
+
+  refl-neighborhood-Pseudometric-Space-WIP :
+    (d : ℚ⁺) (x : type-Pseudometric-Space-WIP) →
+    neighborhood-Pseudometric-Space-WIP d x x
+  refl-neighborhood-Pseudometric-Space-WIP =
+    pr1 is-pseudometric-neighborhood-Pseudometric-Space-WIP
+
+  symmetric-neighborhood-Pseudometric-Space-WIP :
+    (d : ℚ⁺) (x y : type-Pseudometric-Space-WIP) →
+    neighborhood-Pseudometric-Space-WIP d x y →
+    neighborhood-Pseudometric-Space-WIP d y x
+  symmetric-neighborhood-Pseudometric-Space-WIP =
+    pr1 (pr2 is-pseudometric-neighborhood-Pseudometric-Space-WIP)
+
+  inv-neighborhood-Pseudometric-Space-WIP :
+    {d : ℚ⁺} {x y : type-Pseudometric-Space-WIP} →
+    neighborhood-Pseudometric-Space-WIP d x y →
+    neighborhood-Pseudometric-Space-WIP d y x
+  inv-neighborhood-Pseudometric-Space-WIP {d} {x} {y} =
+    symmetric-neighborhood-Pseudometric-Space-WIP d x y
+
+  triangular-neighborhood-Pseudometric-Space-WIP :
+    (x y z : type-Pseudometric-Space-WIP) (d₁ d₂ : ℚ⁺) →
+    neighborhood-Pseudometric-Space-WIP d₂ y z →
+    neighborhood-Pseudometric-Space-WIP d₁ x y →
+    neighborhood-Pseudometric-Space-WIP (d₁ +ℚ⁺ d₂) x z
+  triangular-neighborhood-Pseudometric-Space-WIP =
+    pr1 (pr2 (pr2 is-pseudometric-neighborhood-Pseudometric-Space-WIP))
+
+  saturated-neighborhood-Pseudometric-Space-WIP :
+    (ε : ℚ⁺) (x y : type-Pseudometric-Space-WIP) →
+    ((δ : ℚ⁺) → neighborhood-Pseudometric-Space-WIP (ε +ℚ⁺ δ) x y) →
+    neighborhood-Pseudometric-Space-WIP ε x y
+  saturated-neighborhood-Pseudometric-Space-WIP =
+    pr2 (pr2 (pr2 is-pseudometric-neighborhood-Pseudometric-Space-WIP))
+
+  monotonic-neighborhood-Pseudometric-Space-WIP :
+    (x y : type-Pseudometric-Space-WIP) (d₁ d₂ : ℚ⁺) →
+    le-ℚ⁺ d₁ d₂ →
+    neighborhood-Pseudometric-Space-WIP d₁ x y →
+    neighborhood-Pseudometric-Space-WIP d₂ x y
+  monotonic-neighborhood-Pseudometric-Space-WIP =
+    is-monotonic-is-reflexive-triangular-Rational-Neighborhood-Relation
+      neighborhood-prop-Pseudometric-Space-WIP
+      refl-neighborhood-Pseudometric-Space-WIP
+      triangular-neighborhood-Pseudometric-Space-WIP
+
+  iff-le-neighborhood-Pseudometric-Space-WIP :
+    ( ε : ℚ⁺) (x y : type-Pseudometric-Space-WIP) →
+    ( neighborhood-Pseudometric-Space-WIP ε x y) ↔
+    ( (δ : ℚ⁺) → le-ℚ⁺ ε δ → neighborhood-Pseudometric-Space-WIP δ x y)
+  iff-le-neighborhood-Pseudometric-Space-WIP =
+    iff-le-neighborhood-saturated-monotonic-Rational-Neighborhood-Relation
+      neighborhood-prop-Pseudometric-Space-WIP
+      monotonic-neighborhood-Pseudometric-Space-WIP
+      saturated-neighborhood-Pseudometric-Space-WIP
+```
+
+## External links
+
+- [Pseudometric spaces](https://en.wikipedia.org/wiki/Pseudometric_space) at
+  Wikipedia
diff --git a/src/metric-spaces/rational-neighborhoods.lagda.md b/src/metric-spaces/rational-neighborhoods.lagda.md
new file mode 100644
index 0000000000..070ea3a62e
--- /dev/null
+++ b/src/metric-spaces/rational-neighborhoods.lagda.md
@@ -0,0 +1,340 @@
+# Rational neighborhood relations on types
+
+```agda
+module metric-spaces.rational-neighborhoods where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.binary-relations
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.equivalence-relations
+open import foundation.equivalences
+open import foundation.existential-quantification
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.negation
+open import foundation.propositional-extensionality
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.torsorial-type-families
+open import foundation.transport-along-identifications
+open import foundation.univalence
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "rational neighborhood relation" Agda=Rational-Neighborhood-Relation}}
+is a type family of
+[proposition-valued binary relations](foundation.binary-relations.md) indexed by
+the
+[positive rational numbers](elementary-number-theory.positive-rational-numbers.md).
+
+Given a rational neighborhood relation `N` on `A` and some positive rational
+number `d : ℚ⁺` such that `N d x y` holds for some pair of points `x y : A`, we
+interpret `d` as an
+{{#concept "upper bound" Disambiguation="on the distance with respect to a rational neighborhood relation" Agda=is-upper-bound-dist-Rational-Neighborhood-Relation}}
+on the distance between `x` and `y` with respect to the rational neighborhood
+relation.
+
+## Definitions
+
+### Rational neighborhood relation on a type
+
+```agda
+module _
+  {l1 : Level} (l2 : Level) (A : UU l1)
+  where
+
+  Rational-Neighborhood-Relation : UU (l1 ⊔ lsuc l2)
+  Rational-Neighborhood-Relation = ℚ⁺ → Relation-Prop l2 A
+
+module _
+  {l1 l2 : Level} {A : UU l1} (B : Rational-Neighborhood-Relation l2 A)
+  where
+
+  neighborhood-Rational-Neighborhood-Relation :
+    ℚ⁺ → Relation l2 A
+  neighborhood-Rational-Neighborhood-Relation d x y =
+    type-Prop (B d x y)
+
+  is-prop-neighborhood-Rational-Neighborhood-Relation :
+    (d : ℚ⁺) (x y : A) →
+    is-prop (neighborhood-Rational-Neighborhood-Relation d x y)
+  is-prop-neighborhood-Rational-Neighborhood-Relation d x y =
+    is-prop-type-Prop (B d x y)
+
+  is-upper-bound-dist-prop-Rational-Neighborhood-Relation :
+    A → A → ℚ⁺ → Prop l2
+  is-upper-bound-dist-prop-Rational-Neighborhood-Relation x y d = B d x y
+
+  is-upper-bound-dist-Rational-Neighborhood-Relation :
+    A → A → ℚ⁺ → UU l2
+  is-upper-bound-dist-Rational-Neighborhood-Relation x y d =
+    neighborhood-Rational-Neighborhood-Relation d x y
+
+  is-prop-is-upper-bound-dist-Rational-Neighborhood-Relation :
+    (x y : A) (d : ℚ⁺) →
+    is-prop (is-upper-bound-dist-Rational-Neighborhood-Relation x y d)
+  is-prop-is-upper-bound-dist-Rational-Neighborhood-Relation x y d =
+    is-prop-neighborhood-Rational-Neighborhood-Relation d x y
+```
+
+## Properties
+
+### Equality of rational neighborhood relations
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (N : Rational-Neighborhood-Relation l2 A)
+  {l2' : Level} (N' : Rational-Neighborhood-Relation l2' A)
+  where
+
+  Eq-prop-Rational-Neighborhood-Relation : Prop (l1 ⊔ l2 ⊔ l2')
+  Eq-prop-Rational-Neighborhood-Relation =
+    Π-Prop
+      ( ℚ⁺)
+      ( λ d →
+        Π-Prop
+          ( A)
+          ( λ x →
+            Π-Prop
+              ( A)
+              ( λ y → N d x y ⇔ N' d x y)))
+
+  Eq-Rational-Neighborhood-Relation : UU (l1 ⊔ l2 ⊔ l2')
+  Eq-Rational-Neighborhood-Relation =
+    type-Prop Eq-prop-Rational-Neighborhood-Relation
+
+  is-prop-Eq-Rational-Neighborhood-Relation :
+    is-prop Eq-Rational-Neighborhood-Relation
+  is-prop-Eq-Rational-Neighborhood-Relation =
+    is-prop-type-Prop Eq-prop-Rational-Neighborhood-Relation
+```
+
+### Identity principle for rational neighborhood relations
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (N : Rational-Neighborhood-Relation l2 A)
+  where
+
+  refl-Eq-Rational-Neighborhood-Relation : Eq-Rational-Neighborhood-Relation N N
+  refl-Eq-Rational-Neighborhood-Relation d x y = id-iff
+
+  Eq-eq-Rational-Neighborhood-Relation :
+    (N' : Rational-Neighborhood-Relation l2 A) →
+    N ＝ N' →
+    Eq-Rational-Neighborhood-Relation N N'
+  Eq-eq-Rational-Neighborhood-Relation .N refl =
+    refl-Eq-Rational-Neighborhood-Relation
+
+  eq-Eq-Rational-Neighborhood-Relation :
+    (N' : Rational-Neighborhood-Relation l2 A) →
+    Eq-Rational-Neighborhood-Relation N N' →
+    N ＝ N'
+  eq-Eq-Rational-Neighborhood-Relation N' H =
+    eq-htpy
+      ( λ d →
+        eq-htpy
+        ( λ x →
+          eq-htpy
+          ( λ y →
+            eq-iff' (N d x y) (N' d x y) (H d x y))))
+
+  is-torsorial-Eq-Rational-Neighborhood-Relation :
+    is-torsorial (Eq-Rational-Neighborhood-Relation N)
+  is-torsorial-Eq-Rational-Neighborhood-Relation =
+    ( N , refl-Eq-Rational-Neighborhood-Relation) ,
+    ( λ (N' , e) →
+      eq-type-subtype
+        ( Eq-prop-Rational-Neighborhood-Relation N)
+        ( eq-Eq-Rational-Neighborhood-Relation N' e))
+
+  is-fiberwise-equiv-Eq-eq-Rational-Neighborhood-Relation :
+    (N' : Rational-Neighborhood-Relation l2 A) →
+    is-equiv (Eq-eq-Rational-Neighborhood-Relation N')
+  is-fiberwise-equiv-Eq-eq-Rational-Neighborhood-Relation =
+    fundamental-theorem-id
+      is-torsorial-Eq-Rational-Neighborhood-Relation
+      Eq-eq-Rational-Neighborhood-Relation
+
+  equiv-Eq-eq-Rational-Neighborhood-Relation :
+    (N' : Rational-Neighborhood-Relation l2 A) →
+    (N ＝ N') ≃ (Eq-Rational-Neighborhood-Relation N N')
+  equiv-Eq-eq-Rational-Neighborhood-Relation N' =
+    Eq-eq-Rational-Neighborhood-Relation N' ,
+    is-fiberwise-equiv-Eq-eq-Rational-Neighborhood-Relation N'
+```
+
+### Characterization of the transport of rational neighborhood relations along equality of types
+
+```agda
+module _
+  {l1 l2 : Level} (A : UU l1)
+  where
+
+  Eq-map-eq-tr-Rational-Neighborhood-Relation :
+    (B : UU l1) (e : A ＝ B) (S : Rational-Neighborhood-Relation l2 A) →
+    Eq-Rational-Neighborhood-Relation
+      ( S)
+      ( λ d x y →
+        tr (Rational-Neighborhood-Relation l2) e S d (map-eq e x) (map-eq e y))
+  Eq-map-eq-tr-Rational-Neighborhood-Relation .A refl S =
+    refl-Eq-Rational-Neighborhood-Relation S
+
+  eq-map-eq-tr-Rational-Neighborhood-Relation :
+    (B : UU l1) (e : A ＝ B) (S : Rational-Neighborhood-Relation l2 A) →
+    Id
+      ( S)
+      ( λ d x y →
+        tr (Rational-Neighborhood-Relation l2) e S d (map-eq e x) (map-eq e y))
+  eq-map-eq-tr-Rational-Neighborhood-Relation B e S =
+    eq-Eq-Rational-Neighborhood-Relation
+      ( S)
+      ( λ d x y →
+        tr (Rational-Neighborhood-Relation l2) e S d (map-eq e x) (map-eq e y))
+      ( Eq-map-eq-tr-Rational-Neighborhood-Relation B e S)
+
+  Eq-map-inv-eq-tr-Rational-Neighborhood-Relation :
+    (B : UU l1) (e : A ＝ B) (S : Rational-Neighborhood-Relation l2 A) →
+    Eq-Rational-Neighborhood-Relation
+      ( tr (Rational-Neighborhood-Relation l2) e S)
+      ( λ d x y → S d (map-inv-eq e x) (map-inv-eq e y))
+  Eq-map-inv-eq-tr-Rational-Neighborhood-Relation .A refl S =
+    refl-Eq-Rational-Neighborhood-Relation S
+
+  eq-map-inv-eq-tr-Rational-Neighborhood-Relation :
+    (B : UU l1) (e : A ＝ B) (S : Rational-Neighborhood-Relation l2 A) →
+    Id
+      ( tr (Rational-Neighborhood-Relation l2) e S)
+      ( λ d x y → S d (map-inv-eq e x) (map-inv-eq e y))
+  eq-map-inv-eq-tr-Rational-Neighborhood-Relation B e S =
+    eq-Eq-Rational-Neighborhood-Relation
+      ( tr (Rational-Neighborhood-Relation l2) e S)
+      ( λ d x y → S d (map-inv-eq e x) (map-inv-eq e y))
+      ( Eq-map-inv-eq-tr-Rational-Neighborhood-Relation B e S)
+```
+
+### The similarity relation induced by a rational neighborhood relation
+
+```agda
+module _ {l1 l2 : Level} {A : UU l1} (N : Rational-Neighborhood-Relation l2 A)
+  where
+
+  sim-prop-Rational-Neighborhood-Relation : Relation-Prop (l1 ⊔ l2) A
+  sim-prop-Rational-Neighborhood-Relation x y =
+    Π-Prop
+      ( ℚ⁺)
+      ( λ d →
+        Π-Prop
+          ( A)
+          ( λ z →
+            product-Prop
+              ( N d x z ⇔ N d y z)
+              ( N d z x ⇔ N d z y)))
+
+  sim-Rational-Neighborhood-Relation : Relation (l1 ⊔ l2) A
+  sim-Rational-Neighborhood-Relation x y =
+    type-Prop (sim-prop-Rational-Neighborhood-Relation x y)
+
+  is-prop-sim-Rational-Neighborhood-Relatiion :
+    (x y : A) → is-prop (sim-Rational-Neighborhood-Relation x y)
+  is-prop-sim-Rational-Neighborhood-Relatiion x y =
+    is-prop-type-Prop (sim-prop-Rational-Neighborhood-Relation x y)
+
+  iff-left-neighbor-sim-Rational-Neighborhood-Relation :
+    {x y : A} →
+    sim-Rational-Neighborhood-Relation x y →
+    (d : ℚ⁺) (z : A) →
+    neighborhood-Rational-Neighborhood-Relation N d x z ↔
+    neighborhood-Rational-Neighborhood-Relation N d y z
+  iff-left-neighbor-sim-Rational-Neighborhood-Relation x≍y d z =
+    pr1 (x≍y d z)
+
+  iff-right-neighbor-sim-Rational-Neighborhood-Relation :
+    {x y : A} →
+    sim-Rational-Neighborhood-Relation x y →
+    (d : ℚ⁺) (z : A) →
+    neighborhood-Rational-Neighborhood-Relation N d z x ↔
+    neighborhood-Rational-Neighborhood-Relation N d z y
+  iff-right-neighbor-sim-Rational-Neighborhood-Relation x≍y d z =
+    pr2 (x≍y d z)
+
+  refl-sim-Rational-Neighborhood-Relation :
+    (x : A) → sim-Rational-Neighborhood-Relation x x
+  refl-sim-Rational-Neighborhood-Relation x d z = id-iff , id-iff
+
+  sim-eq-Rational-Neighborhood-Relation :
+    (x y : A) → x ＝ y → sim-Rational-Neighborhood-Relation x y
+  sim-eq-Rational-Neighborhood-Relation x .x refl =
+    refl-sim-Rational-Neighborhood-Relation x
+
+  symmetric-sim-Rational-Neighborhood-Relation :
+    (x y : A) →
+    sim-Rational-Neighborhood-Relation x y →
+    sim-Rational-Neighborhood-Relation y x
+  symmetric-sim-Rational-Neighborhood-Relation x y x≍y d z =
+    ( inv-iff (iff-left-neighbor-sim-Rational-Neighborhood-Relation x≍y d z)) ,
+    ( inv-iff (iff-right-neighbor-sim-Rational-Neighborhood-Relation x≍y d z))
+
+  inv-sim-Rational-Neighborhood-Relation :
+    {x y : A} →
+    sim-Rational-Neighborhood-Relation x y →
+    sim-Rational-Neighborhood-Relation y x
+  inv-sim-Rational-Neighborhood-Relation {x} {y} =
+    symmetric-sim-Rational-Neighborhood-Relation x y
+
+  transitive-sim-Rational-Neighborhood-Relation :
+    (x y z : A) →
+    sim-Rational-Neighborhood-Relation y z →
+    sim-Rational-Neighborhood-Relation x y →
+    sim-Rational-Neighborhood-Relation x z
+  transitive-sim-Rational-Neighborhood-Relation x y z y≍z x≍y d w =
+    ( ( iff-left-neighbor-sim-Rational-Neighborhood-Relation y≍z d w) ∘iff
+      ( iff-left-neighbor-sim-Rational-Neighborhood-Relation x≍y d w)) ,
+    ( ( iff-right-neighbor-sim-Rational-Neighborhood-Relation y≍z d w) ∘iff
+      ( iff-right-neighbor-sim-Rational-Neighborhood-Relation x≍y d w))
+
+  is-equivalence-relation-sim-Rational-Neighborhood-Relation :
+    is-equivalence-relation (sim-prop-Rational-Neighborhood-Relation)
+  is-equivalence-relation-sim-Rational-Neighborhood-Relation =
+    refl-sim-Rational-Neighborhood-Relation ,
+    symmetric-sim-Rational-Neighborhood-Relation ,
+    transitive-sim-Rational-Neighborhood-Relation
+
+  equivalence-sim-Rational-Neighborhood-Relation :
+    equivalence-relation (l1 ⊔ l2) A
+  equivalence-sim-Rational-Neighborhood-Relation =
+    sim-prop-Rational-Neighborhood-Relation ,
+    is-equivalence-relation-sim-Rational-Neighborhood-Relation
+```
+
+### Similar elements have equivalent self-neighborhoods
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (N : Rational-Neighborhood-Relation l2 A)
+  where
+
+  iff-self-neighborhood-sim-Rational-Neighborhood-Relation :
+    (d : ℚ⁺) (x y : A) →
+    sim-Rational-Neighborhood-Relation N x y →
+    neighborhood-Rational-Neighborhood-Relation N d x x ↔
+    neighborhood-Rational-Neighborhood-Relation N d y y
+  iff-self-neighborhood-sim-Rational-Neighborhood-Relation d x y x≍y =
+    ( iff-right-neighbor-sim-Rational-Neighborhood-Relation N x≍y d y) ∘iff
+    ( iff-left-neighbor-sim-Rational-Neighborhood-Relation N x≍y d x)
+```
diff --git a/src/metric-spaces/reflexive-rational-neighborhoods.lagda.md b/src/metric-spaces/reflexive-rational-neighborhoods.lagda.md
new file mode 100644
index 0000000000..1fc82e1c0b
--- /dev/null
+++ b/src/metric-spaces/reflexive-rational-neighborhoods.lagda.md
@@ -0,0 +1,49 @@
+# Reflexive rational neighborhoods on types
+
+```agda
+module metric-spaces.reflexive-rational-neighborhoods where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.binary-relations
+open import foundation.function-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import metric-spaces.rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+A [rational neighborhood](metric-spaces.rational-neighborhoods.md) is
+{{#concept "reflexive" Disambiguation="rational neighborhood relation" Agda=is-reflexive-Rational-Neighborhood-Relation}}
+if any element is in all neighborhoods of itself.
+
+## Definitions
+
+### The property of being a reflexive rational neighborhood relation
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (B : Rational-Neighborhood-Relation l2 A)
+  where
+
+  is-reflexive-prop-Rational-Neighborhood-Relation : Prop (l1 ⊔ l2)
+  is-reflexive-prop-Rational-Neighborhood-Relation =
+    Π-Prop ℚ⁺ (is-reflexive-prop-Relation-Prop ∘ B)
+
+  is-reflexive-Rational-Neighborhood-Relation : UU (l1 ⊔ l2)
+  is-reflexive-Rational-Neighborhood-Relation =
+    type-Prop is-reflexive-prop-Rational-Neighborhood-Relation
+
+  is-prop-is-reflexive-Rational-Neighborhood-Relation :
+    is-prop is-reflexive-Rational-Neighborhood-Relation
+  is-prop-is-reflexive-Rational-Neighborhood-Relation =
+    is-prop-type-Prop is-reflexive-prop-Rational-Neighborhood-Relation
+```
diff --git a/src/metric-spaces/saturated-rational-neighborhoods.lagda.md b/src/metric-spaces/saturated-rational-neighborhoods.lagda.md
new file mode 100644
index 0000000000..b3875fbe99
--- /dev/null
+++ b/src/metric-spaces/saturated-rational-neighborhoods.lagda.md
@@ -0,0 +1,145 @@
+# Saturated rational neighborhood relations
+
+```agda
+module metric-spaces.saturated-rational-neighborhoods where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-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-functions
+open import foundation.binary-relations
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositional-extensionality
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.torsorial-type-families
+open import foundation.transport-along-identifications
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import metric-spaces.monotonic-rational-neighborhoods
+open import metric-spaces.rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+A [rational neighborhood relation](metric-spaces.rational-neighborhoods.md) on a
+type `A` is
+{{#concept "saturated" Disambiguation="rational neighborhood relation" Agda=is-saturated-Rational-Neighborhood-Relation}}
+if `ε`-neighborhoods satisfy the following condition:
+
+- For any `x y : A`, if `x` and `y` are in a `(ε + δ)`-neighborhood for all
+  [positive rational numbers](elementary-number-theory.positive-rational-numbers.md)
+  `δ`, then they are in a `ε`-neighborhood.
+
+Or, equivalently if for any `(x y : A)`, the subset of
+[upper bounds](metric-spaces.rational-neighborhoods.md) on the distance between
+`x` and `y` is closed on the left:
+
+- For any `ε : ℚ⁺`, if `ε + δ` is an upper bound of the distance between `x` and
+  `y` for all `(δ : ℚ⁺)`, then so is `ε`.
+
+## Definitions
+
+### The property of being a saturated rational neighborhood relation
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (N : Rational-Neighborhood-Relation l2 A)
+  where
+
+  is-saturated-prop-Rational-Neighborhood-Relation : Prop (l1 ⊔ l2)
+  is-saturated-prop-Rational-Neighborhood-Relation =
+    Π-Prop
+      ( ℚ⁺)
+      ( λ ε →
+        Π-Prop
+        ( A)
+        ( λ x →
+          Π-Prop
+            ( A)
+            ( λ y →
+              hom-Prop
+                ( Π-Prop
+                  ( ℚ⁺)
+                  ( λ δ → N (ε +ℚ⁺ δ) x y))
+                ( N ε x y))))
+
+  is-saturated-Rational-Neighborhood-Relation : UU (l1 ⊔ l2)
+  is-saturated-Rational-Neighborhood-Relation =
+    type-Prop is-saturated-prop-Rational-Neighborhood-Relation
+
+  is-prop-is-saturated-Rational-Neighborhood-Relation :
+    is-prop is-saturated-Rational-Neighborhood-Relation
+  is-prop-is-saturated-Rational-Neighborhood-Relation =
+    is-prop-type-Prop is-saturated-prop-Rational-Neighborhood-Relation
+```
+
+### The saturation of a rational neighborhood relation
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (N : Rational-Neighborhood-Relation l2 A)
+  where
+
+  saturate-Rational-Neighborhood-Relation : Rational-Neighborhood-Relation l2 A
+  saturate-Rational-Neighborhood-Relation ε x y =
+    Π-Prop ℚ⁺ (λ δ → N (ε +ℚ⁺ δ) x y)
+```
+
+## Properties
+
+### The saturation of a rational neighborhood relation is saturated
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (N : Rational-Neighborhood-Relation l2 A)
+  where
+
+  is-saturated-saturate-Rational-Neighborhood-Relation :
+    is-saturated-Rational-Neighborhood-Relation
+      ( saturate-Rational-Neighborhood-Relation N)
+  is-saturated-saturate-Rational-Neighborhood-Relation ε x y H δ =
+    tr
+      ( is-upper-bound-dist-Rational-Neighborhood-Relation N x y)
+      ( ( associative-add-ℚ⁺
+          ( ε)
+          ( left-summand-split-ℚ⁺ δ)
+          ( right-summand-split-ℚ⁺ δ)) ∙
+        ( ap (add-ℚ⁺ ε) (eq-add-split-ℚ⁺ δ)))
+      ( H (left-summand-split-ℚ⁺ δ) (right-summand-split-ℚ⁺ δ))
+```
+
+### In a monotonic saturated rational neighborhood relation, `N ε x y ⇔ (∀ δ → ε < δ → N δ x y)`
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (N : Rational-Neighborhood-Relation l2 A)
+  (monotonic-N : is-monotonic-Rational-Neighborhood-Relation N)
+  (saturated-N : is-saturated-Rational-Neighborhood-Relation N)
+  where
+
+  iff-le-neighborhood-saturated-monotonic-Rational-Neighborhood-Relation :
+    ( ε : ℚ⁺) (x y : A) →
+    ( neighborhood-Rational-Neighborhood-Relation N ε x y) ↔
+    ( (δ : ℚ⁺) →
+      le-ℚ⁺ ε δ →
+      neighborhood-Rational-Neighborhood-Relation N δ x y)
+  iff-le-neighborhood-saturated-monotonic-Rational-Neighborhood-Relation ε x y =
+    ( λ Nxy δ ε<δ → monotonic-N x y ε δ ε<δ Nxy) ,
+    ( λ H → saturated-N ε x y λ δ → H (ε +ℚ⁺ δ) (le-left-add-ℚ⁺ ε δ))
+```
diff --git a/src/metric-spaces/short-functions-metric-spaces-WIP.lagda.md b/src/metric-spaces/short-functions-metric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..bedf0d9902
--- /dev/null
+++ b/src/metric-spaces/short-functions-metric-spaces-WIP.lagda.md
@@ -0,0 +1,345 @@
+# Short functions between metric spaces (WIP)
+
+```agda
+module metric-spaces.short-functions-metric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.existential-quantification
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.sequences
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import metric-spaces.isometries-metric-spaces-WIP
+open import metric-spaces.metric-spaces-WIP
+open import metric-spaces.ordering-rational-neighborhoods
+open import metric-spaces.preimage-rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+A [function](metric-spaces.functions-metric-spaces.md) `f` between two
+[metric spaces](metric-spaces.metric-spaces.md) `A` and `B` is
+{{#concept "short" Disambiguation="function between metric spaces" Agda=is-short-function-Metric-Space-WIP WD="metric map" WDID=Q2713824}}
+if the [rational neighborhood relation](metric-spaces.rational-neighborhoods.md)
+on `A` is [finer](metric-spaces.ordering-rational-neighborhoods.md) than the
+[preimage](metric-spaces.preimage-rational-neighborhoods.md) by `f` of the
+rational neighborhood relation on `B`. I.e., upper bounds on the distance
+between two points in `A` are upper bounds of the distance between their images
+in `B`.
+
+## Definitions
+
+### The property of being a short function between metric spaces
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  (f : type-function-Metric-Space-WIP A B)
+  where
+
+  is-short-function-prop-Metric-Space-WIP : Prop (l1 ⊔ l2 ⊔ l2')
+  is-short-function-prop-Metric-Space-WIP =
+    leq-prop-Rational-Neighborhood-Relation
+      ( neighborhood-prop-Metric-Space-WIP A)
+      ( preimage-Rational-Neighborhood-Relation
+        ( f)
+        ( neighborhood-prop-Metric-Space-WIP B))
+
+  is-short-function-Metric-Space-WIP : UU (l1 ⊔ l2 ⊔ l2')
+  is-short-function-Metric-Space-WIP =
+    type-Prop is-short-function-prop-Metric-Space-WIP
+
+  is-prop-is-short-function-Metric-Space-WIP :
+    is-prop is-short-function-Metric-Space-WIP
+  is-prop-is-short-function-Metric-Space-WIP =
+    is-prop-type-Prop is-short-function-prop-Metric-Space-WIP
+```
+
+### The set of short functions between metric spaces
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  where
+
+  set-short-function-Metric-Space-WIP : Set (l1 ⊔ l2 ⊔ l1' ⊔ l2')
+  set-short-function-Metric-Space-WIP =
+    set-subset
+      ( set-function-Metric-Space-WIP A B)
+      ( is-short-function-prop-Metric-Space-WIP A B)
+
+  short-function-Metric-Space-WIP : UU (l1 ⊔ l2 ⊔ l1' ⊔ l2')
+  short-function-Metric-Space-WIP = type-Set set-short-function-Metric-Space-WIP
+
+  is-set-short-function-Metric-Space-WIP :
+    is-set short-function-Metric-Space-WIP
+  is-set-short-function-Metric-Space-WIP =
+    is-set-type-Set set-short-function-Metric-Space-WIP
+
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  (f : short-function-Metric-Space-WIP A B)
+  where
+
+  map-short-function-Metric-Space-WIP : type-function-Metric-Space-WIP A B
+  map-short-function-Metric-Space-WIP = pr1 f
+
+  is-short-map-short-function-Metric-Space-WIP :
+    is-short-function-Metric-Space-WIP A B map-short-function-Metric-Space-WIP
+  is-short-map-short-function-Metric-Space-WIP = pr2 f
+```
+
+## Properties
+
+### The identity function on a metric space is short
+
+```agda
+module _
+  {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  where
+
+  is-short-id-Metric-Space-WIP :
+    is-short-function-Metric-Space-WIP A A (λ x → x)
+  is-short-id-Metric-Space-WIP d x y H = H
+
+  short-id-Metric-Space-WIP : short-function-Metric-Space-WIP A A
+  short-id-Metric-Space-WIP =
+    (λ x → x) , is-short-id-Metric-Space-WIP
+```
+
+### Equality of short functions between metric spaces is characterized by homotopy of their carrier maps
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  (f g : short-function-Metric-Space-WIP A B)
+  where
+
+  equiv-eq-htpy-map-short-function-Metric-Space-WIP :
+    ( f ＝ g) ≃
+    ( map-short-function-Metric-Space-WIP A B f ~
+      map-short-function-Metric-Space-WIP A B g)
+  equiv-eq-htpy-map-short-function-Metric-Space-WIP =
+    equiv-funext ∘e
+    extensionality-type-subtype'
+      ( is-short-function-prop-Metric-Space-WIP A B) f g
+
+  eq-htpy-map-short-function-Metric-Space-WIP :
+    ( map-short-function-Metric-Space-WIP A B f ~
+      map-short-function-Metric-Space-WIP A B g) →
+    ( f ＝ g)
+  eq-htpy-map-short-function-Metric-Space-WIP =
+    map-inv-equiv equiv-eq-htpy-map-short-function-Metric-Space-WIP
+```
+
+### Composition of short functions
+
+```agda
+module _
+  {l1a l2a l1b l2b l1c l2c : Level}
+  (A : Metric-Space-WIP l1a l2a)
+  (B : Metric-Space-WIP l1b l2b)
+  (C : Metric-Space-WIP l1c l2c)
+  where
+
+  is-short-comp-is-short-function-Metric-Space-WIP :
+    (g : type-function-Metric-Space-WIP B C) →
+    (f : type-function-Metric-Space-WIP A B) →
+    is-short-function-Metric-Space-WIP B C g →
+    is-short-function-Metric-Space-WIP A B f →
+    is-short-function-Metric-Space-WIP A C (g ∘ f)
+  is-short-comp-is-short-function-Metric-Space-WIP g f H K d x y =
+    H d (f x) (f y) ∘ K d x y
+
+  comp-short-function-Metric-Space-WIP :
+    short-function-Metric-Space-WIP B C →
+    short-function-Metric-Space-WIP A B →
+    short-function-Metric-Space-WIP A C
+  comp-short-function-Metric-Space-WIP g f =
+    ( map-short-function-Metric-Space-WIP B C g ∘
+      map-short-function-Metric-Space-WIP A B f) ,
+    ( is-short-comp-is-short-function-Metric-Space-WIP
+      ( map-short-function-Metric-Space-WIP B C g)
+      ( map-short-function-Metric-Space-WIP A B f)
+      ( is-short-map-short-function-Metric-Space-WIP B C g)
+      ( is-short-map-short-function-Metric-Space-WIP A B f))
+```
+
+### Unit laws for composition of short maps between metric spaces
+
+```agda
+module _
+  {l1a l2a l1b l2b : Level}
+  (A : Metric-Space-WIP l1a l2a)
+  (B : Metric-Space-WIP l1b l2b)
+  (f : short-function-Metric-Space-WIP A B)
+  where
+
+  left-unit-law-comp-short-function-Metric-Space-WIP :
+    ( comp-short-function-Metric-Space-WIP A B B
+      ( short-id-Metric-Space-WIP B)
+      ( f)) ＝
+    ( f)
+  left-unit-law-comp-short-function-Metric-Space-WIP =
+    eq-htpy-map-short-function-Metric-Space-WIP
+      ( A)
+      ( B)
+      ( comp-short-function-Metric-Space-WIP
+        ( A)
+        ( B)
+        ( B)
+        ( short-id-Metric-Space-WIP B)
+        ( f))
+      ( f)
+      ( λ x → refl)
+
+  right-unit-law-comp-short-function-Metric-Space-WIP :
+    ( comp-short-function-Metric-Space-WIP A A B
+      ( f)
+      ( short-id-Metric-Space-WIP A)) ＝
+    ( f)
+  right-unit-law-comp-short-function-Metric-Space-WIP =
+    eq-htpy-map-short-function-Metric-Space-WIP
+      ( A)
+      ( B)
+      ( f)
+      ( comp-short-function-Metric-Space-WIP
+        ( A)
+        ( A)
+        ( B)
+        ( f)
+        ( short-id-Metric-Space-WIP A))
+      ( λ x → refl)
+```
+
+### Associativity of composition of short maps between metric spaces
+
+```agda
+module _
+  {l1a l2a l1b l2b l1c l2c l1d l2d : Level}
+  (A : Metric-Space-WIP l1a l2a)
+  (B : Metric-Space-WIP l1b l2b)
+  (C : Metric-Space-WIP l1c l2c)
+  (D : Metric-Space-WIP l1d l2d)
+  (h : short-function-Metric-Space-WIP C D)
+  (g : short-function-Metric-Space-WIP B C)
+  (f : short-function-Metric-Space-WIP A B)
+  where
+
+  associative-comp-short-function-Metric-Space-WIP :
+    ( comp-short-function-Metric-Space-WIP A B D
+      ( comp-short-function-Metric-Space-WIP B C D h g)
+        ( f)) ＝
+    ( comp-short-function-Metric-Space-WIP A C D
+      ( h)
+      ( comp-short-function-Metric-Space-WIP A B C g f))
+  associative-comp-short-function-Metric-Space-WIP =
+    eq-htpy-map-short-function-Metric-Space-WIP
+      ( A)
+      ( D)
+      ( comp-short-function-Metric-Space-WIP A B D
+        ( comp-short-function-Metric-Space-WIP B C D h g)
+        ( f))
+      ( comp-short-function-Metric-Space-WIP A C D
+        ( h)
+        ( comp-short-function-Metric-Space-WIP A B C g f))
+      ( λ x → refl)
+```
+
+### Constant functions between metric spaces are short
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  (b : type-Metric-Space-WIP B)
+  where
+
+  is-short-constant-function-Metric-Space-WIP :
+    is-short-function-Metric-Space-WIP A B (λ _ → b)
+  is-short-constant-function-Metric-Space-WIP ε x y H =
+    refl-neighborhood-Metric-Space-WIP B ε b
+```
+
+### Any isometry between metric spaces is short
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  (f : type-function-Metric-Space-WIP A B)
+  where
+
+  is-short-is-isometry-Metric-Space-WIP :
+    is-isometry-Metric-Space-WIP A B f →
+    is-short-function-Metric-Space-WIP A B f
+  is-short-is-isometry-Metric-Space-WIP I =
+    preserves-neighborhood-map-isometry-Metric-Space-WIP A B (f , I)
+```
+
+### The embedding of isometries of metric spaces into short maps
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l1' l2')
+  where
+
+  short-isometry-Metric-Space-WIP :
+    isometry-Metric-Space-WIP A B → short-function-Metric-Space-WIP A B
+  short-isometry-Metric-Space-WIP f =
+    map-isometry-Metric-Space-WIP A B f ,
+    is-short-is-isometry-Metric-Space-WIP
+      ( A)
+      ( B)
+      ( map-isometry-Metric-Space-WIP A B f)
+      ( is-isometry-map-isometry-Metric-Space-WIP A B f)
+
+  is-emb-short-isometry-Metric-Space-WIP :
+    is-emb short-isometry-Metric-Space-WIP
+  is-emb-short-isometry-Metric-Space-WIP =
+    is-emb-right-factor
+      ( map-short-function-Metric-Space-WIP A B)
+      ( short-isometry-Metric-Space-WIP)
+      ( is-emb-inclusion-subtype (is-short-function-prop-Metric-Space-WIP A B))
+      ( is-emb-htpy
+        ( λ f → refl)
+        ( is-emb-inclusion-subtype (is-isometry-prop-Metric-Space-WIP A B)))
+
+  emb-short-isometry-Metric-Space :
+    isometry-Metric-Space-WIP A B ↪ short-function-Metric-Space-WIP A B
+  emb-short-isometry-Metric-Space =
+    short-isometry-Metric-Space-WIP ,
+    is-emb-short-isometry-Metric-Space-WIP
+```
+
+## See also
+
+- The
+  [category of short functions on metric spaces](metric-spaces.category-of-metric-spaces-and-short-functions.md)
+
+## External links
+
+- [Short maps](https://ncatlab.org/nlab/show/short+map) at $n$Lab
+- [Metric maps](https://en.wikipedia.org/wiki/Metric_map) at Wikipedia
diff --git a/src/metric-spaces/short-functions-metric-spaces.lagda.md b/src/metric-spaces/short-functions-metric-spaces.lagda.md
index 566e76808f..ed1f20ba8c 100644
--- a/src/metric-spaces/short-functions-metric-spaces.lagda.md
+++ b/src/metric-spaces/short-functions-metric-spaces.lagda.md
@@ -228,7 +228,7 @@ module _
       ( λ x → refl)
 ```
 
-### Associatity of composition of short maps between metric spaces
+### Associativity of composition of short maps between metric spaces
 
 ```agda
 module _
diff --git a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md
new file mode 100644
index 0000000000..976a9cbffe
--- /dev/null
+++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md
@@ -0,0 +1,257 @@
+# Similarity of elements in pseudometric spaces
+
+```agda
+module metric-spaces.similarity-of-elements-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.binary-relations
+open import foundation.dependent-pair-types
+open import foundation.equivalence-relations
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositions
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import metric-spaces.pseudometric-spaces-WIP
+open import metric-spaces.rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+Two elements `x y` of a
+[pseudometric space](metric-spaces.pseudometric-spaces-WIP.md) are
+{{#concept "similar" Disambiguation="elements of a pseudometric space" Agda=sim-Pseudometric-Space-WIP}}
+if any of the following equivalent propositions holds:
+
+- they are similar w.r.t the underlying
+  [rational neighborhood relation](metric-spaces.rational-neighborhoods.md);
+- they have the same neighbors: `∀ δ z → N δ x z ↔ N δ y z`;
+- they share all neighborhoods: `∀ δ → N δ x y`.
+
+Similarity in a pseudometric space is an
+[equivalence relation](foundation.equivalence-relations.md).
+
+## Definitions
+
+### Neighborhood similarity relation in pseudometric spaces
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  where
+
+  sim-prop-Pseudometric-Space-WIP :
+    Relation-Prop l2 (type-Pseudometric-Space-WIP A)
+  sim-prop-Pseudometric-Space-WIP x y =
+    Π-Prop ℚ⁺ (is-upper-bound-dist-prop-Pseudometric-Space-WIP A x y)
+
+  sim-Pseudometric-Space-WIP :
+    Relation l2 (type-Pseudometric-Space-WIP A)
+  sim-Pseudometric-Space-WIP =
+    type-Relation-Prop sim-prop-Pseudometric-Space-WIP
+
+  is-prop-sim-Pseudometric-Space-WIP :
+    (x y : type-Pseudometric-Space-WIP A) →
+    is-prop (sim-Pseudometric-Space-WIP x y)
+  is-prop-sim-Pseudometric-Space-WIP =
+    is-prop-type-Relation-Prop sim-prop-Pseudometric-Space-WIP
+```
+
+## Properties
+
+### Similarity in pseudometric spaces is reflexive
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  where
+
+  refl-sim-Pseudometric-Space-WIP :
+    (x : type-Pseudometric-Space-WIP A) →
+    sim-Pseudometric-Space-WIP A x x
+  refl-sim-Pseudometric-Space-WIP x d =
+    refl-neighborhood-Pseudometric-Space-WIP A d x
+
+  sim-eq-Pseudometric-Space-WIP :
+    (x y : type-Pseudometric-Space-WIP A) →
+    x ＝ y →
+    sim-Pseudometric-Space-WIP A x y
+  sim-eq-Pseudometric-Space-WIP x .x refl =
+    refl-sim-Pseudometric-Space-WIP x
+```
+
+### Similarity in pseudometric spaces is symmetric
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  where
+
+  symmetric-sim-Pseudometric-Space-WIP :
+    (x y : type-Pseudometric-Space-WIP A) →
+    sim-Pseudometric-Space-WIP A x y →
+    sim-Pseudometric-Space-WIP A y x
+  symmetric-sim-Pseudometric-Space-WIP x y Nxy d =
+    symmetric-neighborhood-Pseudometric-Space-WIP A d x y (Nxy d)
+
+  inv-sim-Pseudometric-Space-WIP :
+    {x y : type-Pseudometric-Space-WIP A} →
+    sim-Pseudometric-Space-WIP A x y →
+    sim-Pseudometric-Space-WIP A y x
+  inv-sim-Pseudometric-Space-WIP {x} {y} =
+    symmetric-sim-Pseudometric-Space-WIP x y
+```
+
+### Similarity in pseudometric spaces is transitive
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  where
+
+  transitive-sim-Pseudometric-Space-WIP :
+    (x y z : type-Pseudometric-Space-WIP A) →
+    sim-Pseudometric-Space-WIP A y z →
+    sim-Pseudometric-Space-WIP A x y →
+    sim-Pseudometric-Space-WIP A x z
+  transitive-sim-Pseudometric-Space-WIP x y z Nyz Nxy d =
+    tr
+      ( is-upper-bound-dist-Pseudometric-Space-WIP A x z)
+      ( eq-add-split-ℚ⁺ d)
+      ( triangular-neighborhood-Pseudometric-Space-WIP
+        ( A)
+        ( x)
+        ( y)
+        ( z)
+        ( left-summand-split-ℚ⁺ d)
+        ( right-summand-split-ℚ⁺ d)
+        ( Nyz (right-summand-split-ℚ⁺ d))
+        ( Nxy (left-summand-split-ℚ⁺ d)))
+```
+
+### Similarity in pseudometric spaces is an equivalence relation
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  where
+
+  is-equivalence-relation-sim-Pseudometric-Space-WIP :
+    is-equivalence-relation (sim-prop-Pseudometric-Space-WIP A)
+  is-equivalence-relation-sim-Pseudometric-Space-WIP =
+    ( refl-sim-Pseudometric-Space-WIP A) ,
+    ( symmetric-sim-Pseudometric-Space-WIP A) ,
+    ( transitive-sim-Pseudometric-Space-WIP A)
+
+  equivalence-sim-Pseudometric-Space-WIP :
+    equivalence-relation l2 (type-Pseudometric-Space-WIP A)
+  equivalence-sim-Pseudometric-Space-WIP =
+    ( sim-prop-Pseudometric-Space-WIP A) ,
+    ( is-equivalence-relation-sim-Pseudometric-Space-WIP)
+```
+
+### Similar elements are elements with the same neighbors
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  where
+
+  preserves-neighborhood-sim-Pseudometric-Space :
+    { x y : type-Pseudometric-Space-WIP A} →
+    ( sim-Pseudometric-Space-WIP A x y) →
+    ( d : ℚ⁺) (z : type-Pseudometric-Space-WIP A) →
+    neighborhood-Pseudometric-Space-WIP A d x z →
+    neighborhood-Pseudometric-Space-WIP A d y z
+  preserves-neighborhood-sim-Pseudometric-Space {x} {y} x≍y d z Nxz =
+    saturated-neighborhood-Pseudometric-Space-WIP
+      ( A)
+      ( d)
+      ( y)
+      ( z)
+      ( λ δ →
+        tr
+          ( is-upper-bound-dist-Pseudometric-Space-WIP A y z)
+          ( commutative-add-ℚ⁺ δ d)
+          ( triangular-neighborhood-Pseudometric-Space-WIP
+            ( A)
+            ( y)
+            ( x)
+            ( z)
+            ( δ)
+            ( d)
+            ( Nxz)
+            ( symmetric-neighborhood-Pseudometric-Space-WIP
+              ( A)
+              ( δ)
+              ( x)
+              ( y)
+              ( x≍y δ))))
+
+  iff-same-neighbors-sim-Pseudometric-Space :
+    { x y : type-Pseudometric-Space-WIP A} →
+    ( sim-Pseudometric-Space-WIP A x y) ↔
+    ( (d : ℚ⁺) (z : type-Pseudometric-Space-WIP A) →
+      neighborhood-Pseudometric-Space-WIP A d x z ↔
+      neighborhood-Pseudometric-Space-WIP A d y z)
+  iff-same-neighbors-sim-Pseudometric-Space =
+    ( λ x≍y d z →
+      ( preserves-neighborhood-sim-Pseudometric-Space x≍y d z) ,
+      ( preserves-neighborhood-sim-Pseudometric-Space
+        ( inv-sim-Pseudometric-Space-WIP A x≍y)
+        ( d)
+        ( z))) ,
+    ( λ same-neighbors d →
+      backward-implication
+        ( same-neighbors d _)
+        ( refl-sim-Pseudometric-Space-WIP A _ d))
+```
+
+### Similar elements are elements similar w.r.t the underlying rational neighborhood relation
+
+```agda
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space-WIP l1 l2)
+  where
+
+  iff-same-neighbors-same-neighborhood-Pseudometric-Space :
+    {x y : type-Pseudometric-Space-WIP A} →
+    ( (d : ℚ⁺) (z : type-Pseudometric-Space-WIP A) →
+      neighborhood-Pseudometric-Space-WIP A d x z ↔
+      neighborhood-Pseudometric-Space-WIP A d y z) ↔
+    ( sim-Rational-Neighborhood-Relation
+      ( neighborhood-prop-Pseudometric-Space-WIP A)
+      ( x)
+      ( y))
+  iff-same-neighbors-same-neighborhood-Pseudometric-Space =
+    ( λ H d z →
+      ( H d z) ,
+      ( inv-neighborhood-Pseudometric-Space-WIP A ∘
+        pr1 (H d z) ∘
+        inv-neighborhood-Pseudometric-Space-WIP A) ,
+      ( inv-neighborhood-Pseudometric-Space-WIP A ∘
+        pr2 (H d z) ∘
+        inv-neighborhood-Pseudometric-Space-WIP A)) ,
+    ( iff-left-neighbor-sim-Rational-Neighborhood-Relation
+      ( neighborhood-prop-Pseudometric-Space-WIP A))
+
+  iff-same-neighborhood-sim-Pseudometric-Space :
+    { x y : type-Pseudometric-Space-WIP A} →
+    ( sim-Pseudometric-Space-WIP A x y) ↔
+    ( sim-Rational-Neighborhood-Relation
+      ( neighborhood-prop-Pseudometric-Space-WIP A)
+      ( x)
+      ( y))
+  iff-same-neighborhood-sim-Pseudometric-Space =
+    ( iff-same-neighbors-same-neighborhood-Pseudometric-Space) ∘iff
+    ( iff-same-neighbors-sim-Pseudometric-Space A)
+```
diff --git a/src/metric-spaces/subspaces-metric-spaces-WIP.lagda.md b/src/metric-spaces/subspaces-metric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..268c6de0b9
--- /dev/null
+++ b/src/metric-spaces/subspaces-metric-spaces-WIP.lagda.md
@@ -0,0 +1,165 @@
+# Subspaces of metric spaces (WIP)
+
+```agda
+module metric-spaces.subspaces-metric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.logical-equivalences
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import metric-spaces.extensional-pseudometric-spaces-WIP
+open import metric-spaces.isometries-metric-spaces-WIP
+open import metric-spaces.metric-spaces-WIP
+open import metric-spaces.pseudometric-spaces-WIP
+open import metric-spaces.rational-neighborhoods
+open import metric-spaces.reflexive-rational-neighborhoods
+open import metric-spaces.saturated-rational-neighborhoods
+open import metric-spaces.symmetric-rational-neighborhoods
+open import metric-spaces.triangular-rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+[Subsets](foundation.subtypes.md) of
+[metric spaces](metric-spaces.metric-spaces.md) inherit the metric structure of
+their ambient space; these are
+{{#concept "metric subspaces" Agda=subspace-Metric-Space-WIP}} of metric spaces.
+
+The natural inclusion of subspace into its ambient space is an
+[isometry](metric-spaces.isometries-metric-spaces.md).
+
+## Definitions
+
+### Subsets of metric spaces
+
+```agda
+module _
+  (l : Level) {l1 l2 : Level} (A : Metric-Space-WIP l1 l2)
+  where
+
+  subset-Metric-Space-WIP : UU (lsuc l ⊔ l1)
+  subset-Metric-Space-WIP = subtype l (type-Metric-Space-WIP A)
+```
+
+### Metric subspace of a metric space
+
+```agda
+module _
+  {l l1 l2 : Level}
+  (A : Metric-Space-WIP l1 l2)
+  (S : subset-Metric-Space-WIP l A)
+  where
+
+  neighborhood-prop-subset-Metric-Space-WIP :
+    Rational-Neighborhood-Relation l2 (type-subtype S)
+  neighborhood-prop-subset-Metric-Space-WIP d x y =
+    neighborhood-prop-Metric-Space-WIP A d (pr1 x) (pr1 y)
+
+  is-reflexive-neighborhood-subset-Metric-Space-WIP :
+    is-reflexive-Rational-Neighborhood-Relation
+      neighborhood-prop-subset-Metric-Space-WIP
+  is-reflexive-neighborhood-subset-Metric-Space-WIP d x =
+    refl-neighborhood-Metric-Space-WIP A d (pr1 x)
+
+  is-symmetric-neighborhood-subset-Metric-Space-WIP :
+    is-symmetric-Rational-Neighborhood-Relation
+      neighborhood-prop-subset-Metric-Space-WIP
+  is-symmetric-neighborhood-subset-Metric-Space-WIP d x y =
+    symmetric-neighborhood-Metric-Space-WIP A d (pr1 x) (pr1 y)
+
+  is-triangular-neighborhood-subset-Metric-Space-WIP :
+    is-triangular-Rational-Neighborhood-Relation
+      neighborhood-prop-subset-Metric-Space-WIP
+  is-triangular-neighborhood-subset-Metric-Space-WIP x y z =
+    triangular-neighborhood-Metric-Space-WIP A (pr1 x) (pr1 y) (pr1 z)
+
+  is-saturated-neighborhood-subset-Metric-Space-WIP :
+    is-saturated-Rational-Neighborhood-Relation
+      neighborhood-prop-subset-Metric-Space-WIP
+  is-saturated-neighborhood-subset-Metric-Space-WIP ε x y =
+    saturated-neighborhood-Metric-Space-WIP
+      ( A)
+      ( ε)
+      ( pr1 x)
+      ( pr1 y)
+
+  pseudometric-subspace-Metric-Space-WIP :
+    Pseudometric-Space-WIP (l ⊔ l1) l2
+  pseudometric-subspace-Metric-Space-WIP =
+    ( type-subtype S) ,
+    ( neighborhood-prop-subset-Metric-Space-WIP ,
+      is-reflexive-neighborhood-subset-Metric-Space-WIP ,
+      is-symmetric-neighborhood-subset-Metric-Space-WIP ,
+      is-triangular-neighborhood-subset-Metric-Space-WIP ,
+      is-saturated-neighborhood-subset-Metric-Space-WIP)
+
+  is-extensional-pseudometric-subspace-Metric-Space-WIP :
+    is-extensional-Pseudometric-Space-WIP
+      pseudometric-subspace-Metric-Space-WIP
+  is-extensional-pseudometric-subspace-Metric-Space-WIP =
+    is-extensional-is-tight-Pseudometric-Space
+      ( pseudometric-subspace-Metric-Space-WIP)
+      ( λ x y →
+        eq-type-subtype S ∘
+        eq-sim-Metric-Space-WIP A (pr1 x) (pr1 y))
+
+  subspace-Metric-Space-WIP : Metric-Space-WIP (l ⊔ l1) l2
+  subspace-Metric-Space-WIP =
+    make-Metric-Space-WIP
+      ( type-subtype S)
+      ( neighborhood-prop-subset-Metric-Space-WIP)
+      ( is-reflexive-neighborhood-subset-Metric-Space-WIP)
+      ( is-symmetric-neighborhood-subset-Metric-Space-WIP)
+      ( is-triangular-neighborhood-subset-Metric-Space-WIP)
+      ( is-saturated-neighborhood-subset-Metric-Space-WIP)
+      ( is-extensional-pseudometric-subspace-Metric-Space-WIP)
+```
+
+### Inclusion of a metric subspace into its ambient space
+
+```agda
+module _
+  {l l1 l2 : Level}
+  (A : Metric-Space-WIP l1 l2)
+  (S : subset-Metric-Space-WIP l A)
+  where
+
+  inclusion-subspace-Metric-Space-WIP :
+    type-function-Metric-Space-WIP
+      ( subspace-Metric-Space-WIP A S)
+      ( A)
+  inclusion-subspace-Metric-Space-WIP = inclusion-subtype S
+```
+
+## Properties
+
+### The inclusion of a subspace into its ambient space is an isometry
+
+```agda
+module _
+  {l l1 l2 : Level}
+  (A : Metric-Space-WIP l1 l2)
+  (S : subset-Metric-Space-WIP l A)
+  where
+
+  is-isometry-inclusion-subspace-Metric-Space-WIP :
+    is-isometry-Metric-Space-WIP
+      (subspace-Metric-Space-WIP A S)
+      (A)
+      (inclusion-subspace-Metric-Space-WIP A S)
+  is-isometry-inclusion-subspace-Metric-Space-WIP d x y = id-iff
+
+  isometry-inclusion-subspace-Metric-Space-WIP :
+    isometry-Metric-Space-WIP (subspace-Metric-Space-WIP A S) A
+  isometry-inclusion-subspace-Metric-Space-WIP =
+    inclusion-subspace-Metric-Space-WIP A S ,
+    is-isometry-inclusion-subspace-Metric-Space-WIP
+```
diff --git a/src/metric-spaces/symmetric-rational-neighborhoods.lagda.md b/src/metric-spaces/symmetric-rational-neighborhoods.lagda.md
new file mode 100644
index 0000000000..c23e85b6b4
--- /dev/null
+++ b/src/metric-spaces/symmetric-rational-neighborhoods.lagda.md
@@ -0,0 +1,49 @@
+# Symmetric rational neighborhoods on types
+
+```agda
+module metric-spaces.symmetric-rational-neighborhoods where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.binary-relations
+open import foundation.function-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import metric-spaces.rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+A [rational neighborhood](metric-spaces.rational-neighborhoods.md) is
+{{#concept "symmetric" Disambiguation="rational neighborhood relation" Agda=is-symmetric-Rational-Neighborhood-Relation}}
+if all neighborhoods are symmetric.
+
+## Definitions
+
+### The property of being a symmetric rational neighborhood relation
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (B : Rational-Neighborhood-Relation l2 A)
+  where
+
+  is-symmetric-prop-Rational-Neighborhood-Relation : Prop (l1 ⊔ l2)
+  is-symmetric-prop-Rational-Neighborhood-Relation =
+    Π-Prop ℚ⁺ (is-symmetric-prop-Relation-Prop ∘ B)
+
+  is-symmetric-Rational-Neighborhood-Relation : UU (l1 ⊔ l2)
+  is-symmetric-Rational-Neighborhood-Relation =
+    type-Prop is-symmetric-prop-Rational-Neighborhood-Relation
+
+  is-prop-is-symmetric-Rational-Neighborhood-Relation :
+    is-prop is-symmetric-Rational-Neighborhood-Relation
+  is-prop-is-symmetric-Rational-Neighborhood-Relation =
+    is-prop-type-Prop is-symmetric-prop-Rational-Neighborhood-Relation
+```
diff --git a/src/metric-spaces/triangular-rational-neighborhoods.lagda.md b/src/metric-spaces/triangular-rational-neighborhoods.lagda.md
new file mode 100644
index 0000000000..df7ce99b3c
--- /dev/null
+++ b/src/metric-spaces/triangular-rational-neighborhoods.lagda.md
@@ -0,0 +1,94 @@
+# Triangular rational neighborhood relations on types
+
+```agda
+module metric-spaces.triangular-rational-neighborhoods where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.binary-relations
+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.monotonic-rational-neighborhoods
+open import metric-spaces.rational-neighborhoods
+open import metric-spaces.reflexive-rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+A [rational neighborhood relation](metric-spaces.premetric-structures.md) is
+{{#concept "triangular" Disambiguation="rational neighborhood relation" agda=is-triangular-Rational-Neighborhood-Relation}}
+if it is additively transitive, i.e., if any `d₂`-neighbor of a `d₁`-neighbor of
+an element is its `d₁ + d₂`-neighbor.
+
+## Definitions
+
+### The property of being a triangular rational neighborhood relation
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (B : Rational-Neighborhood-Relation l2 A)
+  where
+
+  is-triangular-prop-Rational-Neighborhood-Relation : Prop (l1 ⊔ l2)
+  is-triangular-prop-Rational-Neighborhood-Relation =
+    Π-Prop
+      ( A)
+      ( λ x →
+        ( Π-Prop
+          ( A)
+          ( λ y →
+            ( Π-Prop
+              ( A)
+              ( λ z →
+                Π-Prop
+                  ( ℚ⁺)
+                  ( λ d₁ →
+                    ( Π-Prop
+                      ( ℚ⁺)
+                      ( λ d₂ →
+                        hom-Prop
+                          ( B d₂ y z)
+                          ( hom-Prop
+                            ( B d₁ x y)
+                            ( B (d₁ +ℚ⁺ d₂) x z))))))))))
+
+  is-triangular-Rational-Neighborhood-Relation : UU (l1 ⊔ l2)
+  is-triangular-Rational-Neighborhood-Relation =
+    type-Prop is-triangular-prop-Rational-Neighborhood-Relation
+
+  is-prop-is-triangular-Rational-Neighborhood-Relation :
+    is-prop is-triangular-Rational-Neighborhood-Relation
+  is-prop-is-triangular-Rational-Neighborhood-Relation =
+    is-prop-type-Prop is-triangular-prop-Rational-Neighborhood-Relation
+```
+
+## Properties
+
+### Any triangular reflexive rational neighborhood relation is monotonic
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (B : Rational-Neighborhood-Relation l2 A)
+  (R : is-reflexive-Rational-Neighborhood-Relation B)
+  (T : is-triangular-Rational-Neighborhood-Relation B)
+  where
+
+  is-monotonic-is-reflexive-triangular-Rational-Neighborhood-Relation :
+    is-monotonic-Rational-Neighborhood-Relation B
+  is-monotonic-is-reflexive-triangular-Rational-Neighborhood-Relation
+    x y d₁ d₂ I H₁ =
+    tr
+      ( λ d → neighborhood-Rational-Neighborhood-Relation B d x y)
+      ( right-diff-law-add-ℚ⁺ d₁ d₂ I)
+      ( T x y y d₁ (le-diff-ℚ⁺ d₁ d₂ I) (R (le-diff-ℚ⁺ d₁ d₂ I) y) H₁)
+```
diff --git a/src/metric-spaces/uniformly-continuous-functions-metric-spaces-WIP.lagda.md b/src/metric-spaces/uniformly-continuous-functions-metric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..cb443ea946
--- /dev/null
+++ b/src/metric-spaces/uniformly-continuous-functions-metric-spaces-WIP.lagda.md
@@ -0,0 +1,238 @@
+# Uniformly continuous functions between metric spaces (WIP)
+
+```agda
+module metric-spaces.uniformly-continuous-functions-metric-spaces-WIP where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.inhabited-subtypes
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import logic.functoriality-existential-quantification
+
+open import metric-spaces.continuous-functions-metric-spaces-WIP
+open import metric-spaces.isometries-metric-spaces-WIP
+open import metric-spaces.metric-spaces-WIP
+open import metric-spaces.short-functions-metric-spaces-WIP
+```
+
+</details>
+
+## Idea
+
+A [function](metric-spaces.functions-metric-spaces.md) `f` between
+[metric spaces](metric-spaces.metric-spaces.md) `X` and `Y` is
+{{#concept "uniformly continuous" Disambiguation="function between metric spaces" WDID=Q741865 WD="uniform continuity" Agda=is-uniformly-continuous-function-Metric-Space-WIP}}
+if there exists a function `m : ℚ⁺ → ℚ⁺` such that for any `x : X`, whenever
+`x'` is in an `m ε`-neighborhood of `x`, `f x'` is in an `ε`-neighborhood of
+`f x`. The function `m` is called a modulus of uniform continuity of `f`.
+
+## Definitions
+
+### The property of being a uniformly continuous function
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (X : Metric-Space-WIP l1 l2)
+  (Y : Metric-Space-WIP l3 l4)
+  (f : type-function-Metric-Space-WIP X Y)
+  where
+
+  is-modulus-of-uniform-continuity-prop-function-Metric-Space-WIP :
+    (ℚ⁺ → ℚ⁺) → Prop (l1 ⊔ l2 ⊔ l4)
+  is-modulus-of-uniform-continuity-prop-function-Metric-Space-WIP m =
+    Π-Prop
+      ( type-Metric-Space-WIP X)
+      ( λ x →
+        is-modulus-of-continuity-at-point-prop-function-Metric-Space-WIP
+          X
+          Y
+          f
+          x
+          m)
+
+  modulus-of-uniform-continuity-function-Metric-Space-WIP : UU (l1 ⊔ l2 ⊔ l4)
+  modulus-of-uniform-continuity-function-Metric-Space-WIP =
+    type-subtype is-modulus-of-uniform-continuity-prop-function-Metric-Space-WIP
+
+  is-uniformly-continuous-prop-function-Metric-Space-WIP : Prop (l1 ⊔ l2 ⊔ l4)
+  is-uniformly-continuous-prop-function-Metric-Space-WIP =
+    is-inhabited-subtype-Prop
+      is-modulus-of-uniform-continuity-prop-function-Metric-Space-WIP
+
+  is-uniformly-continuous-function-Metric-Space-WIP : UU (l1 ⊔ l2 ⊔ l4)
+  is-uniformly-continuous-function-Metric-Space-WIP =
+    type-Prop is-uniformly-continuous-prop-function-Metric-Space-WIP
+```
+
+### The type of uniformly continuous functions between metric spaces
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (X : Metric-Space-WIP l1 l2)
+  (Y : Metric-Space-WIP l3 l4)
+  where
+
+  uniformly-continuous-function-Metric-Space-WIP : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  uniformly-continuous-function-Metric-Space-WIP =
+    type-subtype (is-uniformly-continuous-prop-function-Metric-Space-WIP X Y)
+
+  map-uniformly-continuous-function-Metric-Space-WIP :
+    uniformly-continuous-function-Metric-Space-WIP →
+    type-function-Metric-Space-WIP X Y
+  map-uniformly-continuous-function-Metric-Space-WIP = pr1
+
+  is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space-WIP :
+    (f : uniformly-continuous-function-Metric-Space-WIP) →
+    is-uniformly-continuous-function-Metric-Space-WIP
+      ( X)
+      ( Y)
+      ( map-uniformly-continuous-function-Metric-Space-WIP f)
+  is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space-WIP =
+    pr2
+```
+
+## Properties
+
+### Uniformly continuous functions are continuous at all points
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (X : Metric-Space-WIP l1 l2)
+  (Y : Metric-Space-WIP l3 l4)
+  (f : type-function-Metric-Space-WIP X Y)
+  where
+
+  is-continuous-at-point-is-uniformly-continuous-function-Metric-Space-WIP :
+    is-uniformly-continuous-function-Metric-Space-WIP X Y f →
+    (x : type-Metric-Space-WIP X) →
+    is-continuous-at-point-function-Metric-Space-WIP X Y f x
+  is-continuous-at-point-is-uniformly-continuous-function-Metric-Space-WIP H x =
+    elim-exists
+      ( is-continuous-at-point-prop-function-Metric-Space-WIP X Y f x)
+      ( λ m K → intro-exists m (K x))
+      ( H)
+```
+
+### The identity function is uniformly continuous
+
+```agda
+module _
+  {l1 l2 : Level} (X : Metric-Space-WIP l1 l2)
+  where
+
+  is-uniformly-continuous-id-Metric-Space-WIP :
+    is-uniformly-continuous-function-Metric-Space-WIP X X id
+  is-uniformly-continuous-id-Metric-Space-WIP =
+    intro-exists id (λ _ _ _ → id)
+```
+
+### The composition of uniformly continuous functions is uniformly continuous
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  (X : Metric-Space-WIP l1 l2)
+  (Y : Metric-Space-WIP l3 l4)
+  (Z : Metric-Space-WIP l5 l6)
+  where
+
+  is-uniformly-continuous-comp-function-Metric-Space-WIP :
+    (g : type-function-Metric-Space-WIP Y Z) →
+    (f : type-function-Metric-Space-WIP X Y) →
+    is-uniformly-continuous-function-Metric-Space-WIP Y Z g →
+    is-uniformly-continuous-function-Metric-Space-WIP X Y f →
+    is-uniformly-continuous-function-Metric-Space-WIP X Z (g ∘ f)
+  is-uniformly-continuous-comp-function-Metric-Space-WIP g f H K =
+    do
+      mg , is-modulus-uniform-mg ← H
+      mf , is-modulus-uniform-mf ← K
+      intro-exists
+        ( mf ∘ mg)
+        ( λ x ε x' →
+          is-modulus-uniform-mg (f x) ε (f x') ∘
+          is-modulus-uniform-mf x (mg ε) x')
+    where
+      open
+        do-syntax-trunc-Prop
+          ( is-uniformly-continuous-prop-function-Metric-Space-WIP X Z (g ∘ f))
+
+  comp-uniformly-continuous-function-Metric-Space-WIP :
+    uniformly-continuous-function-Metric-Space-WIP Y Z →
+    uniformly-continuous-function-Metric-Space-WIP X Y →
+    uniformly-continuous-function-Metric-Space-WIP X Z
+  comp-uniformly-continuous-function-Metric-Space-WIP g f =
+    ( map-uniformly-continuous-function-Metric-Space-WIP Y Z g ∘
+      map-uniformly-continuous-function-Metric-Space-WIP X Y f) ,
+    ( is-uniformly-continuous-comp-function-Metric-Space-WIP
+      ( map-uniformly-continuous-function-Metric-Space-WIP Y Z g)
+      ( map-uniformly-continuous-function-Metric-Space-WIP X Y f)
+      ( is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space-WIP
+        ( Y)
+        ( Z)
+        ( g))
+      ( is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space-WIP
+        ( X)
+        ( Y)
+        ( f)))
+```
+
+### Short maps are uniformly continuous
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (A : Metric-Space-WIP l1 l2)
+  (B : Metric-Space-WIP l3 l4)
+  where
+
+  is-uniformly-continuous-is-short-function-Metric-Space-WIP :
+    (f : type-function-Metric-Space-WIP A B) →
+    is-short-function-Metric-Space-WIP A B f →
+    is-uniformly-continuous-function-Metric-Space-WIP A B f
+  is-uniformly-continuous-is-short-function-Metric-Space-WIP f H =
+    intro-exists id (λ x d → H d x)
+
+  uniformly-continuous-short-function-Metric-Space :
+    short-function-Metric-Space-WIP A B →
+    uniformly-continuous-function-Metric-Space-WIP A B
+  uniformly-continuous-short-function-Metric-Space =
+    tot is-uniformly-continuous-is-short-function-Metric-Space-WIP
+```
+
+### Isometries are uniformly continuous
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (A : Metric-Space-WIP l1 l2) (B : Metric-Space-WIP l3 l4)
+  where
+
+  is-uniformly-continuous-is-isometry-Metric-Space-WIP :
+    (f : type-function-Metric-Space-WIP A B) →
+    is-isometry-Metric-Space-WIP A B f →
+    is-uniformly-continuous-function-Metric-Space-WIP A B f
+  is-uniformly-continuous-is-isometry-Metric-Space-WIP f =
+    is-uniformly-continuous-is-short-function-Metric-Space-WIP A B f ∘
+    is-short-is-isometry-Metric-Space-WIP A B f
+
+  uniformly-continuous-isometry-Metric-Space :
+    isometry-Metric-Space-WIP A B →
+    uniformly-continuous-function-Metric-Space-WIP A B
+  uniformly-continuous-isometry-Metric-Space =
+    tot is-uniformly-continuous-is-isometry-Metric-Space-WIP
+```