From d5040e066108fefd1cffe383b0c4709e9e5455a0 Mon Sep 17 00:00:00 2001
From: malarbol <malarbol+git@gmail.com>
Date: Thu, 8 May 2025 21:51:00 +0200
Subject: [PATCH 1/5] large premetric spaces

---
 src/metric-spaces.lagda.md                    |   2 +
 .../large-premetric-spaces.lagda.md           | 121 ++++++++++++++++++
 .../large-rational-neighborhoods.lagda.md     |  86 +++++++++++++
 3 files changed, 209 insertions(+)
 create mode 100644 src/metric-spaces/large-premetric-spaces.lagda.md
 create mode 100644 src/metric-spaces/large-rational-neighborhoods.lagda.md

diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md
index 0bf9402bb1..237ec81f93 100644
--- a/src/metric-spaces.lagda.md
+++ b/src/metric-spaces.lagda.md
@@ -69,6 +69,8 @@ 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-premetric-spaces public
+open import metric-spaces.large-premetric-spaces public
+open import metric-spaces.large-rational-neighborhoods public
 open import metric-spaces.limits-of-cauchy-approximations-premetric-spaces public
 open import metric-spaces.limits-of-sequences-metric-spaces public
 open import metric-spaces.limits-of-sequences-premetric-spaces public
diff --git a/src/metric-spaces/large-premetric-spaces.lagda.md b/src/metric-spaces/large-premetric-spaces.lagda.md
new file mode 100644
index 0000000000..cc0a45ac9b
--- /dev/null
+++ b/src/metric-spaces/large-premetric-spaces.lagda.md
@@ -0,0 +1,121 @@
+# Large premetric spaces
+
+```agda
+module metric-spaces.large-premetric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.identity-types
+open import foundation.large-binary-relations
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import metric-spaces.large-rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+A {{concept "large premetric space" Agda-Large-Premetric-Space}} is a family of
+types indexed by universe levels equipped with a reflexive, symmetric and
+triangular
+[large rational neighborhood](metric-spaces.large-rational-neighborhoods.md).
+
+## Definitions
+
+```agda
+record
+  Large-Premetric-Space (α : Level → Level) (β : Level → Level → Level) : UUω
+  where
+  constructor
+    make-Large-Premetric-Space
+  field
+    type-Large-Premetric-Space : (l : Level) → UU (α l)
+    neighborhood-Large-Premetric-Space :
+      Large-Rational-Neighborhood β type-Large-Premetric-Space
+    refl-neighborhood-Large-Premetric-Space :
+      is-reflexive-Large-Rational-Neighborhood
+        neighborhood-Large-Premetric-Space
+    symmetric-neighborhood-Large-Premetric-Space :
+      is-symmetric-Large-Rational-Neighborhood
+        neighborhood-Large-Premetric-Space
+    triangular-neighborhood-Large-Premetric-Space :
+      is-triangular-Large-Rational-Neighborhood
+        neighborhood-Large-Premetric-Space
+
+open Large-Premetric-Space public
+
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (M : Large-Premetric-Space α β)
+  where
+
+  is-in-neighborhood-Large-Premetric-Space :
+    (d : ℚ⁺) {l1 l2 : Level} →
+    type-Large-Premetric-Space M l1 →
+    type-Large-Premetric-Space M l2 →
+    UU (β l1 l2)
+  is-in-neighborhood-Large-Premetric-Space =
+    is-in-neighborhood-Large-Rational-Neighborhood
+      (neighborhood-Large-Premetric-Space M)
+
+  is-prop-is-in-neighborhood-Large-Premetric-Space :
+    (d : ℚ⁺) {l1 l2 : Level}
+    (x : type-Large-Premetric-Space M l1)
+    (y : type-Large-Premetric-Space M l2) →
+    is-prop (is-in-neighborhood-Large-Premetric-Space d x y)
+  is-prop-is-in-neighborhood-Large-Premetric-Space =
+    is-prop-is-in-neighborhood-Large-Rational-Neighborhood
+      (neighborhood-Large-Premetric-Space M)
+
+  is-upper-bound-dist-prop-Large-Premetric-Space :
+    {l1 l2 : Level}
+    (x : type-Large-Premetric-Space M l1)
+    (y : type-Large-Premetric-Space M l2) →
+    ℚ⁺ →
+    Prop (β l1 l2)
+  is-upper-bound-dist-prop-Large-Premetric-Space x y d =
+    neighborhood-Large-Premetric-Space M d x y
+
+  is-upper-bound-dist-Large-Premetric-Space :
+    {l1 l2 : Level}
+    (x : type-Large-Premetric-Space M l1)
+    (y : type-Large-Premetric-Space M l2) →
+    ℚ⁺ →
+    UU (β l1 l2)
+  is-upper-bound-dist-Large-Premetric-Space x y d =
+    is-in-neighborhood-Large-Premetric-Space d x y
+
+  is-prop-is-upper-bound-dist-Large-Premetric-Space :
+    {l1 l2 : Level}
+    (x : type-Large-Premetric-Space M l1)
+    (y : type-Large-Premetric-Space M l2) →
+    (d : ℚ⁺) →
+    is-prop (is-upper-bound-dist-Large-Premetric-Space x y d)
+  is-prop-is-upper-bound-dist-Large-Premetric-Space x y d =
+    is-prop-is-in-neighborhood-Large-Premetric-Space d x y
+```
+
+## Properties
+
+### Equal elements of a large premetric space are neighors
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (M : Large-Premetric-Space α β)
+  where
+
+  neighborhood-eq-Large-Premetric-Space :
+    {l : Level} (x y : type-Large-Premetric-Space M l) →
+    (x ＝ y) →
+    (d : ℚ⁺) →
+    is-in-neighborhood-Large-Premetric-Space M d x y
+  neighborhood-eq-Large-Premetric-Space x .x refl d =
+    refl-neighborhood-Large-Premetric-Space M d x
+```
diff --git a/src/metric-spaces/large-rational-neighborhoods.lagda.md b/src/metric-spaces/large-rational-neighborhoods.lagda.md
new file mode 100644
index 0000000000..80ede8f525
--- /dev/null
+++ b/src/metric-spaces/large-rational-neighborhoods.lagda.md
@@ -0,0 +1,86 @@
+# Large rational neighborhoods on types
+
+```agda
+module metric-spaces.large-rational-neighborhoods where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.large-binary-relations
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A {{concept "large rational neighborhood" Agda=Large-Rational-Neighborhood}} on
+a family of types indexed by universe levels `A` is a family of
+[large relations](foundation.large-binary-relations.md) on `A` indexed by the
+[positive rational numbers](elementary-number-theory.positive-rational-numbers.md).
+
+## Definitions
+
+```agda
+module _
+  {α : Level → Level} (β : Level → Level → Level)
+  (A : (l : Level) → UU (α l))
+  where
+
+  Large-Rational-Neighborhood : UUω
+  Large-Rational-Neighborhood =
+    ℚ⁺ → Large-Relation-Prop β A
+
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  {A : (l : Level) → UU (α l)}
+  (N : Large-Rational-Neighborhood β A)
+  (d : ℚ⁺) {l1 l2 : Level} (x : A l1) (y : A l2)
+  where
+
+  neighborhood-Large-Rational-Neighborhood : Prop (β l1 l2)
+  neighborhood-Large-Rational-Neighborhood = N d x y
+
+  is-in-neighborhood-Large-Rational-Neighborhood : UU (β l1 l2)
+  is-in-neighborhood-Large-Rational-Neighborhood =
+    type-Prop neighborhood-Large-Rational-Neighborhood
+
+  is-prop-is-in-neighborhood-Large-Rational-Neighborhood :
+    is-prop is-in-neighborhood-Large-Rational-Neighborhood
+  is-prop-is-in-neighborhood-Large-Rational-Neighborhood =
+    is-prop-type-Prop neighborhood-Large-Rational-Neighborhood
+```
+
+## Properties
+
+### Specification of properties of rational neighborhoods
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  {A : (l : Level) → UU (α l)}
+  (N : Large-Rational-Neighborhood β A)
+  where
+
+  is-reflexive-Large-Rational-Neighborhood : UUω
+  is-reflexive-Large-Rational-Neighborhood =
+    (d : ℚ⁺) {l : Level} (x : A l) →
+    is-in-neighborhood-Large-Rational-Neighborhood N d x x
+
+  is-symmetric-Large-Rational-Neighborhood : UUω
+  is-symmetric-Large-Rational-Neighborhood =
+    (d : ℚ⁺) {l1 l2 : Level} (x : A l1) (y : A l2) →
+    is-in-neighborhood-Large-Rational-Neighborhood N d x y →
+    is-in-neighborhood-Large-Rational-Neighborhood N d y x
+
+  is-triangular-Large-Rational-Neighborhood : UUω
+  is-triangular-Large-Rational-Neighborhood =
+    (ε δ : ℚ⁺) {l1 l2 l3 : Level} (x : A l1) (y : A l2) (z : A l3) →
+    is-in-neighborhood-Large-Rational-Neighborhood N δ y z →
+    is-in-neighborhood-Large-Rational-Neighborhood N ε x y →
+    is-in-neighborhood-Large-Rational-Neighborhood N (ε +ℚ⁺ δ) x z
+```

From a5f93b9f1038b86b8ab97642ea0f6f3124b79b75 Mon Sep 17 00:00:00 2001
From: malarbol <malarbol+git@gmail.com>
Date: Thu, 8 May 2025 22:41:23 +0200
Subject: [PATCH 2/5] similarity of elements in large premetric spaces

---
 src/metric-spaces.lagda.md                    |   1 +
 ...f-elements-large-premetric-spaces.lagda.md | 141 ++++++++++++++++++
 2 files changed, 142 insertions(+)
 create mode 100644 src/metric-spaces/similarity-of-elements-large-premetric-spaces.lagda.md

diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md
index 237ec81f93..a4ed46072a 100644
--- a/src/metric-spaces.lagda.md
+++ b/src/metric-spaces.lagda.md
@@ -104,6 +104,7 @@ 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-large-premetric-spaces public
 open import metric-spaces.subspaces-metric-spaces public
 open import metric-spaces.symmetric-premetric-structures public
 open import metric-spaces.triangular-premetric-structures public
diff --git a/src/metric-spaces/similarity-of-elements-large-premetric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-large-premetric-spaces.lagda.md
new file mode 100644
index 0000000000..489443350f
--- /dev/null
+++ b/src/metric-spaces/similarity-of-elements-large-premetric-spaces.lagda.md
@@ -0,0 +1,141 @@
+# Similarity of elements in large premetric spaces
+
+```agda
+module metric-spaces.similarity-of-elements-large-premetric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.identity-types
+open import foundation.large-binary-relations
+open import foundation.propositions
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import metric-spaces.large-premetric-spaces
+open import metric-spaces.large-rational-neighborhoods
+```
+
+</details>
+
+## Idea
+
+Two elements `x y` of a
+[large premetric space](metric-spaces.large-premetric-spaces.md) are
+{{#concept "similar" Disambiguation="elements of a large premetric space" Agda=sim-element-Large-Premetric-Space}}
+if their distance is bounded by all
+[positive rational numbers](elementary-number-theory.positive-rational-numbers.md).
+Similarity of element sin a large premetric space is reflexive, symmetric and
+transitive.
+
+## Definitions
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (M : Large-Premetric-Space α β)
+  {l1 l2 : Level}
+  (x : type-Large-Premetric-Space M l1)
+  (y : type-Large-Premetric-Space M l2)
+  where
+
+  sim-prop-element-Large-Premetric-Space : Prop (β l1 l2)
+  sim-prop-element-Large-Premetric-Space =
+    Π-Prop
+      ( ℚ⁺)
+      ( is-upper-bound-dist-prop-Large-Premetric-Space M x y)
+
+  sim-element-Large-Premetric-Space : UU (β l1 l2)
+  sim-element-Large-Premetric-Space =
+    type-Prop sim-prop-element-Large-Premetric-Space
+
+  is-prop-sim-element-Large-Premetric-Space :
+    is-prop sim-element-Large-Premetric-Space
+  is-prop-sim-element-Large-Premetric-Space =
+    is-prop-type-Prop sim-prop-element-Large-Premetric-Space
+```
+
+## Properties
+
+### Similarity of elements in large premetric spaces is reflexive
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (M : Large-Premetric-Space α β)
+  {l : Level} (x : type-Large-Premetric-Space M l)
+  where
+
+  sim-eq-element-Large-Premetric-Space :
+    (y : type-Large-Premetric-Space M l) →
+    x ＝ y →
+    sim-element-Large-Premetric-Space M x y
+  sim-eq-element-Large-Premetric-Space =
+    neighborhood-eq-Large-Premetric-Space M x
+
+  refl-sim-element-Large-Premetric-Space :
+    sim-element-Large-Premetric-Space M x x
+  refl-sim-element-Large-Premetric-Space =
+    sim-eq-element-Large-Premetric-Space x refl
+```
+
+### Similarity of elements in large premetric spaces is symmetric
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (M : Large-Premetric-Space α β)
+  where
+
+  symmetric-sim-element-Large-Premetric-Space :
+    {l1 l2 : Level}
+    (x : type-Large-Premetric-Space M l1)
+    (y : type-Large-Premetric-Space M l2) →
+    sim-element-Large-Premetric-Space M x y →
+    sim-element-Large-Premetric-Space M y x
+  symmetric-sim-element-Large-Premetric-Space x y x~y d =
+    symmetric-neighborhood-Large-Premetric-Space M d x y (x~y d)
+
+  inv-sim-element-Large-Premetric-Space :
+    {l1 l2 : Level}
+    {x : type-Large-Premetric-Space M l1}
+    {y : type-Large-Premetric-Space M l2} →
+    sim-element-Large-Premetric-Space M x y →
+    sim-element-Large-Premetric-Space M y x
+  inv-sim-element-Large-Premetric-Space {x = x} {y = y} =
+    symmetric-sim-element-Large-Premetric-Space x y
+```
+
+### Similarity of elements in large premetric spaces is transitive
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (M : Large-Premetric-Space α β)
+  where
+
+  transitive-sim-element-Large-Premetric-Space :
+    {l1 l2 l3 : Level}
+    (x : type-Large-Premetric-Space M l1)
+    (y : type-Large-Premetric-Space M l2)
+    (z : type-Large-Premetric-Space M l3) →
+    sim-element-Large-Premetric-Space M y z →
+    sim-element-Large-Premetric-Space M x y →
+    sim-element-Large-Premetric-Space M x z
+  transitive-sim-element-Large-Premetric-Space x y z y~z x~y d =
+    tr
+      ( is-upper-bound-dist-Large-Premetric-Space M x z)
+      ( eq-add-split-ℚ⁺ d)
+      ( triangular-neighborhood-Large-Premetric-Space
+        ( M)
+        ( left-summand-split-ℚ⁺ d)
+        ( right-summand-split-ℚ⁺ d)
+        ( x)
+        ( y)
+        ( z)
+        ( y~z (right-summand-split-ℚ⁺ d))
+        ( x~y (left-summand-split-ℚ⁺ d)))
+```

From 7caba3e3dd667c8f8d82a5fb78031d48821915da Mon Sep 17 00:00:00 2001
From: malarbol <malarbol+git@gmail.com>
Date: Thu, 8 May 2025 23:30:59 +0200
Subject: [PATCH 3/5] typo

---
 src/metric-spaces/large-premetric-spaces.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/metric-spaces/large-premetric-spaces.lagda.md b/src/metric-spaces/large-premetric-spaces.lagda.md
index cc0a45ac9b..19e2c2ccee 100644
--- a/src/metric-spaces/large-premetric-spaces.lagda.md
+++ b/src/metric-spaces/large-premetric-spaces.lagda.md
@@ -21,7 +21,7 @@ open import metric-spaces.large-rational-neighborhoods
 
 ## Idea
 
-A {{concept "large premetric space" Agda-Large-Premetric-Space}} is a family of
+A {{concept "large premetric space" Agda=Large-Premetric-Space}} is a family of
 types indexed by universe levels equipped with a reflexive, symmetric and
 triangular
 [large rational neighborhood](metric-spaces.large-rational-neighborhoods.md).

From 88f3d70cba0d8668740799ec5c553d0f980c8d6b Mon Sep 17 00:00:00 2001
From: malarbol <malarbol+git@gmail.com>
Date: Fri, 9 May 2025 01:23:05 +0200
Subject: [PATCH 4/5] large metric spaces

---
 src/metric-spaces.lagda.md                    |   1 +
 .../large-metric-spaces.lagda.md              | 185 ++++++++++++++++++
 2 files changed, 186 insertions(+)
 create mode 100644 src/metric-spaces/large-metric-spaces.lagda.md

diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md
index a4ed46072a..fc2e8d5442 100644
--- a/src/metric-spaces.lagda.md
+++ b/src/metric-spaces.lagda.md
@@ -69,6 +69,7 @@ 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-premetric-spaces public
+open import metric-spaces.large-metric-spaces public
 open import metric-spaces.large-premetric-spaces public
 open import metric-spaces.large-rational-neighborhoods public
 open import metric-spaces.limits-of-cauchy-approximations-premetric-spaces public
diff --git a/src/metric-spaces/large-metric-spaces.lagda.md b/src/metric-spaces/large-metric-spaces.lagda.md
new file mode 100644
index 0000000000..1e8f30c04f
--- /dev/null
+++ b/src/metric-spaces/large-metric-spaces.lagda.md
@@ -0,0 +1,185 @@
+# Large metric spaces
+
+```agda
+module metric-spaces.large-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.identity-types
+open import foundation.large-binary-relations
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import metric-spaces.large-premetric-spaces
+open import metric-spaces.large-rational-neighborhoods
+open import metric-spaces.similarity-of-elements-large-premetric-spaces
+```
+
+</details>
+
+## Idea
+
+A {{#concept "large metric space" Agda=Large-Metric-Space}} is a
+[large premetric space](metric-spaces.large-premetric-spaces.md) where
+[similarity](metric-spaces.similarity-of-elements-large-premetric-spaces.md) has
+propositional fibers.
+
+## Definitions
+
+### Extensional large premetric spaces
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (M : Large-Premetric-Space α β)
+  where
+
+  is-extensional-Large-Premetric-Space : UUω
+  is-extensional-Large-Premetric-Space =
+    {l1 l2 : Level} → (x : type-Large-Premetric-Space M l1) →
+    is-prop
+      ( Σ
+        ( type-Large-Premetric-Space M l2)
+        ( sim-element-Large-Premetric-Space M x))
+```
+
+### The type of large metric spaces
+
+```agda
+record
+  Large-Metric-Space (α : Level → Level) (β : Level → Level → Level) : UUω
+  where
+  constructor
+    make-Large-Metric-Space
+  field
+    premetric-space-Large-Metric-Space :
+      Large-Premetric-Space α β
+    is-extensional-Large-Metric-Space :
+      is-extensional-Large-Premetric-Space (premetric-space-Large-Metric-Space)
+
+open Large-Metric-Space public
+
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (M : Large-Metric-Space α β)
+  where
+
+  type-Large-Metric-Space : (l : Level) → UU (α l)
+  type-Large-Metric-Space =
+    type-Large-Premetric-Space
+      ( premetric-space-Large-Metric-Space M)
+
+  neighborhood-Large-Metric-Space :
+    Large-Rational-Neighborhood β type-Large-Metric-Space
+  neighborhood-Large-Metric-Space =
+    neighborhood-Large-Premetric-Space
+      ( premetric-space-Large-Metric-Space M)
+
+  is-in-neighborhood-Large-Metric-Space :
+    (d : ℚ⁺) {l1 l2 : Level} →
+    type-Large-Metric-Space l1 →
+    type-Large-Metric-Space l2 →
+    UU (β l1 l2)
+  is-in-neighborhood-Large-Metric-Space =
+    is-in-neighborhood-Large-Premetric-Space
+      ( premetric-space-Large-Metric-Space M)
+
+  is-prop-is-in-neighborhood-Large-Metric-Space :
+    (d : ℚ⁺) {l1 l2 : Level}
+    (x : type-Large-Metric-Space l1)
+    (y : type-Large-Metric-Space l2) →
+    is-prop (is-in-neighborhood-Large-Metric-Space d x y)
+  is-prop-is-in-neighborhood-Large-Metric-Space =
+    is-prop-is-in-neighborhood-Large-Rational-Neighborhood
+      neighborhood-Large-Metric-Space
+
+  is-upper-bound-dist-prop-Large-Metric-Space :
+    {l1 l2 : Level}
+    (x : type-Large-Metric-Space l1)
+    (y : type-Large-Metric-Space l2) →
+    ℚ⁺ →
+    Prop (β l1 l2)
+  is-upper-bound-dist-prop-Large-Metric-Space x y d =
+    neighborhood-Large-Metric-Space d x y
+
+  is-upper-bound-dist-Large-Metric-Space :
+    {l1 l2 : Level}
+    (x : type-Large-Metric-Space l1)
+    (y : type-Large-Metric-Space l2) →
+    ℚ⁺ →
+    UU (β l1 l2)
+  is-upper-bound-dist-Large-Metric-Space x y d =
+    is-in-neighborhood-Large-Metric-Space d x y
+
+  is-prop-is-upper-bound-dist-Large-Metric-Space :
+    {l1 l2 : Level}
+    (x : type-Large-Metric-Space l1)
+    (y : type-Large-Metric-Space l2) →
+    (d : ℚ⁺) →
+    is-prop (is-upper-bound-dist-Large-Metric-Space x y d)
+  is-prop-is-upper-bound-dist-Large-Metric-Space x y d =
+    is-prop-is-in-neighborhood-Large-Metric-Space d x y
+
+  refl-neighborhood-Large-Metric-Space :
+    (d : ℚ⁺) {l : Level} (x : type-Large-Metric-Space l) →
+    is-in-neighborhood-Large-Metric-Space d x x
+  refl-neighborhood-Large-Metric-Space =
+    refl-neighborhood-Large-Premetric-Space
+      ( premetric-space-Large-Metric-Space M)
+
+  symmetric-neighborhood-Large-Metric-Space :
+    (d : ℚ⁺) {l1 l2 : Level}
+    (x : type-Large-Metric-Space l1)
+    (y : type-Large-Metric-Space l2) →
+    is-in-neighborhood-Large-Metric-Space d x y →
+    is-in-neighborhood-Large-Metric-Space d y x
+  symmetric-neighborhood-Large-Metric-Space =
+    symmetric-neighborhood-Large-Premetric-Space
+      ( premetric-space-Large-Metric-Space M)
+
+  inv-neighborhood-Large-Metric-Space :
+    (d : ℚ⁺) {l1 l2 : Level}
+    {x : type-Large-Metric-Space l1}
+    {y : type-Large-Metric-Space l2} →
+    is-in-neighborhood-Large-Metric-Space d x y →
+    is-in-neighborhood-Large-Metric-Space d y x
+  inv-neighborhood-Large-Metric-Space d {x = x} {y = y} =
+    symmetric-neighborhood-Large-Metric-Space d x y
+
+  triangular-neighborhood-Large-Metric-Space :
+    (ε δ : ℚ⁺) {l1 l2 l3 : Level}
+    (x : type-Large-Metric-Space l1)
+    (y : type-Large-Metric-Space l2)
+    (z : type-Large-Metric-Space l3) →
+    is-in-neighborhood-Large-Metric-Space δ y z →
+    is-in-neighborhood-Large-Metric-Space ε x y →
+    is-in-neighborhood-Large-Metric-Space (ε +ℚ⁺ δ) x z
+  triangular-neighborhood-Large-Metric-Space =
+    triangular-neighborhood-Large-Premetric-Space
+      ( premetric-space-Large-Metric-Space M)
+```
+
+## Properties
+
+### Equal elements of a large metric space are neighors
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (M : Large-Metric-Space α β)
+  where
+
+  neighborhood-eq-Large-Metric-Space :
+    {l : Level} (x y : type-Large-Metric-Space M l) →
+    (x ＝ y) →
+    (d : ℚ⁺) →
+    is-in-neighborhood-Large-Metric-Space M d x y
+  neighborhood-eq-Large-Metric-Space =
+    neighborhood-eq-Large-Premetric-Space
+      ( premetric-space-Large-Metric-Space M)
+```

From d6e583418bf522dae6a557c21abac63b21f597aa Mon Sep 17 00:00:00 2001
From: malarbol <malarbol+git@gmail.com>
Date: Fri, 9 May 2025 19:41:35 +0200
Subject: [PATCH 5/5] rename Large-Rational-Neighborhood-Relation

---
 .../large-metric-spaces.lagda.md              |  4 +-
 .../large-premetric-spaces.lagda.md           | 12 ++---
 .../large-rational-neighborhoods.lagda.md     | 50 +++++++++----------
 3 files changed, 33 insertions(+), 33 deletions(-)

diff --git a/src/metric-spaces/large-metric-spaces.lagda.md b/src/metric-spaces/large-metric-spaces.lagda.md
index 1e8f30c04f..81b9e43d4b 100644
--- a/src/metric-spaces/large-metric-spaces.lagda.md
+++ b/src/metric-spaces/large-metric-spaces.lagda.md
@@ -75,7 +75,7 @@ module _
       ( premetric-space-Large-Metric-Space M)
 
   neighborhood-Large-Metric-Space :
-    Large-Rational-Neighborhood β type-Large-Metric-Space
+    Large-Rational-Neighborhood-Relation β type-Large-Metric-Space
   neighborhood-Large-Metric-Space =
     neighborhood-Large-Premetric-Space
       ( premetric-space-Large-Metric-Space M)
@@ -95,7 +95,7 @@ module _
     (y : type-Large-Metric-Space l2) →
     is-prop (is-in-neighborhood-Large-Metric-Space d x y)
   is-prop-is-in-neighborhood-Large-Metric-Space =
-    is-prop-is-in-neighborhood-Large-Rational-Neighborhood
+    is-prop-is-in-neighborhood-Large-Rational-Neighborhood-Relation
       neighborhood-Large-Metric-Space
 
   is-upper-bound-dist-prop-Large-Metric-Space :
diff --git a/src/metric-spaces/large-premetric-spaces.lagda.md b/src/metric-spaces/large-premetric-spaces.lagda.md
index 19e2c2ccee..7f5f2f3966 100644
--- a/src/metric-spaces/large-premetric-spaces.lagda.md
+++ b/src/metric-spaces/large-premetric-spaces.lagda.md
@@ -37,15 +37,15 @@ record
   field
     type-Large-Premetric-Space : (l : Level) → UU (α l)
     neighborhood-Large-Premetric-Space :
-      Large-Rational-Neighborhood β type-Large-Premetric-Space
+      Large-Rational-Neighborhood-Relation β type-Large-Premetric-Space
     refl-neighborhood-Large-Premetric-Space :
-      is-reflexive-Large-Rational-Neighborhood
+      is-reflexive-Large-Rational-Neighborhood-Relation
         neighborhood-Large-Premetric-Space
     symmetric-neighborhood-Large-Premetric-Space :
-      is-symmetric-Large-Rational-Neighborhood
+      is-symmetric-Large-Rational-Neighborhood-Relation
         neighborhood-Large-Premetric-Space
     triangular-neighborhood-Large-Premetric-Space :
-      is-triangular-Large-Rational-Neighborhood
+      is-triangular-Large-Rational-Neighborhood-Relation
         neighborhood-Large-Premetric-Space
 
 open Large-Premetric-Space public
@@ -61,7 +61,7 @@ module _
     type-Large-Premetric-Space M l2 →
     UU (β l1 l2)
   is-in-neighborhood-Large-Premetric-Space =
-    is-in-neighborhood-Large-Rational-Neighborhood
+    is-in-neighborhood-Large-Rational-Neighborhood-Relation
       (neighborhood-Large-Premetric-Space M)
 
   is-prop-is-in-neighborhood-Large-Premetric-Space :
@@ -70,7 +70,7 @@ module _
     (y : type-Large-Premetric-Space M l2) →
     is-prop (is-in-neighborhood-Large-Premetric-Space d x y)
   is-prop-is-in-neighborhood-Large-Premetric-Space =
-    is-prop-is-in-neighborhood-Large-Rational-Neighborhood
+    is-prop-is-in-neighborhood-Large-Rational-Neighborhood-Relation
       (neighborhood-Large-Premetric-Space M)
 
   is-upper-bound-dist-prop-Large-Premetric-Space :
diff --git a/src/metric-spaces/large-rational-neighborhoods.lagda.md b/src/metric-spaces/large-rational-neighborhoods.lagda.md
index 80ede8f525..920f5c9592 100644
--- a/src/metric-spaces/large-rational-neighborhoods.lagda.md
+++ b/src/metric-spaces/large-rational-neighborhoods.lagda.md
@@ -31,28 +31,28 @@ module _
   (A : (l : Level) → UU (α l))
   where
 
-  Large-Rational-Neighborhood : UUω
-  Large-Rational-Neighborhood =
+  Large-Rational-Neighborhood-Relation : UUω
+  Large-Rational-Neighborhood-Relation =
     ℚ⁺ → Large-Relation-Prop β A
 
 module _
   {α : Level → Level} {β : Level → Level → Level}
   {A : (l : Level) → UU (α l)}
-  (N : Large-Rational-Neighborhood β A)
+  (N : Large-Rational-Neighborhood-Relation β A)
   (d : ℚ⁺) {l1 l2 : Level} (x : A l1) (y : A l2)
   where
 
-  neighborhood-Large-Rational-Neighborhood : Prop (β l1 l2)
-  neighborhood-Large-Rational-Neighborhood = N d x y
+  neighborhood-Large-Rational-Neighborhood-Relation : Prop (β l1 l2)
+  neighborhood-Large-Rational-Neighborhood-Relation = N d x y
 
-  is-in-neighborhood-Large-Rational-Neighborhood : UU (β l1 l2)
-  is-in-neighborhood-Large-Rational-Neighborhood =
-    type-Prop neighborhood-Large-Rational-Neighborhood
+  is-in-neighborhood-Large-Rational-Neighborhood-Relation : UU (β l1 l2)
+  is-in-neighborhood-Large-Rational-Neighborhood-Relation =
+    type-Prop neighborhood-Large-Rational-Neighborhood-Relation
 
-  is-prop-is-in-neighborhood-Large-Rational-Neighborhood :
-    is-prop is-in-neighborhood-Large-Rational-Neighborhood
-  is-prop-is-in-neighborhood-Large-Rational-Neighborhood =
-    is-prop-type-Prop neighborhood-Large-Rational-Neighborhood
+  is-prop-is-in-neighborhood-Large-Rational-Neighborhood-Relation :
+    is-prop is-in-neighborhood-Large-Rational-Neighborhood-Relation
+  is-prop-is-in-neighborhood-Large-Rational-Neighborhood-Relation =
+    is-prop-type-Prop neighborhood-Large-Rational-Neighborhood-Relation
 ```
 
 ## Properties
@@ -63,24 +63,24 @@ module _
 module _
   {α : Level → Level} {β : Level → Level → Level}
   {A : (l : Level) → UU (α l)}
-  (N : Large-Rational-Neighborhood β A)
+  (N : Large-Rational-Neighborhood-Relation β A)
   where
 
-  is-reflexive-Large-Rational-Neighborhood : UUω
-  is-reflexive-Large-Rational-Neighborhood =
+  is-reflexive-Large-Rational-Neighborhood-Relation : UUω
+  is-reflexive-Large-Rational-Neighborhood-Relation =
     (d : ℚ⁺) {l : Level} (x : A l) →
-    is-in-neighborhood-Large-Rational-Neighborhood N d x x
+    is-in-neighborhood-Large-Rational-Neighborhood-Relation N d x x
 
-  is-symmetric-Large-Rational-Neighborhood : UUω
-  is-symmetric-Large-Rational-Neighborhood =
+  is-symmetric-Large-Rational-Neighborhood-Relation : UUω
+  is-symmetric-Large-Rational-Neighborhood-Relation =
     (d : ℚ⁺) {l1 l2 : Level} (x : A l1) (y : A l2) →
-    is-in-neighborhood-Large-Rational-Neighborhood N d x y →
-    is-in-neighborhood-Large-Rational-Neighborhood N d y x
+    is-in-neighborhood-Large-Rational-Neighborhood-Relation N d x y →
+    is-in-neighborhood-Large-Rational-Neighborhood-Relation N d y x
 
-  is-triangular-Large-Rational-Neighborhood : UUω
-  is-triangular-Large-Rational-Neighborhood =
+  is-triangular-Large-Rational-Neighborhood-Relation : UUω
+  is-triangular-Large-Rational-Neighborhood-Relation =
     (ε δ : ℚ⁺) {l1 l2 l3 : Level} (x : A l1) (y : A l2) (z : A l3) →
-    is-in-neighborhood-Large-Rational-Neighborhood N δ y z →
-    is-in-neighborhood-Large-Rational-Neighborhood N ε x y →
-    is-in-neighborhood-Large-Rational-Neighborhood N (ε +ℚ⁺ δ) x z
+    is-in-neighborhood-Large-Rational-Neighborhood-Relation N δ y z →
+    is-in-neighborhood-Large-Rational-Neighborhood-Relation N ε x y →
+    is-in-neighborhood-Large-Rational-Neighborhood-Relation N (ε +ℚ⁺ δ) x z
 ```