diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md
index 0bf9402bb1..fc2e8d5442 100644
--- a/src/metric-spaces.lagda.md
+++ b/src/metric-spaces.lagda.md
@@ -69,6 +69,9 @@ 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
 open import metric-spaces.limits-of-sequences-metric-spaces public
 open import metric-spaces.limits-of-sequences-premetric-spaces public
@@ -102,6 +105,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/large-metric-spaces.lagda.md b/src/metric-spaces/large-metric-spaces.lagda.md
new file mode 100644
index 0000000000..81b9e43d4b
--- /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-Relation β 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-Relation
+      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)
+```
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..7f5f2f3966
--- /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-Relation β type-Large-Premetric-Space
+    refl-neighborhood-Large-Premetric-Space :
+      is-reflexive-Large-Rational-Neighborhood-Relation
+        neighborhood-Large-Premetric-Space
+    symmetric-neighborhood-Large-Premetric-Space :
+      is-symmetric-Large-Rational-Neighborhood-Relation
+        neighborhood-Large-Premetric-Space
+    triangular-neighborhood-Large-Premetric-Space :
+      is-triangular-Large-Rational-Neighborhood-Relation
+        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-Relation
+      (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-Relation
+      (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..920f5c9592
--- /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-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-Relation β A)
+  (d : ℚ⁺) {l1 l2 : Level} (x : A l1) (y : A l2)
+  where
+
+  neighborhood-Large-Rational-Neighborhood-Relation : Prop (β l1 l2)
+  neighborhood-Large-Rational-Neighborhood-Relation = N d x y
+
+  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-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
+
+### Specification of properties of rational neighborhoods
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  {A : (l : Level) → UU (α l)}
+  (N : Large-Rational-Neighborhood-Relation β A)
+  where
+
+  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-Relation N d x x
+
+  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-Relation N d x y →
+    is-in-neighborhood-Large-Rational-Neighborhood-Relation N d y x
+
+  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-Relation N δ y z →
+    is-in-neighborhood-Large-Rational-Neighborhood-Relation N ε x y →
+    is-in-neighborhood-Large-Rational-Neighborhood-Relation N (ε +ℚ⁺ δ) x z
+```
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)))
+```