diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md
index 0bf9402bb1..f46d7d8dea 100644
--- a/src/metric-spaces.lagda.md
+++ b/src/metric-spaces.lagda.md
@@ -86,15 +86,19 @@ open import metric-spaces.metric-space-of-short-functions-metric-spaces public
 open import metric-spaces.metric-spaces 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.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.premetric-spaces public
+open import metric-spaces.premetric-spaces-WIP public
 open import metric-spaces.premetric-structures public
 open import metric-spaces.pseudometric-spaces public
 open import metric-spaces.pseudometric-structures public
+open import metric-spaces.rational-neighborhoods 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.sequences-metric-spaces public
@@ -102,9 +106,12 @@ 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-premetric-spaces public
+open import metric-spaces.similarity-of-elements-premetric-spaces public
 open import metric-spaces.subspaces-metric-spaces 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-premetric-spaces public
 ```
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..e1f53e6439
--- /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="premetric" Agda=is-monotonic-Rational-Neighborhood-Relation}}
+if any `d₁`-neighborhoods are `d₂`-neighborhoods for `d₁ < d₂`.
+
+## Definitions
+
+### The property of being a monotonic premetric structure
+
+```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/premetric-spaces-WIP.lagda.md b/src/metric-spaces/premetric-spaces-WIP.lagda.md
new file mode 100644
index 0000000000..c13c35f20b
--- /dev/null
+++ b/src/metric-spaces/premetric-spaces-WIP.lagda.md
@@ -0,0 +1,184 @@
+# Premetric spaces (WIP)
+
+```agda
+module metric-spaces.premetric-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.symmetric-rational-neighborhoods
+open import metric-spaces.triangular-rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+A {{#concept "premetric space" Agda=Premetric-Space-WIP}} is a type equipped
+with [reflexive](metric-spaces.reflexive-rational-neighborhoods.md),
+[symmetric](metric-spaces.symmetric-rational-neighborhoods.md) and
+[triangular](metric-spaces.triangular-rational-neighborhoods.md)
+[rational neighborhood relation](metric-spaces.rational-neighborhoods.md)
+
+Given a premetric `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 with respect to a premetric structure"}}
+on the distance between `x` and `y` with respect to the premetric.
+
+## 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-premetric-prop-Rational-Neighborhood-Relation : Prop (l1 ⊔ l2)
+  is-premetric-prop-Rational-Neighborhood-Relation =
+    product-Prop
+      ( is-reflexive-prop-Rational-Neighborhood-Relation B)
+      ( product-Prop
+        ( is-symmetric-prop-Rational-Neighborhood-Relation B)
+        ( is-triangular-prop-Rational-Neighborhood-Relation B))
+
+  is-premetric-Rational-Neighborhood-Relation : UU (l1 ⊔ l2)
+  is-premetric-Rational-Neighborhood-Relation =
+    type-Prop is-premetric-prop-Rational-Neighborhood-Relation
+
+  is-prop-is-premetric-Rational-Neighborhood-Relation :
+    is-prop is-premetric-Rational-Neighborhood-Relation
+  is-prop-is-premetric-Rational-Neighborhood-Relation =
+    is-prop-type-Prop (is-premetric-prop-Rational-Neighborhood-Relation)
+
+Premetric-Structure :
+  {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2)
+Premetric-Structure l2 A =
+  type-subtype (is-premetric-prop-Rational-Neighborhood-Relation A {l2})
+```
+
+### Premetric spaces
+
+```agda
+Premetric-Space-WIP : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Premetric-Space-WIP l1 l2 = Σ (UU l1) (Premetric-Structure l2)
+
+module _
+  {l1 l2 : Level} (A : Premetric-Space-WIP l1 l2)
+  where
+
+  type-Premetric-Space-WIP : UU l1
+  type-Premetric-Space-WIP = pr1 A
+
+  structure-Premetric-Space-WIP :
+    Premetric-Structure l2 type-Premetric-Space-WIP
+  structure-Premetric-Space-WIP = pr2 A
+
+  neighborhood-prop-Premetric-Space-WIP :
+    Rational-Neighborhood-Relation l2 type-Premetric-Space-WIP
+  neighborhood-prop-Premetric-Space-WIP =
+    pr1 structure-Premetric-Space-WIP
+
+  neighborhood-Premetric-Space-WIP :
+    ℚ⁺ → Relation l2 type-Premetric-Space-WIP
+  neighborhood-Premetric-Space-WIP =
+    neighborhood-Rational-Neighborhood-Relation
+      neighborhood-prop-Premetric-Space-WIP
+
+  is-prop-neighborhood-Premetric-Space-WIP :
+    (d : ℚ⁺) (x y : type-Premetric-Space-WIP) →
+    is-prop (neighborhood-Premetric-Space-WIP d x y)
+  is-prop-neighborhood-Premetric-Space-WIP =
+    is-prop-neighborhood-Rational-Neighborhood-Relation
+      neighborhood-prop-Premetric-Space-WIP
+
+  is-upper-bound-dist-prop-Premetric-Space-WIP :
+    (x y : type-Premetric-Space-WIP) → ℚ⁺ → Prop l2
+  is-upper-bound-dist-prop-Premetric-Space-WIP x y d =
+    neighborhood-prop-Premetric-Space-WIP d x y
+
+  is-upper-bound-dist-Premetric-Space-WIP :
+    (x y : type-Premetric-Space-WIP) → ℚ⁺ → UU l2
+  is-upper-bound-dist-Premetric-Space-WIP x y d =
+    neighborhood-Premetric-Space-WIP d x y
+
+  is-prop-is-upper-bound-dist-Premetric-Space-WIP :
+    (x y : type-Premetric-Space-WIP) (d : ℚ⁺) →
+    is-prop (is-upper-bound-dist-Premetric-Space-WIP x y d)
+  is-prop-is-upper-bound-dist-Premetric-Space-WIP x y d =
+    is-prop-neighborhood-Premetric-Space-WIP d x y
+
+  is-premetric-neighborhood-Premetric-Space-WIP :
+    is-premetric-Rational-Neighborhood-Relation
+      type-Premetric-Space-WIP
+      neighborhood-prop-Premetric-Space-WIP
+  is-premetric-neighborhood-Premetric-Space-WIP =
+    pr2 structure-Premetric-Space-WIP
+
+  refl-neighborhood-Premetric-Space-WIP :
+    (d : ℚ⁺) (x : type-Premetric-Space-WIP) →
+    neighborhood-Premetric-Space-WIP d x x
+  refl-neighborhood-Premetric-Space-WIP =
+    pr1 is-premetric-neighborhood-Premetric-Space-WIP
+
+  symmetric-neighborhood-Premetric-Space-WIP :
+    (d : ℚ⁺) (x y : type-Premetric-Space-WIP) →
+    neighborhood-Premetric-Space-WIP d x y →
+    neighborhood-Premetric-Space-WIP d y x
+  symmetric-neighborhood-Premetric-Space-WIP =
+    pr1 (pr2 is-premetric-neighborhood-Premetric-Space-WIP)
+
+  inv-neighborhood-Premetric-Space-WIP :
+    {d : ℚ⁺} {x y : type-Premetric-Space-WIP} →
+    neighborhood-Premetric-Space-WIP d x y →
+    neighborhood-Premetric-Space-WIP d y x
+  inv-neighborhood-Premetric-Space-WIP {d} {x} {y} =
+    symmetric-neighborhood-Premetric-Space-WIP d x y
+
+  triangular-neighborhood-Premetric-Space-WIP :
+    (x y z : type-Premetric-Space-WIP) (d₁ d₂ : ℚ⁺) →
+    neighborhood-Premetric-Space-WIP d₂ y z →
+    neighborhood-Premetric-Space-WIP d₁ x y →
+    neighborhood-Premetric-Space-WIP (d₁ +ℚ⁺ d₂) x z
+  triangular-neighborhood-Premetric-Space-WIP =
+    pr2 (pr2 is-premetric-neighborhood-Premetric-Space-WIP)
+
+  monotonic-neighborhood-Premetric-Space-WIP :
+    (x y : type-Premetric-Space-WIP) (d₁ d₂ : ℚ⁺) →
+    le-ℚ⁺ d₁ d₂ →
+    neighborhood-Premetric-Space-WIP d₁ x y →
+    neighborhood-Premetric-Space-WIP d₂ x y
+  monotonic-neighborhood-Premetric-Space-WIP =
+    is-monotonic-is-reflexive-triangular-Rational-Neighborhood-Relation
+      neighborhood-prop-Premetric-Space-WIP
+      refl-neighborhood-Premetric-Space-WIP
+      triangular-neighborhood-Premetric-Space-WIP
+```
diff --git a/src/metric-spaces/rational-neighborhoods.lagda.md b/src/metric-spaces/rational-neighborhoods.lagda.md
new file mode 100644
index 0000000000..f3f7c1dff9
--- /dev/null
+++ b/src/metric-spaces/rational-neighborhoods.lagda.md
@@ -0,0 +1,54 @@
+# 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.propositions
+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).
+
+## 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)
+```
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..a9858ba7aa
--- /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="premetric" 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/similarity-of-elements-premetric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-premetric-spaces.lagda.md
new file mode 100644
index 0000000000..a65ce14c61
--- /dev/null
+++ b/src/metric-spaces/similarity-of-elements-premetric-spaces.lagda.md
@@ -0,0 +1,136 @@
+# Similarity of elements in premetric spaces
+
+```agda
+module metric-spaces.similarity-of-elements-premetric-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.identity-types
+open import foundation.propositions
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import metric-spaces.premetric-spaces-WIP
+```
+
+</details>
+
+## Idea
+
+Two elements `x y` of a [premetric space](metric-spaces.premetric-spaces-WIP.md)
+are
+{{#concept "similar" Disambiguation="elements of a premetric space" Agda=sim-Premetric-Space}}
+if they share all neighborhoods. Similarity in premetric spaces is an
+[equivalence relation](foundation.equivalence-relations.md).
+
+## Definitions
+
+### Neighborhood similarity relation in premetric spaces
+
+```agda
+module _
+  {l1 l2 : Level} (A : Premetric-Space-WIP l1 l2)
+  where
+
+  sim-prop-Premetric-Space-WIP :
+    Relation-Prop l2 (type-Premetric-Space-WIP A)
+  sim-prop-Premetric-Space-WIP x y =
+    Π-Prop ℚ⁺ (is-upper-bound-dist-prop-Premetric-Space-WIP A x y)
+
+  sim-Premetric-Space-WIP :
+    Relation l2 (type-Premetric-Space-WIP A)
+  sim-Premetric-Space-WIP =
+    type-Relation-Prop sim-prop-Premetric-Space-WIP
+
+  is-prop-sim-Premetric-Space-WIP :
+    (x y : type-Premetric-Space-WIP A) →
+    is-prop (sim-Premetric-Space-WIP x y)
+  is-prop-sim-Premetric-Space-WIP =
+    is-prop-type-Relation-Prop sim-prop-Premetric-Space-WIP
+```
+
+## Properties
+
+### Similarity in premetric spaces is reflexive
+
+```agda
+module _
+  {l1 l2 : Level} (A : Premetric-Space-WIP l1 l2)
+  where
+
+  refl-sim-Premetric-Space-WIP :
+    (x : type-Premetric-Space-WIP A) →
+    sim-Premetric-Space-WIP A x x
+  refl-sim-Premetric-Space-WIP x d =
+    refl-neighborhood-Premetric-Space-WIP A d x
+```
+
+### Similarity in premetric spaces is symmetric
+
+```agda
+module _
+  {l1 l2 : Level} (A : Premetric-Space-WIP l1 l2)
+  where
+
+  symmetric-sim-Premetric-Space-WIP :
+    (x y : type-Premetric-Space-WIP A) →
+    sim-Premetric-Space-WIP A x y →
+    sim-Premetric-Space-WIP A y x
+  symmetric-sim-Premetric-Space-WIP x y Nxy d =
+    symmetric-neighborhood-Premetric-Space-WIP A d x y (Nxy d)
+```
+
+### Similarity in premetric spaces is transitive
+
+```agda
+module _
+  {l1 l2 : Level} (A : Premetric-Space-WIP l1 l2)
+  where
+
+  transitive-sim-Premetric-Space-WIP :
+    (x y z : type-Premetric-Space-WIP A) →
+    sim-Premetric-Space-WIP A y z →
+    sim-Premetric-Space-WIP A x y →
+    sim-Premetric-Space-WIP A x z
+  transitive-sim-Premetric-Space-WIP x y z Nyz Nxy d =
+    tr
+      ( is-upper-bound-dist-Premetric-Space-WIP A x z)
+      ( eq-add-split-ℚ⁺ d)
+      ( triangular-neighborhood-Premetric-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 premetric spaces is an equivalence relation
+
+```agda
+module _
+  {l1 l2 : Level} (A : Premetric-Space-WIP l1 l2)
+  where
+
+  is-equivalence-relation-sim-Premetric-Space :
+    is-equivalence-relation (sim-prop-Premetric-Space-WIP A)
+  is-equivalence-relation-sim-Premetric-Space =
+    ( refl-sim-Premetric-Space-WIP A) ,
+    ( symmetric-sim-Premetric-Space-WIP A) ,
+    ( transitive-sim-Premetric-Space-WIP A)
+
+  equivalence-sim-Premetric-Space :
+    equivalence-relation l2 (type-Premetric-Space-WIP A)
+  equivalence-sim-Premetric-Space =
+    ( sim-prop-Premetric-Space-WIP A) ,
+    ( is-equivalence-relation-sim-Premetric-Space)
+```
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..3ba14632e6
--- /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="premetric" 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..b9c04c4d0e
--- /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 premetric 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₁)
+```