diff --git a/config/codespell-dictionary.txt b/config/codespell-dictionary.txt
index 42eb42d013..67d1419ed8 100644
--- a/config/codespell-dictionary.txt
+++ b/config/codespell-dictionary.txt
@@ -79,3 +79,4 @@ morphsims->morphisms
 outout->output
 ringr->ring
 ringrs->rings
+semiorm->seminorm
diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md
index 240d62913f..59e8798cf4 100644
--- a/src/linear-algebra.lagda.md
+++ b/src/linear-algebra.lagda.md
@@ -34,16 +34,19 @@ open import linear-algebra.linear-spans-left-modules-rings public
 open import linear-algebra.matrices public
 open import linear-algebra.matrices-on-rings public
 open import linear-algebra.multiplication-matrices public
+open import linear-algebra.normed-real-vector-spaces public
 open import linear-algebra.orthogonality-bilinear-forms-real-vector-spaces public
 open import linear-algebra.orthogonality-real-inner-product-spaces public
 open import linear-algebra.preimages-of-left-module-structures-along-homomorphisms-of-rings public
 open import linear-algebra.rational-modules public
+open import linear-algebra.real-banach-spaces public
 open import linear-algebra.real-inner-product-spaces public
 open import linear-algebra.real-vector-spaces public
 open import linear-algebra.right-modules-rings public
 open import linear-algebra.scalar-multiplication-matrices public
 open import linear-algebra.scalar-multiplication-tuples public
 open import linear-algebra.scalar-multiplication-tuples-on-rings public
+open import linear-algebra.seminormed-real-vector-spaces public
 open import linear-algebra.subsets-left-modules-rings public
 open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces public
 open import linear-algebra.transposition-matrices public
diff --git a/src/linear-algebra/normed-real-vector-spaces.lagda.md b/src/linear-algebra/normed-real-vector-spaces.lagda.md
new file mode 100644
index 0000000000..de825ec122
--- /dev/null
+++ b/src/linear-algebra/normed-real-vector-spaces.lagda.md
@@ -0,0 +1,253 @@
+# Normed real vector spaces
+
+```agda
+module linear-algebra.normed-real-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+
+open import linear-algebra.real-vector-spaces
+open import linear-algebra.seminormed-real-vector-spaces
+
+open import metric-spaces.equality-of-metric-spaces
+open import metric-spaces.located-metric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.metrics
+
+open import real-numbers.absolute-value-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.distance-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+open import real-numbers.nonnegative-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.saturation-inequality-nonnegative-real-numbers
+open import real-numbers.similarity-real-numbers
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "norm" WDID=Q956437 WD="norm" Disambiguation="on a real vector space" Agda=norm-ℝ-Vector-Space}}
+on a [real vector space](linear-algebra.real-vector-spaces.md) `V` is a
+[seminorm](linear-algebra.seminormed-real-vector-spaces.md) `p` on `V` that is
+**extensional**: if `p(v) = 0`, then `v` is the zero vector.
+
+A real vector space equipped with such a norm is called a
+{{#concept "normed vector space" Disambiguation="normed real vector space" WDID=Q726210 WD="normed vector space" Agda=Normed-ℝ-Vector-Space}}.
+
+A norm on a real vector space induces a
+[located](metric-spaces.located-metric-spaces.md)
+[metric space](metric-spaces.metric-spaces.md) on the vector space, defined by
+the neighborhood relation that `v` and `w` are in an `ε`-neighborhood of each
+other if `p(v - w) ≤ ε`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} (V : ℝ-Vector-Space l1 l2) (p : seminorm-ℝ-Vector-Space V)
+  where
+
+  is-norm-prop-seminorm-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
+  is-norm-prop-seminorm-ℝ-Vector-Space =
+    Π-Prop
+      ( type-ℝ-Vector-Space V)
+      ( λ v →
+        hom-Prop
+          ( Id-Prop (ℝ-Set l1) (pr1 p v) (raise-ℝ l1 zero-ℝ))
+          ( is-zero-prop-ℝ-Vector-Space V v))
+
+  is-norm-seminorm-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
+  is-norm-seminorm-ℝ-Vector-Space =
+    type-Prop is-norm-prop-seminorm-ℝ-Vector-Space
+
+norm-ℝ-Vector-Space : {l1 l2 : Level} → ℝ-Vector-Space l1 l2 → UU (lsuc l1 ⊔ l2)
+norm-ℝ-Vector-Space V = type-subtype (is-norm-prop-seminorm-ℝ-Vector-Space V)
+
+Normed-ℝ-Vector-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Normed-ℝ-Vector-Space l1 l2 = Σ (ℝ-Vector-Space l1 l2) norm-ℝ-Vector-Space
+```
+
+## Properties
+
+```agda
+module _
+  {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2)
+  where
+
+  vector-space-Normed-ℝ-Vector-Space : ℝ-Vector-Space l1 l2
+  vector-space-Normed-ℝ-Vector-Space = pr1 V
+
+  norm-Normed-ℝ-Vector-Space :
+    norm-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
+  norm-Normed-ℝ-Vector-Space = pr2 V
+
+  seminorm-Normed-ℝ-Vector-Space :
+    seminorm-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
+  seminorm-Normed-ℝ-Vector-Space = pr1 norm-Normed-ℝ-Vector-Space
+
+  seminormed-vector-space-Normed-ℝ-Vector-Space :
+    Seminormed-ℝ-Vector-Space l1 l2
+  seminormed-vector-space-Normed-ℝ-Vector-Space =
+    ( vector-space-Normed-ℝ-Vector-Space , seminorm-Normed-ℝ-Vector-Space)
+
+  set-Normed-ℝ-Vector-Space : Set l2
+  set-Normed-ℝ-Vector-Space =
+    set-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
+
+  type-Normed-ℝ-Vector-Space : UU l2
+  type-Normed-ℝ-Vector-Space =
+    type-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
+
+  add-Normed-ℝ-Vector-Space :
+    type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space →
+    type-Normed-ℝ-Vector-Space
+  add-Normed-ℝ-Vector-Space =
+    add-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
+
+  diff-Normed-ℝ-Vector-Space :
+    type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space →
+    type-Normed-ℝ-Vector-Space
+  diff-Normed-ℝ-Vector-Space =
+    diff-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
+
+  zero-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space
+  zero-Normed-ℝ-Vector-Space =
+    zero-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
+
+  map-norm-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space → ℝ l1
+  map-norm-Normed-ℝ-Vector-Space = pr1 (pr1 norm-Normed-ℝ-Vector-Space)
+
+  nonnegative-norm-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space → ℝ⁰⁺ l1
+  nonnegative-norm-Normed-ℝ-Vector-Space =
+    nonnegative-seminorm-Seminormed-ℝ-Vector-Space
+      ( seminormed-vector-space-Normed-ℝ-Vector-Space)
+
+  dist-Normed-ℝ-Vector-Space :
+    type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space → ℝ l1
+  dist-Normed-ℝ-Vector-Space =
+    dist-Seminormed-ℝ-Vector-Space seminormed-vector-space-Normed-ℝ-Vector-Space
+
+  nonnegative-dist-Normed-ℝ-Vector-Space :
+    type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space → ℝ⁰⁺ l1
+  nonnegative-dist-Normed-ℝ-Vector-Space =
+    nonnegative-dist-Seminormed-ℝ-Vector-Space
+      ( seminormed-vector-space-Normed-ℝ-Vector-Space)
+
+  is-extensional-norm-Normed-ℝ-Metric-Space :
+    (v : type-Normed-ℝ-Vector-Space) →
+    map-norm-Normed-ℝ-Vector-Space v ＝ raise-ℝ l1 zero-ℝ →
+    v ＝ zero-Normed-ℝ-Vector-Space
+  is-extensional-norm-Normed-ℝ-Metric-Space = pr2 norm-Normed-ℝ-Vector-Space
+
+  is-extensional-dist-Normed-ℝ-Metric-Space :
+    (v w : type-Normed-ℝ-Vector-Space) →
+    dist-Normed-ℝ-Vector-Space v w ＝ raise-ℝ l1 zero-ℝ →
+    v ＝ w
+  is-extensional-dist-Normed-ℝ-Metric-Space v w |v-w|=0 =
+    eq-is-zero-right-subtraction-Ab
+      ( ab-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space)
+      ( is-extensional-norm-Normed-ℝ-Metric-Space
+        ( diff-Normed-ℝ-Vector-Space v w)
+        ( |v-w|=0))
+
+  commutative-dist-Normed-ℝ-Vector-Space :
+    (v w : type-Normed-ℝ-Vector-Space) →
+    dist-Normed-ℝ-Vector-Space v w ＝ dist-Normed-ℝ-Vector-Space w v
+  commutative-dist-Normed-ℝ-Vector-Space =
+    commutative-dist-Seminormed-ℝ-Vector-Space
+      ( seminormed-vector-space-Normed-ℝ-Vector-Space)
+```
+
+### The metric space of a normed vector space
+
+```agda
+module _
+  {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2)
+  where
+
+  refl-norm-Normed-ℝ-Vector-Space :
+    (v : type-Normed-ℝ-Vector-Space V) →
+    sim-ℝ zero-ℝ (dist-Normed-ℝ-Vector-Space V v v)
+  refl-norm-Normed-ℝ-Vector-Space v =
+    inv-tr
+      ( sim-ℝ zero-ℝ)
+      ( is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space
+        ( seminormed-vector-space-Normed-ℝ-Vector-Space V)
+        ( v))
+      ( sim-raise-ℝ l1 zero-ℝ)
+
+  metric-Normed-ℝ-Vector-Space : Metric l1 (set-Normed-ℝ-Vector-Space V)
+  metric-Normed-ℝ-Vector-Space =
+    ( nonnegative-dist-Normed-ℝ-Vector-Space V ,
+      refl-norm-Normed-ℝ-Vector-Space ,
+      ( λ v w → eq-ℝ⁰⁺ _ _ (commutative-dist-Normed-ℝ-Vector-Space V v w)) ,
+      triangular-dist-Seminormed-ℝ-Vector-Space
+        ( seminormed-vector-space-Normed-ℝ-Vector-Space V) ,
+      ( λ v w 0~dvw →
+        is-extensional-dist-Normed-ℝ-Metric-Space V v w
+          ( eq-sim-ℝ
+            ( transitive-sim-ℝ _ _ _
+              ( sim-raise-ℝ l1 zero-ℝ)
+              ( symmetric-sim-ℝ 0~dvw)))))
+
+  metric-space-Normed-ℝ-Vector-Space : Metric-Space l2 l1
+  metric-space-Normed-ℝ-Vector-Space =
+    metric-space-Metric
+      ( set-Normed-ℝ-Vector-Space V)
+      ( metric-Normed-ℝ-Vector-Space)
+
+  located-metric-space-Normed-ℝ-Vector-Space : Located-Metric-Space l2 l1
+  located-metric-space-Normed-ℝ-Vector-Space =
+    located-metric-space-Metric
+      ( set-Normed-ℝ-Vector-Space V)
+      ( metric-Normed-ℝ-Vector-Space)
+```
+
+## Properties
+
+### The real numbers are a normed vector space over themselves with norm `x ↦ |x|`
+
+```agda
+normed-real-vector-space-ℝ :
+  (l : Level) → Normed-ℝ-Vector-Space l (lsuc l)
+normed-real-vector-space-ℝ l =
+  ( real-vector-space-ℝ l ,
+    ( abs-ℝ , triangle-inequality-abs-ℝ , abs-mul-ℝ) ,
+    eq-raise-zero-eq-raise-zero-abs-ℝ)
+
+abstract
+  eq-metric-space-normed-real-vector-space-metric-space-ℝ :
+    (l : Level) →
+    metric-space-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l) ＝
+    metric-space-ℝ l
+  eq-metric-space-normed-real-vector-space-metric-space-ℝ l =
+    eq-isometric-eq-Metric-Space _ _
+      ( refl , λ d x y → inv-iff (neighborhood-iff-leq-dist-ℝ d x y))
+```
+
+## See also
+
+- [Real Banach spaces](linear-algebra.real-banach-spaces.md), normed real vector
+  spaces for which the induced metric space is
+  [complete](metric-spaces.complete-metric-spaces.md)
+
+## External links
+
+- [Normed vector space](https://en.wikipedia.org/wiki/Normed_vector_space) on
+  Wikipedia
diff --git a/src/linear-algebra/real-banach-spaces.lagda.md b/src/linear-algebra/real-banach-spaces.lagda.md
new file mode 100644
index 0000000000..1ed7c36a32
--- /dev/null
+++ b/src/linear-algebra/real-banach-spaces.lagda.md
@@ -0,0 +1,77 @@
+# Real Banach spaces
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module linear-algebra.real-banach-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import linear-algebra.normed-real-vector-spaces
+
+open import metric-spaces.complete-metric-spaces
+
+open import real-numbers.cauchy-completeness-dedekind-real-numbers
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "real Banach space" WDID=Q194397 WD="Banach space" Agda=ℝ-Banach-Space}}
+is a [normed](linear-algebra.normed-real-vector-spaces.md)
+[real vector space](linear-algebra.real-vector-spaces.md) such that the
+[metric space](metric-spaces.metric-spaces.md) induced by the norm is
+[complete](metric-spaces.complete-metric-spaces.md).
+
+## Definition
+
+```agda
+is-banach-prop-Normed-ℝ-Vector-Space :
+  {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) → Prop (l1 ⊔ l2)
+is-banach-prop-Normed-ℝ-Vector-Space V =
+  is-complete-prop-Metric-Space (metric-space-Normed-ℝ-Vector-Space V)
+
+is-banach-Normed-ℝ-Vector-Space :
+  {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) → UU (l1 ⊔ l2)
+is-banach-Normed-ℝ-Vector-Space V =
+  type-Prop (is-banach-prop-Normed-ℝ-Vector-Space V)
+
+ℝ-Banach-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+ℝ-Banach-Space l1 l2 =
+  type-subtype (is-banach-prop-Normed-ℝ-Vector-Space {l1} {l2})
+```
+
+## Properties
+
+### The real numbers are a real Banach space with norm `x ↦ |x|`
+
+```agda
+abstract
+  is-banach-normed-real-vector-space-ℝ :
+    (l : Level) →
+    is-banach-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l)
+  is-banach-normed-real-vector-space-ℝ l =
+    inv-tr
+      ( is-complete-Metric-Space)
+      ( eq-metric-space-normed-real-vector-space-metric-space-ℝ l)
+      ( is-complete-metric-space-ℝ l)
+
+real-banach-space-ℝ : (l : Level) → ℝ-Banach-Space l (lsuc l)
+real-banach-space-ℝ l =
+  ( normed-real-vector-space-ℝ l ,
+    is-banach-normed-real-vector-space-ℝ l)
+```
+
+## External links
+
+- [Banach space](https://en.wikipedia.org/wiki/Banach_space) on Wikipedia
diff --git a/src/linear-algebra/real-vector-spaces.lagda.md b/src/linear-algebra/real-vector-spaces.lagda.md
index 62eeac6439..526b466b41 100644
--- a/src/linear-algebra/real-vector-spaces.lagda.md
+++ b/src/linear-algebra/real-vector-spaces.lagda.md
@@ -250,3 +250,4 @@ real-vector-space-ℝ l =
 ## See also
 
 - [Vector spaces](linear-algebra.vector-spaces.md)
+- [Normed real vector spaces](linear-algebra.normed-real-vector-spaces.md)
diff --git a/src/linear-algebra/seminormed-real-vector-spaces.lagda.md b/src/linear-algebra/seminormed-real-vector-spaces.lagda.md
new file mode 100644
index 0000000000..487eebac05
--- /dev/null
+++ b/src/linear-algebra/seminormed-real-vector-spaces.lagda.md
@@ -0,0 +1,596 @@
+# Seminormed real vector spaces
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module linear-algebra.seminormed-real-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-relations
+open import foundation.conjunction
+open import foundation.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.universe-levels
+
+open import group-theory.abelian-groups
+
+open import linear-algebra.real-vector-spaces
+
+open import metric-spaces.pseudometric-spaces
+
+open import order-theory.large-posets
+
+open import real-numbers.absolute-value-real-numbers
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.inequalities-addition-and-subtraction-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.multiplication-positive-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.negation-real-numbers
+open import real-numbers.nonnegative-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.saturation-inequality-nonnegative-real-numbers
+open import real-numbers.similarity-real-numbers
+open import real-numbers.strict-inequality-real-numbers
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "seminorm" WDID=Q1416088 WD="seminorm" Disambiguation="on a real vector space" Agda=seminorm-ℝ-Vector-Space}}
+on a [real vector space](linear-algebra.real-vector-spaces.md) `V` is a
+[real](real-numbers.dedekind-real-numbers.md)-valued function `p` on the vector
+space which is
+
+- **Triangular.** `p(x + y) ≤ p(x) + p(y)` for all `x` and `y` in `V`, and
+- **Absolutely homogeneous.** `p(c * x) = |c| * p(x)` for all real numbers `c`
+  and `x` in `V`.
+
+These conditions together imply that `p(x) ≥ 0` for any `x`, and `p(0) = 0`.
+
+A real vector space equipped with such a seminorm is called a
+{{#concept "seminormed space" WD="seminormed space" WDID=Q63793693 Agda=Seminormed-ℝ-Vector-Space}}.
+A seminormed space has an induced
+[pseudometric structure](metric-spaces.pseudometric-spaces.md) defined by the
+neighborhood relation that `v` and `w` are in an `ε`-neighborhood of each other
+if `p(v - w) ≤ ε`.
+
+**Terminology.** The term _absolute homogeneity_ comes from the more general
+concept of
+[homogeneous functions](https://en.wikipedia.org/wiki/Homogeneous_function). A
+multivariable function `f` on real vector spaces is said to be _homogeneous of
+degree `k`_ if for every scalar `s` we have that
+`f(sx₀,sx₁,…,sxₙ) = sᵏf(x₀,x₁,…,xₙ)`. In particular, you may note that any
+homogeneous bilinear form must be homogeneous of degree one.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Vector-Space l1 l2)
+  (p : type-ℝ-Vector-Space V → ℝ l1)
+  where
+
+  is-triangular-prop-seminorm-ℝ-Vector-Space : Prop (l1 ⊔ l2)
+  is-triangular-prop-seminorm-ℝ-Vector-Space =
+    Π-Prop
+      ( type-ℝ-Vector-Space V)
+      ( λ x →
+        Π-Prop
+          ( type-ℝ-Vector-Space V)
+          ( λ y → leq-prop-ℝ (p (add-ℝ-Vector-Space V x y)) (p x +ℝ p y)))
+
+  is-triangular-seminorm-ℝ-Vector-Space : UU (l1 ⊔ l2)
+  is-triangular-seminorm-ℝ-Vector-Space =
+    type-Prop is-triangular-prop-seminorm-ℝ-Vector-Space
+
+  is-absolutely-homogeneous-prop-seminorm-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
+  is-absolutely-homogeneous-prop-seminorm-ℝ-Vector-Space =
+    Π-Prop
+      ( ℝ l1)
+      ( λ c →
+        Π-Prop
+          ( type-ℝ-Vector-Space V)
+          ( λ x →
+            Id-Prop
+              ( ℝ-Set l1)
+              ( p (mul-ℝ-Vector-Space V c x))
+              ( abs-ℝ c *ℝ p x)))
+
+  is-absolutely-homogeneous-seminorm-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
+  is-absolutely-homogeneous-seminorm-ℝ-Vector-Space =
+    type-Prop is-absolutely-homogeneous-prop-seminorm-ℝ-Vector-Space
+
+  is-seminorm-prop-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
+  is-seminorm-prop-ℝ-Vector-Space =
+    is-triangular-prop-seminorm-ℝ-Vector-Space ∧
+    is-absolutely-homogeneous-prop-seminorm-ℝ-Vector-Space
+
+  is-seminorm-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
+  is-seminorm-ℝ-Vector-Space = type-Prop is-seminorm-prop-ℝ-Vector-Space
+
+seminorm-ℝ-Vector-Space :
+  {l1 l2 : Level} → ℝ-Vector-Space l1 l2 → UU (lsuc l1 ⊔ l2)
+seminorm-ℝ-Vector-Space V =
+  type-subtype (is-seminorm-prop-ℝ-Vector-Space V)
+
+Seminormed-ℝ-Vector-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Seminormed-ℝ-Vector-Space l1 l2 =
+  Σ (ℝ-Vector-Space l1 l2) seminorm-ℝ-Vector-Space
+```
+
+## Properties
+
+### Vector space properties
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : Seminormed-ℝ-Vector-Space l1 l2)
+  where
+
+  vector-space-Seminormed-ℝ-Vector-Space : ℝ-Vector-Space l1 l2
+  vector-space-Seminormed-ℝ-Vector-Space = pr1 V
+
+  set-Seminormed-ℝ-Vector-Space : Set l2
+  set-Seminormed-ℝ-Vector-Space =
+    set-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+
+  type-Seminormed-ℝ-Vector-Space : UU l2
+  type-Seminormed-ℝ-Vector-Space =
+    type-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+
+  seminorm-Seminormed-ℝ-Vector-Space :
+    seminorm-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+  seminorm-Seminormed-ℝ-Vector-Space = pr2 V
+
+  map-seminorm-Seminormed-ℝ-Vector-Space :
+    type-Seminormed-ℝ-Vector-Space → ℝ l1
+  map-seminorm-Seminormed-ℝ-Vector-Space =
+    pr1 seminorm-Seminormed-ℝ-Vector-Space
+
+  zero-Seminormed-ℝ-Vector-Space : type-Seminormed-ℝ-Vector-Space
+  zero-Seminormed-ℝ-Vector-Space =
+    zero-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+
+  is-zero-prop-Seminormed-ℝ-Vector-Space :
+    subtype l2 type-Seminormed-ℝ-Vector-Space
+  is-zero-prop-Seminormed-ℝ-Vector-Space =
+    is-zero-prop-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+
+  is-zero-Seminormed-ℝ-Vector-Space : type-Seminormed-ℝ-Vector-Space → UU l2
+  is-zero-Seminormed-ℝ-Vector-Space =
+    is-zero-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+
+  add-Seminormed-ℝ-Vector-Space :
+    type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space →
+    type-Seminormed-ℝ-Vector-Space
+  add-Seminormed-ℝ-Vector-Space =
+    add-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+
+  mul-Seminormed-ℝ-Vector-Space :
+    ℝ l1 → type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space
+  mul-Seminormed-ℝ-Vector-Space =
+    mul-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+
+  neg-Seminormed-ℝ-Vector-Space :
+    type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space
+  neg-Seminormed-ℝ-Vector-Space =
+    neg-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+
+  diff-Seminormed-ℝ-Vector-Space :
+    type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space →
+    type-Seminormed-ℝ-Vector-Space
+  diff-Seminormed-ℝ-Vector-Space v w =
+    add-Seminormed-ℝ-Vector-Space v (neg-Seminormed-ℝ-Vector-Space w)
+
+  right-inverse-law-add-Seminormed-ℝ-Vector-Space :
+    (v : type-Seminormed-ℝ-Vector-Space) →
+    add-Seminormed-ℝ-Vector-Space v (neg-Seminormed-ℝ-Vector-Space v) ＝
+    zero-Seminormed-ℝ-Vector-Space
+  right-inverse-law-add-Seminormed-ℝ-Vector-Space =
+    right-inverse-law-add-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+
+  add-diff-Seminormed-ℝ-Vector-Space :
+    (v w x : type-Seminormed-ℝ-Vector-Space) →
+    add-Seminormed-ℝ-Vector-Space
+      ( diff-Seminormed-ℝ-Vector-Space v w)
+      ( diff-Seminormed-ℝ-Vector-Space w x) ＝
+    diff-Seminormed-ℝ-Vector-Space v x
+  add-diff-Seminormed-ℝ-Vector-Space =
+    add-diff-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+
+  neg-neg-Seminormed-ℝ-Vector-Space :
+    (v : type-Seminormed-ℝ-Vector-Space) →
+    neg-Seminormed-ℝ-Vector-Space (neg-Seminormed-ℝ-Vector-Space v) ＝ v
+  neg-neg-Seminormed-ℝ-Vector-Space =
+    neg-neg-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+
+  left-zero-law-mul-Seminormed-ℝ-Vector-Space :
+    (v : type-Seminormed-ℝ-Vector-Space) →
+    mul-Seminormed-ℝ-Vector-Space (raise-ℝ l1 zero-ℝ) v ＝
+    zero-Seminormed-ℝ-Vector-Space
+  left-zero-law-mul-Seminormed-ℝ-Vector-Space =
+    left-zero-law-mul-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+
+  mul-neg-one-Seminormed-ℝ-Vector-Space :
+    (v : type-Seminormed-ℝ-Vector-Space) →
+    mul-Seminormed-ℝ-Vector-Space (neg-ℝ (raise-ℝ l1 one-ℝ)) v ＝
+    neg-Seminormed-ℝ-Vector-Space v
+  mul-neg-one-Seminormed-ℝ-Vector-Space =
+    mul-neg-one-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space
+
+  distributive-neg-diff-Seminormed-ℝ-Vector-Space :
+    (v w : type-Seminormed-ℝ-Vector-Space) →
+    neg-Seminormed-ℝ-Vector-Space (diff-Seminormed-ℝ-Vector-Space v w) ＝
+    diff-Seminormed-ℝ-Vector-Space w v
+  distributive-neg-diff-Seminormed-ℝ-Vector-Space =
+    neg-right-subtraction-Ab
+      ( ab-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space)
+
+  triangular-seminorm-Seminormed-ℝ-Vector-Space :
+    (v w : type-Seminormed-ℝ-Vector-Space) →
+    leq-ℝ
+      ( map-seminorm-Seminormed-ℝ-Vector-Space
+        ( add-Seminormed-ℝ-Vector-Space v w))
+      ( map-seminorm-Seminormed-ℝ-Vector-Space v +ℝ
+        map-seminorm-Seminormed-ℝ-Vector-Space w)
+  triangular-seminorm-Seminormed-ℝ-Vector-Space =
+    pr1 (pr2 seminorm-Seminormed-ℝ-Vector-Space)
+
+  is-absolutely-homogeneous-seminorm-Seminormed-ℝ-Vector-Space :
+    (c : ℝ l1) (v : type-Seminormed-ℝ-Vector-Space) →
+    map-seminorm-Seminormed-ℝ-Vector-Space
+      ( mul-Seminormed-ℝ-Vector-Space c v) ＝
+    abs-ℝ c *ℝ map-seminorm-Seminormed-ℝ-Vector-Space v
+  is-absolutely-homogeneous-seminorm-Seminormed-ℝ-Vector-Space =
+    pr2 (pr2 seminorm-Seminormed-ℝ-Vector-Space)
+
+  dist-Seminormed-ℝ-Vector-Space :
+    type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space → ℝ l1
+  dist-Seminormed-ℝ-Vector-Space v w =
+    map-seminorm-Seminormed-ℝ-Vector-Space
+      ( diff-Seminormed-ℝ-Vector-Space v w)
+```
+
+### The seminorm of the zero vector is zero
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : Seminormed-ℝ-Vector-Space l1 l2)
+  where
+
+  abstract
+    is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space :
+      map-seminorm-Seminormed-ℝ-Vector-Space
+        ( V)
+        ( zero-Seminormed-ℝ-Vector-Space V) ＝
+      raise-ℝ l1 zero-ℝ
+    is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space =
+      equational-reasoning
+        map-seminorm-Seminormed-ℝ-Vector-Space
+          ( V)
+          ( zero-Seminormed-ℝ-Vector-Space V)
+        ＝
+          map-seminorm-Seminormed-ℝ-Vector-Space
+              ( V)
+              ( mul-Seminormed-ℝ-Vector-Space
+                ( V)
+                ( raise-ℝ l1 zero-ℝ)
+                ( zero-Seminormed-ℝ-Vector-Space V))
+          by
+            ap
+              ( map-seminorm-Seminormed-ℝ-Vector-Space V)
+              ( inv (left-zero-law-mul-Seminormed-ℝ-Vector-Space V _))
+        ＝
+          ( abs-ℝ (raise-ℝ l1 zero-ℝ)) *ℝ
+          ( map-seminorm-Seminormed-ℝ-Vector-Space
+            ( V)
+            ( zero-Seminormed-ℝ-Vector-Space V))
+          by is-absolutely-homogeneous-seminorm-Seminormed-ℝ-Vector-Space V _ _
+        ＝
+          ( raise-ℝ l1 (abs-ℝ zero-ℝ)) *ℝ
+          ( map-seminorm-Seminormed-ℝ-Vector-Space
+            ( V)
+            ( zero-Seminormed-ℝ-Vector-Space V))
+          by ap-mul-ℝ (abs-raise-ℝ l1 _) refl
+        ＝
+          ( raise-zero-ℝ l1) *ℝ
+          ( map-seminorm-Seminormed-ℝ-Vector-Space
+            ( V)
+            ( zero-Seminormed-ℝ-Vector-Space V))
+          by ap-mul-ℝ (ap (raise-ℝ l1) abs-zero-ℝ) refl
+        ＝ raise-zero-ℝ l1
+          by left-raise-zero-law-mul-ℝ _
+
+    is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space :
+      (v : type-Seminormed-ℝ-Vector-Space V) →
+      dist-Seminormed-ℝ-Vector-Space V v v ＝ raise-ℝ l1 zero-ℝ
+    is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space v =
+      ( ap
+        ( map-seminorm-Seminormed-ℝ-Vector-Space V)
+        ( right-inverse-law-add-Seminormed-ℝ-Vector-Space V v)) ∙
+      ( is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space)
+
+    sim-zero-diagonal-dist-Seminormed-ℝ-Vector-Space :
+      (v : type-Seminormed-ℝ-Vector-Space V) →
+      sim-ℝ (dist-Seminormed-ℝ-Vector-Space V v v) zero-ℝ
+    sim-zero-diagonal-dist-Seminormed-ℝ-Vector-Space v =
+      inv-tr
+        ( λ x → sim-ℝ x zero-ℝ)
+        ( is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space v)
+        ( sim-raise-ℝ' l1 zero-ℝ)
+```
+
+### The seminorm of the negation of a vector is equal to the seminorm of the vector
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : Seminormed-ℝ-Vector-Space l1 l2)
+  where
+
+  abstract
+    seminorm-neg-Seminormed-ℝ-Vector-Space :
+      (v : type-Seminormed-ℝ-Vector-Space V) →
+      map-seminorm-Seminormed-ℝ-Vector-Space
+        ( V)
+        ( neg-Seminormed-ℝ-Vector-Space V v) ＝
+      map-seminorm-Seminormed-ℝ-Vector-Space V v
+    seminorm-neg-Seminormed-ℝ-Vector-Space v =
+      equational-reasoning
+        map-seminorm-Seminormed-ℝ-Vector-Space
+          ( V)
+          ( neg-Seminormed-ℝ-Vector-Space V v)
+        ＝
+          map-seminorm-Seminormed-ℝ-Vector-Space
+            ( V)
+            ( mul-Seminormed-ℝ-Vector-Space
+              ( V)
+              ( neg-ℝ (raise-ℝ l1 one-ℝ))
+              ( v))
+          by
+            ap
+              ( map-seminorm-Seminormed-ℝ-Vector-Space V)
+              ( inv (mul-neg-one-Seminormed-ℝ-Vector-Space V v))
+        ＝
+          ( abs-ℝ (neg-ℝ (raise-ℝ l1 one-ℝ))) *ℝ
+          ( map-seminorm-Seminormed-ℝ-Vector-Space V v)
+          by is-absolutely-homogeneous-seminorm-Seminormed-ℝ-Vector-Space V _ _
+        ＝
+          ( abs-ℝ (raise-ℝ l1 one-ℝ)) *ℝ
+          ( map-seminorm-Seminormed-ℝ-Vector-Space V v)
+          by ap-mul-ℝ (abs-neg-ℝ _) refl
+        ＝ abs-ℝ one-ℝ *ℝ map-seminorm-Seminormed-ℝ-Vector-Space V v
+          by
+            eq-sim-ℝ
+              ( preserves-sim-right-mul-ℝ _ _ _
+                ( preserves-sim-abs-ℝ (sim-raise-ℝ' l1 one-ℝ)))
+        ＝ one-ℝ *ℝ map-seminorm-Seminormed-ℝ-Vector-Space V v
+          by ap-mul-ℝ (abs-real-ℝ⁺ one-ℝ⁺) refl
+        ＝ map-seminorm-Seminormed-ℝ-Vector-Space V v
+          by left-unit-law-mul-ℝ _
+
+    commutative-dist-Seminormed-ℝ-Vector-Space :
+      (v w : type-Seminormed-ℝ-Vector-Space V) →
+      dist-Seminormed-ℝ-Vector-Space V v w ＝
+      dist-Seminormed-ℝ-Vector-Space V w v
+    commutative-dist-Seminormed-ℝ-Vector-Space v w =
+      ( inv
+        ( ap
+          ( map-seminorm-Seminormed-ℝ-Vector-Space V)
+          ( distributive-neg-diff-Seminormed-ℝ-Vector-Space V w v))) ∙
+      ( seminorm-neg-Seminormed-ℝ-Vector-Space _)
+```
+
+### The distance function on a seminormed vector space satisfies the triangle inequality
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : Seminormed-ℝ-Vector-Space l1 l2)
+  where
+
+  abstract
+    triangular-dist-Seminormed-ℝ-Vector-Space :
+      (v w x : type-Seminormed-ℝ-Vector-Space V) →
+      leq-ℝ
+        ( dist-Seminormed-ℝ-Vector-Space V v x)
+        ( dist-Seminormed-ℝ-Vector-Space V v w +ℝ
+          dist-Seminormed-ℝ-Vector-Space V w x)
+    triangular-dist-Seminormed-ℝ-Vector-Space v w x =
+      let
+        open inequality-reasoning-Large-Poset ℝ-Large-Poset
+      in
+        chain-of-inequalities
+          dist-Seminormed-ℝ-Vector-Space V v x
+          ≤ map-seminorm-Seminormed-ℝ-Vector-Space
+            ( V)
+            ( add-Seminormed-ℝ-Vector-Space
+              ( V)
+              ( diff-Seminormed-ℝ-Vector-Space V v w)
+              ( diff-Seminormed-ℝ-Vector-Space V w x))
+            by
+              leq-eq-ℝ
+                ( ap
+                  ( map-seminorm-Seminormed-ℝ-Vector-Space V)
+                  ( inv (add-diff-Seminormed-ℝ-Vector-Space V v w x)))
+          ≤ ( dist-Seminormed-ℝ-Vector-Space V v w) +ℝ
+            ( dist-Seminormed-ℝ-Vector-Space V w x)
+            by triangular-seminorm-Seminormed-ℝ-Vector-Space V _ _
+```
+
+### The seminorm of a vector is nonnegative
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : Seminormed-ℝ-Vector-Space l1 l2)
+  where
+
+  abstract
+    is-nonnegative-seminorm-Seminormed-ℝ-Vector-Space :
+      (v : type-Seminormed-ℝ-Vector-Space V) →
+      is-nonnegative-ℝ (map-seminorm-Seminormed-ℝ-Vector-Space V v)
+    is-nonnegative-seminorm-Seminormed-ℝ-Vector-Space v =
+      let
+        open inequality-reasoning-Large-Poset ℝ-Large-Poset
+      in
+        reflects-leq-left-mul-ℝ⁺
+          ( positive-real-ℕ⁺ (2 , λ ()))
+          ( zero-ℝ)
+          ( map-seminorm-Seminormed-ℝ-Vector-Space V v)
+          ( chain-of-inequalities
+              real-ℕ 2 *ℝ zero-ℝ
+              ≤ zero-ℝ
+                by leq-sim-ℝ (right-zero-law-mul-ℝ _)
+              ≤ dist-Seminormed-ℝ-Vector-Space V v v
+                by
+                  leq-sim-ℝ
+                    ( symmetric-sim-ℝ
+                      ( sim-zero-diagonal-dist-Seminormed-ℝ-Vector-Space V v))
+              ≤ ( map-seminorm-Seminormed-ℝ-Vector-Space V v) +ℝ
+                ( map-seminorm-Seminormed-ℝ-Vector-Space
+                  ( V)
+                  ( neg-Seminormed-ℝ-Vector-Space V v))
+                by triangular-seminorm-Seminormed-ℝ-Vector-Space V _ _
+              ≤ ( map-seminorm-Seminormed-ℝ-Vector-Space V v) +ℝ
+                ( map-seminorm-Seminormed-ℝ-Vector-Space V v)
+                by
+                  leq-eq-ℝ
+                    ( ap-add-ℝ
+                      ( refl)
+                      ( seminorm-neg-Seminormed-ℝ-Vector-Space V v))
+              ≤ real-ℕ 2 *ℝ map-seminorm-Seminormed-ℝ-Vector-Space V v
+                by leq-eq-ℝ (inv (left-mul-real-ℕ 2 _)))
+
+  nonnegative-seminorm-Seminormed-ℝ-Vector-Space :
+    type-Seminormed-ℝ-Vector-Space V → ℝ⁰⁺ l1
+  nonnegative-seminorm-Seminormed-ℝ-Vector-Space v =
+    ( map-seminorm-Seminormed-ℝ-Vector-Space V v ,
+      is-nonnegative-seminorm-Seminormed-ℝ-Vector-Space v)
+```
+
+### The pseudometric space induced by a seminorm
+
+```agda
+module _
+  {l1 l2 : Level} (V : Seminormed-ℝ-Vector-Space l1 l2)
+  where
+
+  nonnegative-dist-Seminormed-ℝ-Vector-Space :
+    type-Seminormed-ℝ-Vector-Space V → type-Seminormed-ℝ-Vector-Space V → ℝ⁰⁺ l1
+  nonnegative-dist-Seminormed-ℝ-Vector-Space v w =
+    ( dist-Seminormed-ℝ-Vector-Space V v w ,
+      is-nonnegative-seminorm-Seminormed-ℝ-Vector-Space V _)
+
+  neighborhood-prop-Seminormed-ℝ-Vector-Space :
+    ℚ⁺ → Relation-Prop l1 (type-Seminormed-ℝ-Vector-Space V)
+  neighborhood-prop-Seminormed-ℝ-Vector-Space ε v w =
+    leq-prop-ℝ
+      ( dist-Seminormed-ℝ-Vector-Space V v w)
+      ( real-ℚ⁺ ε)
+
+  neighborhood-Seminormed-ℝ-Vector-Space :
+    ℚ⁺ → Relation l1 (type-Seminormed-ℝ-Vector-Space V)
+  neighborhood-Seminormed-ℝ-Vector-Space d =
+    type-Relation-Prop (neighborhood-prop-Seminormed-ℝ-Vector-Space d)
+
+  abstract
+    refl-neighborhood-Seminormed-ℝ-Vector-Space :
+      (ε : ℚ⁺) (v : type-Seminormed-ℝ-Vector-Space V) →
+      neighborhood-Seminormed-ℝ-Vector-Space ε v v
+    refl-neighborhood-Seminormed-ℝ-Vector-Space ε v =
+      leq-le-ℝ
+        ( preserves-le-left-sim-ℝ
+          ( real-ℚ⁺ ε)
+          ( zero-ℝ)
+          ( dist-Seminormed-ℝ-Vector-Space V v v)
+          ( symmetric-sim-ℝ
+            ( sim-zero-diagonal-dist-Seminormed-ℝ-Vector-Space V v))
+          ( preserves-is-positive-real-ℚ (is-positive-rational-ℚ⁺ ε)))
+
+    symmetric-neighborhood-Seminormed-ℝ-Vector-Space :
+      (d : ℚ⁺) (v w : type-Seminormed-ℝ-Vector-Space V) →
+      neighborhood-Seminormed-ℝ-Vector-Space d v w →
+      neighborhood-Seminormed-ℝ-Vector-Space d w v
+    symmetric-neighborhood-Seminormed-ℝ-Vector-Space d v w =
+      tr
+        ( λ z → leq-ℝ z (real-ℚ⁺ d))
+        ( commutative-dist-Seminormed-ℝ-Vector-Space V v w)
+
+    triangular-neighborhood-Seminormed-ℝ-Vector-Space :
+      (v w x : type-Seminormed-ℝ-Vector-Space V) (d1 d2 : ℚ⁺) →
+      neighborhood-Seminormed-ℝ-Vector-Space d2 w x →
+      neighborhood-Seminormed-ℝ-Vector-Space d1 v w →
+      neighborhood-Seminormed-ℝ-Vector-Space (d1 +ℚ⁺ d2) v x
+    triangular-neighborhood-Seminormed-ℝ-Vector-Space
+      v w x d1 d2 Nd2wx Nd1vw =
+      let
+        open inequality-reasoning-Large-Poset ℝ-Large-Poset
+      in
+        chain-of-inequalities
+        dist-Seminormed-ℝ-Vector-Space V v x
+        ≤ ( dist-Seminormed-ℝ-Vector-Space V v w) +ℝ
+          ( dist-Seminormed-ℝ-Vector-Space V w x)
+          by triangular-dist-Seminormed-ℝ-Vector-Space V v w x
+        ≤ real-ℚ⁺ d1 +ℝ real-ℚ⁺ d2
+          by preserves-leq-add-ℝ Nd1vw Nd2wx
+        ≤ real-ℚ⁺ (d1 +ℚ⁺ d2)
+          by leq-eq-ℝ (add-real-ℚ _ _)
+
+    saturated-neighborhood-Seminormed-ℝ-Vector-Space :
+      (d : ℚ⁺) (v w : type-Seminormed-ℝ-Vector-Space V) →
+      ((δ : ℚ⁺) → neighborhood-Seminormed-ℝ-Vector-Space (d +ℚ⁺ δ) v w) →
+      neighborhood-Seminormed-ℝ-Vector-Space d v w
+    saturated-neighborhood-Seminormed-ℝ-Vector-Space d v w H =
+      saturated-leq-ℝ⁰⁺
+        ( nonnegative-dist-Seminormed-ℝ-Vector-Space v w)
+        ( nonnegative-real-ℚ⁺ d)
+        ( λ δ →
+          inv-tr
+            ( leq-ℝ (dist-Seminormed-ℝ-Vector-Space V v w))
+            ( add-real-ℚ _ _)
+            ( H δ))
+
+  pseudometric-structure-Seminormed-ℝ-Vector-Space :
+    Pseudometric-Structure l1 (type-Seminormed-ℝ-Vector-Space V)
+  pseudometric-structure-Seminormed-ℝ-Vector-Space =
+    ( neighborhood-prop-Seminormed-ℝ-Vector-Space ,
+      refl-neighborhood-Seminormed-ℝ-Vector-Space ,
+      symmetric-neighborhood-Seminormed-ℝ-Vector-Space ,
+      triangular-neighborhood-Seminormed-ℝ-Vector-Space ,
+      saturated-neighborhood-Seminormed-ℝ-Vector-Space)
+
+  pseudometric-space-Seminormed-ℝ-Vector-Space : Pseudometric-Space l2 l1
+  pseudometric-space-Seminormed-ℝ-Vector-Space =
+    ( type-Seminormed-ℝ-Vector-Space V ,
+      pseudometric-structure-Seminormed-ℝ-Vector-Space)
+```
+
+### The real numbers are a seminormed vector space over themselves with seminorm `x ↦ |x|`
+
+```agda
+seminormed-real-vector-space-ℝ :
+  (l : Level) → Seminormed-ℝ-Vector-Space l (lsuc l)
+seminormed-real-vector-space-ℝ l =
+  ( real-vector-space-ℝ l , abs-ℝ , triangle-inequality-abs-ℝ , abs-mul-ℝ)
+```
diff --git a/src/metric-spaces/metrics-of-metric-spaces.lagda.md b/src/metric-spaces/metrics-of-metric-spaces.lagda.md
index ea6ba29759..a918f42c78 100644
--- a/src/metric-spaces/metrics-of-metric-spaces.lagda.md
+++ b/src/metric-spaces/metrics-of-metric-spaces.lagda.md
@@ -109,7 +109,7 @@ module _
     is-reflexive-is-metric-of-Metric-Space :
       is-reflexive-distance-function (set-Metric-Space M) ρ
     is-reflexive-is-metric-of-Metric-Space x =
-      sim-zero-le-positive-rational-ℝ⁰⁺
+      sim-zero-leq-positive-rational-ℝ⁰⁺
         ( ρ x x)
         ( λ ε →
           forward-implication
diff --git a/src/metric-spaces/metrics.lagda.md b/src/metric-spaces/metrics.lagda.md
index 6ed22735b3..67cc1c541a 100644
--- a/src/metric-spaces/metrics.lagda.md
+++ b/src/metric-spaces/metrics.lagda.md
@@ -297,7 +297,7 @@ module _
       is-tight-Pseudometric-Space (pseudometric-space-Metric X μ)
     is-tight-pseudometric-space-Metric x y H =
       is-extensional-dist-Metric X μ x y
-        ( sim-zero-le-positive-rational-ℝ⁰⁺ (dist-Metric X μ x y) H)
+        ( sim-zero-leq-positive-rational-ℝ⁰⁺ (dist-Metric X μ x y) H)
 ```
 
 ### The pseudometric space induced by a metric is extensional
diff --git a/src/real-numbers/absolute-value-real-numbers.lagda.md b/src/real-numbers/absolute-value-real-numbers.lagda.md
index 371e592c16..120e455dd4 100644
--- a/src/real-numbers/absolute-value-real-numbers.lagda.md
+++ b/src/real-numbers/absolute-value-real-numbers.lagda.md
@@ -218,6 +218,18 @@ module _
             ( neg-leq-ℝ
               ( transitive-leq-ℝ _ _ _ (leq-sim-ℝ |x|~0) (neg-leq-abs-ℝ x))))
 
+abstract
+  eq-raise-zero-eq-raise-zero-abs-ℝ :
+    {l : Level} (x : ℝ l) → abs-ℝ x ＝ raise-ℝ l zero-ℝ → x ＝ raise-ℝ l zero-ℝ
+  eq-raise-zero-eq-raise-zero-abs-ℝ {l} x |x|=0 =
+    eq-sim-ℝ
+      ( transitive-sim-ℝ _ _ _
+        ( sim-raise-ℝ l zero-ℝ)
+        ( sim-zero-sim-zero-abs-ℝ x
+          ( transitive-sim-ℝ _ _ _
+            ( sim-raise-ℝ' l zero-ℝ)
+            ( sim-eq-ℝ |x|=0))))
+
 module _
   (x : ℝ lzero) (|x|=0 : abs-ℝ x ＝ zero-ℝ)
   where
diff --git a/src/real-numbers/multiplication-real-numbers.lagda.md b/src/real-numbers/multiplication-real-numbers.lagda.md
index a4d70e4bbd..002c926006 100644
--- a/src/real-numbers/multiplication-real-numbers.lagda.md
+++ b/src/real-numbers/multiplication-real-numbers.lagda.md
@@ -1038,33 +1038,6 @@ abstract
         by ap-add-ℝ (commutative-mul-ℝ z x) (commutative-mul-ℝ z y)
 ```
 
-### Zero laws
-
-```agda
-module _
-  {l : Level} (x : ℝ l)
-  where
-
-  abstract
-    left-zero-law-mul-ℝ : sim-ℝ (zero-ℝ *ℝ x) zero-ℝ
-    left-zero-law-mul-ℝ =
-      inv-tr
-        ( λ y → sim-ℝ y zero-ℝ)
-        ( is-zero-is-idempotent-Ab
-          ( ab-add-ℝ l)
-          ( equational-reasoning
-            zero-ℝ *ℝ x +ℝ zero-ℝ *ℝ x
-            ＝ (zero-ℝ +ℝ zero-ℝ) *ℝ x
-              by inv (right-distributive-mul-add-ℝ zero-ℝ zero-ℝ x)
-            ＝ zero-ℝ *ℝ x
-              by ap-mul-ℝ (left-unit-law-add-ℝ zero-ℝ) refl))
-        ( symmetric-sim-ℝ (sim-raise-ℝ l zero-ℝ))
-
-    right-zero-law-mul-ℝ : sim-ℝ (x *ℝ zero-ℝ) zero-ℝ
-    right-zero-law-mul-ℝ =
-      tr (λ y → sim-ℝ y zero-ℝ) (commutative-mul-ℝ _ _) left-zero-law-mul-ℝ
-```
-
 ### The inclusion of rational numbers preserves multiplication
 
 ```agda
@@ -1166,6 +1139,51 @@ abstract
       ( preserves-sim-left-mul-ℝ a b b' b~b')
 ```
 
+### Zero laws
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  abstract
+    left-zero-law-mul-ℝ : sim-ℝ (zero-ℝ *ℝ x) zero-ℝ
+    left-zero-law-mul-ℝ =
+      inv-tr
+        ( λ y → sim-ℝ y zero-ℝ)
+        ( is-zero-is-idempotent-Ab
+          ( ab-add-ℝ l)
+          ( equational-reasoning
+            zero-ℝ *ℝ x +ℝ zero-ℝ *ℝ x
+            ＝ (zero-ℝ +ℝ zero-ℝ) *ℝ x
+              by inv (right-distributive-mul-add-ℝ zero-ℝ zero-ℝ x)
+            ＝ zero-ℝ *ℝ x
+              by ap-mul-ℝ (left-unit-law-add-ℝ zero-ℝ) refl))
+        ( symmetric-sim-ℝ (sim-raise-ℝ l zero-ℝ))
+
+    left-raise-zero-law-mul-ℝ :
+      raise-zero-ℝ l *ℝ x ＝ raise-zero-ℝ l
+    left-raise-zero-law-mul-ℝ =
+      eq-sim-ℝ
+        ( similarity-reasoning-ℝ
+          raise-zero-ℝ l *ℝ x
+          ~ℝ zero-ℝ *ℝ x
+            by
+              preserves-sim-right-mul-ℝ
+                ( x)
+                ( raise-zero-ℝ l)
+                ( zero-ℝ)
+                ( sim-raise-ℝ' l zero-ℝ)
+          ~ℝ zero-ℝ
+            by left-zero-law-mul-ℝ
+          ~ℝ raise-zero-ℝ l
+            by sim-raise-ℝ l zero-ℝ)
+
+    right-zero-law-mul-ℝ : sim-ℝ (x *ℝ zero-ℝ) zero-ℝ
+    right-zero-law-mul-ℝ =
+      tr (λ y → sim-ℝ y zero-ℝ) (commutative-mul-ℝ _ _) left-zero-law-mul-ℝ
+```
+
 ### Swapping laws for multiplication on real numbers
 
 ```agda
diff --git a/src/real-numbers/positive-real-numbers.lagda.md b/src/real-numbers/positive-real-numbers.lagda.md
index d00d7fc4b6..b924f8f662 100644
--- a/src/real-numbers/positive-real-numbers.lagda.md
+++ b/src/real-numbers/positive-real-numbers.lagda.md
@@ -9,6 +9,10 @@ module real-numbers.positive-real-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.integers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonzero-natural-numbers
+open import elementary-number-theory.positive-integers
 open import elementary-number-theory.positive-rational-numbers
 open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.strict-inequality-positive-rational-numbers
@@ -256,6 +260,32 @@ is-positive-one-ℝ : is-positive-ℝ one-ℝ
 is-positive-one-ℝ = is-positive-real-ℝ⁺ one-ℝ⁺
 ```
 
+### The canonical embedding of integers preserves positivity
+
+```agda
+abstract
+  preserves-is-positive-real-ℤ :
+    {x : ℤ} → is-positive-ℤ x → is-positive-ℝ (real-ℤ x)
+  preserves-is-positive-real-ℤ pos-x =
+    preserves-is-positive-real-ℚ (is-positive-rational-ℤ pos-x)
+
+positive-real-ℤ⁺ : ℤ⁺ → ℝ⁺ lzero
+positive-real-ℤ⁺ (x , pos-x) = (real-ℤ x , preserves-is-positive-real-ℤ pos-x)
+```
+
+### The canonical embedding of a nonzero natural number is positive
+
+```agda
+abstract
+  is-positive-real-is-nonzero-ℕ :
+    {n : ℕ} → is-nonzero-ℕ n → is-positive-ℝ (real-ℕ n)
+  is-positive-real-is-nonzero-ℕ n≠0 =
+    preserves-is-positive-real-ℤ (is-positive-int-is-nonzero-ℕ _ n≠0)
+
+positive-real-ℕ⁺ : ℕ⁺ → ℝ⁺ lzero
+positive-real-ℕ⁺ (n , n≠0) = (real-ℕ n , is-positive-real-is-nonzero-ℕ n≠0)
+```
+
 ### `x` is positive if and only if there exists a positive rational number it is not less than or equal to
 
 ```agda
diff --git a/src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md b/src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md
index 69f3a5fb11..ef8ef84722 100644
--- a/src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md
+++ b/src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md
@@ -57,15 +57,16 @@ module _
 ### If a nonnegative real number is less than or equal to all positive rational numbers, it is similar to zero
 
 ```agda
-sim-zero-le-positive-rational-ℝ⁰⁺ :
-  {l : Level} (x : ℝ⁰⁺ l) →
-  ((ε : ℚ⁺) → leq-ℝ⁰⁺ x (nonnegative-real-ℚ⁺ ε)) →
-  sim-zero-ℝ⁰⁺ x
-sim-zero-le-positive-rational-ℝ⁰⁺ x H =
-  sim-sim-leq-ℝ
-    ( leq-zero-ℝ⁰⁺ x ,
-      saturated-leq-ℝ⁰⁺
-        ( x)
-        ( zero-ℝ⁰⁺)
-        ( λ ε → inv-tr (leq-ℝ⁰⁺ x) (left-unit-law-add-ℝ⁰⁺ _) (H ε)))
+abstract
+  sim-zero-leq-positive-rational-ℝ⁰⁺ :
+    {l : Level} (x : ℝ⁰⁺ l) →
+    ((ε : ℚ⁺) → leq-ℝ⁰⁺ x (nonnegative-real-ℚ⁺ ε)) →
+    sim-zero-ℝ⁰⁺ x
+  sim-zero-leq-positive-rational-ℝ⁰⁺ x H =
+    sim-sim-leq-ℝ
+      ( leq-zero-ℝ⁰⁺ x ,
+        saturated-leq-ℝ⁰⁺
+          ( x)
+          ( zero-ℝ⁰⁺)
+          ( λ ε → inv-tr (leq-ℝ⁰⁺ x) (left-unit-law-add-ℝ⁰⁺ _) (H ε)))
 ```