diff --git a/src/analysis.lagda.md b/src/analysis.lagda.md
index c3893468cc..21e355eece 100644
--- a/src/analysis.lagda.md
+++ b/src/analysis.lagda.md
@@ -3,8 +3,17 @@
 ```agda
 module analysis where
 
+open import analysis.complete-metric-abelian-groups public
+open import analysis.complete-metric-abelian-groups-real-banach-spaces public
+open import analysis.convergent-series-complete-metric-abelian-groups public
 open import analysis.convergent-series-metric-abelian-groups public
+open import analysis.convergent-series-real-banach-spaces public
+open import analysis.convergent-series-real-numbers public
 open import analysis.derivatives-of-real-functions-on-proper-closed-intervals public
 open import analysis.metric-abelian-groups public
+open import analysis.metric-abelian-groups-normed-real-vector-spaces public
+open import analysis.series-complete-metric-abelian-groups public
 open import analysis.series-metric-abelian-groups public
+open import analysis.series-real-banach-spaces public
+open import analysis.series-real-numbers public
 ```
diff --git a/src/analysis/complete-metric-abelian-groups-real-banach-spaces.lagda.md b/src/analysis/complete-metric-abelian-groups-real-banach-spaces.lagda.md
new file mode 100644
index 0000000000..40aa017885
--- /dev/null
+++ b/src/analysis/complete-metric-abelian-groups-real-banach-spaces.lagda.md
@@ -0,0 +1,63 @@
+# Complete metric abelian groups of real Banach spaces
+
+```agda
+module analysis.complete-metric-abelian-groups-real-banach-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.complete-metric-abelian-groups
+open import analysis.metric-abelian-groups
+open import analysis.metric-abelian-groups-normed-real-vector-spaces
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import linear-algebra.real-banach-spaces
+
+open import real-numbers.metric-additive-group-of-real-numbers
+```
+
+</details>
+
+## Idea
+
+Every [real Banach space](linear-algebra.real-banach-spaces.md) forms a
+[complete metric abelian group](analysis.complete-metric-abelian-groups.md)
+under addition.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  where
+
+  metric-ab-add-ℝ-Banach-Space : Metric-Ab l2 l1
+  metric-ab-add-ℝ-Banach-Space =
+    metric-ab-Normed-ℝ-Vector-Space (normed-vector-space-ℝ-Banach-Space V)
+
+  complete-metric-ab-add-ℝ-Banach-Space : Complete-Metric-Ab l2 l1
+  complete-metric-ab-add-ℝ-Banach-Space =
+    ( metric-ab-add-ℝ-Banach-Space , is-complete-metric-space-ℝ-Banach-Space V)
+```
+
+## Properties
+
+### The complete metric abelian group from the reals as a real Banach space equals the standard complete metric abelian group of the reals under addition
+
+```agda
+abstract
+  eq-complete-metric-ab-ℝ :
+    (l : Level) →
+    complete-metric-ab-add-ℝ-Banach-Space (real-banach-space-ℝ l) ＝
+    complete-metric-ab-add-ℝ l
+  eq-complete-metric-ab-ℝ l =
+    eq-type-subtype
+      ( is-complete-prop-Metric-Ab)
+      ( eq-metric-ab-normed-real-vector-space-metric-ab-ℝ l)
+```
diff --git a/src/analysis/complete-metric-abelian-groups.lagda.md b/src/analysis/complete-metric-abelian-groups.lagda.md
new file mode 100644
index 0000000000..e629810ef1
--- /dev/null
+++ b/src/analysis/complete-metric-abelian-groups.lagda.md
@@ -0,0 +1,65 @@
+# Complete metric abelian groups
+
+```agda
+module analysis.complete-metric-abelian-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.metric-abelian-groups
+
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import metric-spaces.complete-metric-spaces
+open import metric-spaces.metric-spaces
+```
+
+</details>
+
+## Idea
+
+A {{#concept "complete metric abelian group" Agda=Complete-Metric-Ab}} is a
+[metric abelian group](analysis.metric-abelian-groups.md) whose associated
+[metric space](metric-spaces.metric-spaces.md) is
+[complete](metric-spaces.complete-metric-spaces.md).
+
+## Definition
+
+```agda
+is-complete-prop-Metric-Ab : {l1 l2 : Level} → Metric-Ab l1 l2 → Prop (l1 ⊔ l2)
+is-complete-prop-Metric-Ab G =
+  is-complete-prop-Metric-Space (metric-space-Metric-Ab G)
+
+is-complete-Metric-Ab : {l1 l2 : Level} → Metric-Ab l1 l2 → UU (l1 ⊔ l2)
+is-complete-Metric-Ab G = is-complete-Metric-Space (metric-space-Metric-Ab G)
+
+Complete-Metric-Ab : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Complete-Metric-Ab l1 l2 = type-subtype (is-complete-prop-Metric-Ab {l1} {l2})
+```
+
+## Properties
+
+```agda
+module _
+  {l1 l2 : Level}
+  (G : Complete-Metric-Ab l1 l2)
+  where
+
+  metric-ab-Complete-Metric-Ab : Metric-Ab l1 l2
+  metric-ab-Complete-Metric-Ab = pr1 G
+
+  metric-space-Complete-Metric-Ab : Metric-Space l1 l2
+  metric-space-Complete-Metric-Ab =
+    metric-space-Metric-Ab metric-ab-Complete-Metric-Ab
+
+  complete-metric-space-Complete-Metric-Ab : Complete-Metric-Space l1 l2
+  complete-metric-space-Complete-Metric-Ab =
+    ( metric-space-Complete-Metric-Ab , pr2 G)
+
+  type-Complete-Metric-Ab : UU l1
+  type-Complete-Metric-Ab = type-Metric-Ab metric-ab-Complete-Metric-Ab
+```
diff --git a/src/analysis/convergent-series-complete-metric-abelian-groups.lagda.md b/src/analysis/convergent-series-complete-metric-abelian-groups.lagda.md
new file mode 100644
index 0000000000..49b1ac0dcc
--- /dev/null
+++ b/src/analysis/convergent-series-complete-metric-abelian-groups.lagda.md
@@ -0,0 +1,79 @@
+# Convergent series in complete metric abelian groups
+
+```agda
+module analysis.convergent-series-complete-metric-abelian-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.complete-metric-abelian-groups
+open import analysis.convergent-series-metric-abelian-groups
+open import analysis.series-complete-metric-abelian-groups
+
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import metric-spaces.cauchy-sequences-complete-metric-spaces
+open import metric-spaces.cauchy-sequences-metric-spaces
+```
+
+</details>
+
+## Idea
+
+A [series](analysis.series-metric-abelian-groups.md)
+[converges](analysis.convergent-series-metric-abelian-groups.md) in a
+[complete metric abelian group](analysis.complete-metric-abelian-groups.md) if
+its partial sums form a
+[Cauchy sequence](metric-spaces.cauchy-sequences-metric-spaces.md).
+
+A slightly modified converse is also true: if a series converges, there
+[exists](foundation.existential-quantification.md) a modulus making it a Cauchy
+sequence.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (G : Complete-Metric-Ab l1 l2)
+  (σ : series-Complete-Metric-Ab G)
+  where
+
+  is-sum-prop-series-Complete-Metric-Ab : type-Complete-Metric-Ab G → Prop l2
+  is-sum-prop-series-Complete-Metric-Ab = is-sum-prop-series-Metric-Ab σ
+
+  is-sum-series-Complete-Metric-Ab : type-Complete-Metric-Ab G → UU l2
+  is-sum-series-Complete-Metric-Ab = is-sum-series-Metric-Ab σ
+
+  is-convergent-prop-series-Complete-Metric-Ab : Prop (l1 ⊔ l2)
+  is-convergent-prop-series-Complete-Metric-Ab =
+    is-convergent-prop-series-Metric-Ab σ
+
+  is-convergent-series-Complete-Metric-Ab : UU (l1 ⊔ l2)
+  is-convergent-series-Complete-Metric-Ab = is-convergent-series-Metric-Ab σ
+```
+
+## Properties
+
+### If the partial sums of a series form a Cauchy sequence, the series converges
+
+```agda
+module _
+  {l1 l2 : Level}
+  (G : Complete-Metric-Ab l1 l2)
+  (σ : series-Complete-Metric-Ab G)
+  where
+
+  is-convergent-is-cauchy-sequence-partial-sum-series-Complete-Metric-Ab :
+    is-cauchy-sequence-Metric-Space
+      ( metric-space-Complete-Metric-Ab G)
+      ( partial-sum-series-Complete-Metric-Ab G σ) →
+    is-convergent-series-Complete-Metric-Ab G σ
+  is-convergent-is-cauchy-sequence-partial-sum-series-Complete-Metric-Ab H =
+    has-limit-cauchy-sequence-Complete-Metric-Space
+      ( complete-metric-space-Complete-Metric-Ab G)
+      ( partial-sum-series-Complete-Metric-Ab G σ , H)
+```
diff --git a/src/analysis/convergent-series-real-banach-spaces.lagda.md b/src/analysis/convergent-series-real-banach-spaces.lagda.md
new file mode 100644
index 0000000000..63fef039f3
--- /dev/null
+++ b/src/analysis/convergent-series-real-banach-spaces.lagda.md
@@ -0,0 +1,79 @@
+# Convergent series in real Banach spaces
+
+```agda
+module analysis.convergent-series-real-banach-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.complete-metric-abelian-groups-real-banach-spaces
+open import analysis.convergent-series-complete-metric-abelian-groups
+open import analysis.convergent-series-metric-abelian-groups
+open import analysis.series-real-banach-spaces
+
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import linear-algebra.real-banach-spaces
+
+open import metric-spaces.cauchy-sequences-metric-spaces
+```
+
+</details>
+
+## Idea
+
+A [series](analysis.series-real-banach-spaces.md)
+[converges](analysis.convergent-series-metric-abelian-groups.md) in a
+[real Banach space](linear-algebra.real-banach-spaces.md) if its partial sums
+form a [Cauchy sequence](metric-spaces.cauchy-sequences-metric-spaces.md).
+
+A slightly modified converse is also true: if a series converges, there
+[exists](foundation.existential-quantification.md) a modulus making it a Cauchy
+sequence.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  (σ : series-ℝ-Banach-Space V)
+  where
+
+  is-sum-prop-series-ℝ-Banach-Space : type-ℝ-Banach-Space V → Prop l1
+  is-sum-prop-series-ℝ-Banach-Space = is-sum-prop-series-Metric-Ab σ
+
+  is-sum-series-ℝ-Banach-Space : type-ℝ-Banach-Space V → UU l1
+  is-sum-series-ℝ-Banach-Space = is-sum-series-Metric-Ab σ
+
+  is-convergent-prop-series-ℝ-Banach-Space : Prop (l1 ⊔ l2)
+  is-convergent-prop-series-ℝ-Banach-Space =
+    is-convergent-prop-series-Metric-Ab σ
+
+  is-convergent-series-ℝ-Banach-Space : UU (l1 ⊔ l2)
+  is-convergent-series-ℝ-Banach-Space = is-convergent-series-Metric-Ab σ
+```
+
+## Properties
+
+### If the partial sums of a series form a Cauchy sequence, the series converges
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  (σ : series-ℝ-Banach-Space V)
+  where
+
+  is-convergent-is-cauchy-sequence-partial-sum-series-ℝ-Banach-Space :
+    is-cauchy-sequence-Metric-Space
+      ( metric-space-ℝ-Banach-Space V)
+      ( partial-sum-series-ℝ-Banach-Space V σ) →
+    is-convergent-series-ℝ-Banach-Space V σ
+  is-convergent-is-cauchy-sequence-partial-sum-series-ℝ-Banach-Space =
+    is-convergent-is-cauchy-sequence-partial-sum-series-Complete-Metric-Ab
+      ( complete-metric-ab-add-ℝ-Banach-Space V)
+      ( σ)
+```
diff --git a/src/analysis/convergent-series-real-numbers.lagda.md b/src/analysis/convergent-series-real-numbers.lagda.md
new file mode 100644
index 0000000000..a7c911dd9e
--- /dev/null
+++ b/src/analysis/convergent-series-real-numbers.lagda.md
@@ -0,0 +1,74 @@
+# Convergent series in the real numbers
+
+```agda
+module analysis.convergent-series-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.convergent-series-complete-metric-abelian-groups
+open import analysis.convergent-series-metric-abelian-groups
+open import analysis.series-real-numbers
+
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import real-numbers.cauchy-sequences-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.metric-additive-group-of-real-numbers
+```
+
+</details>
+
+## Idea
+
+A [series of real numbers](analysis.series-real-numbers.md) is
+{{#concept "convergent" Disambiguation="series in 𝐑" Agda=is-convergent-series-ℝ Agda=convergent-series-ℝ WDID=Q1211057 WD="convergent series"}}
+if its partial sums converge in the
+[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md).
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (σ : series-ℝ l)
+  where
+
+  is-sum-prop-series-ℝ : ℝ l → Prop l
+  is-sum-prop-series-ℝ = is-sum-prop-series-Metric-Ab σ
+
+  is-sum-series-ℝ : ℝ l → UU l
+  is-sum-series-ℝ = is-sum-series-Metric-Ab σ
+
+  is-convergent-prop-series-ℝ : Prop (lsuc l)
+  is-convergent-prop-series-ℝ =
+    is-convergent-prop-series-Metric-Ab σ
+
+  is-convergent-series-ℝ : UU (lsuc l)
+  is-convergent-series-ℝ = is-convergent-series-Metric-Ab σ
+```
+
+## Properties
+
+### If the partial sums of a series form a Cauchy sequence, the series converges
+
+```agda
+module _
+  {l : Level}
+  (σ : series-ℝ l)
+  where
+
+  is-convergent-is-cauchy-sequence-partial-sum-series-ℝ :
+    is-cauchy-sequence-ℝ (partial-sum-series-ℝ σ) →
+    is-convergent-series-ℝ σ
+  is-convergent-is-cauchy-sequence-partial-sum-series-ℝ =
+    is-convergent-is-cauchy-sequence-partial-sum-series-Complete-Metric-Ab
+      ( complete-metric-ab-add-ℝ l)
+      ( σ)
+```
+
+## External links
+
+- [Convergent series](https://en.wikipedia.org/wiki/Ratio_test) on Wikipedia
diff --git a/src/analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md b/src/analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md
new file mode 100644
index 0000000000..4ee09d54d5
--- /dev/null
+++ b/src/analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md
@@ -0,0 +1,94 @@
+# Metric abelian groups of normed real vector spaces
+
+```agda
+module analysis.metric-abelian-groups-normed-real-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.metric-abelian-groups
+
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+
+open import linear-algebra.normed-real-vector-spaces
+
+open import metric-spaces.extensionality-pseudometric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.pseudometric-spaces
+open import metric-spaces.rational-neighborhood-relations
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.distance-real-numbers
+open import real-numbers.large-additive-group-of-real-numbers
+open import real-numbers.metric-additive-group-of-real-numbers
+```
+
+</details>
+
+## Idea
+
+A [normed](linear-algebra.normed-real-vector-spaces.md)
+[real vector space](linear-algebra.real-vector-spaces.md) forms a
+[metric abelian group](analysis.metric-abelian-groups.md) under addition.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : Normed-ℝ-Vector-Space l1 l2)
+  where
+
+  ab-metric-ab-Normed-ℝ-Vector-Space : Ab l2
+  ab-metric-ab-Normed-ℝ-Vector-Space = ab-Normed-ℝ-Vector-Space V
+
+  type-metric-ab-Normed-ℝ-Vector-Space : UU l2
+  type-metric-ab-Normed-ℝ-Vector-Space = type-Normed-ℝ-Vector-Space V
+
+  pseudometric-structure-metric-ab-Normed-ℝ-Vector-Space :
+    Pseudometric-Structure l1 type-metric-ab-Normed-ℝ-Vector-Space
+  pseudometric-structure-metric-ab-Normed-ℝ-Vector-Space =
+    pseudometric-structure-Metric-Space (metric-space-Normed-ℝ-Vector-Space V)
+
+  pseudometric-space-metric-ab-Normed-ℝ-Vector-Space :
+    Pseudometric-Space l2 l1
+  pseudometric-space-metric-ab-Normed-ℝ-Vector-Space =
+    pseudometric-Metric-Space (metric-space-Normed-ℝ-Vector-Space V)
+
+  metric-ab-Normed-ℝ-Vector-Space : Metric-Ab l2 l1
+  metric-ab-Normed-ℝ-Vector-Space =
+    ( ab-metric-ab-Normed-ℝ-Vector-Space ,
+      pseudometric-structure-metric-ab-Normed-ℝ-Vector-Space ,
+      is-extensional-pseudometric-Metric-Space
+        ( metric-space-Normed-ℝ-Vector-Space V) ,
+      is-isometry-neg-Normed-ℝ-Vector-Space V ,
+      is-isometry-left-add-Normed-ℝ-Vector-Space V)
+```
+
+## Properties
+
+### The metric abelian group associated with `ℝ` as a normed vector space over `ℝ` is equal to the metric additive group of `ℝ`
+
+```agda
+abstract
+  eq-metric-ab-normed-real-vector-space-metric-ab-ℝ :
+    (l : Level) →
+    metric-ab-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l) ＝
+    metric-ab-add-ℝ l
+  eq-metric-ab-normed-real-vector-space-metric-ab-ℝ l =
+    eq-pair-eq-fiber
+      ( eq-type-subtype
+        ( λ M → is-metric-ab-prop-Ab-Pseudometric-Structure (ab-add-ℝ l) M)
+        ( eq-type-subtype
+          ( is-pseudometric-prop-Rational-Neighborhood-Relation (ℝ l))
+          ( eq-Eq-Rational-Neighborhood-Relation _ _
+            ( λ d x y → inv-iff (neighborhood-iff-leq-dist-ℝ d x y)))))
+```
diff --git a/src/analysis/metric-abelian-groups.lagda.md b/src/analysis/metric-abelian-groups.lagda.md
index 3306202936..fe8317d466 100644
--- a/src/analysis/metric-abelian-groups.lagda.md
+++ b/src/analysis/metric-abelian-groups.lagda.md
@@ -12,8 +12,10 @@ open import elementary-number-theory.positive-rational-numbers
 open import foundation.action-on-identifications-binary-functions
 open import foundation.binary-relations
 open import foundation.cartesian-product-types
+open import foundation.conjunction
 open import foundation.dependent-pair-types
 open import foundation.identity-types
+open import foundation.propositions
 open import foundation.universe-levels
 
 open import group-theory.abelian-groups
@@ -39,18 +41,25 @@ and negation operation are
 ## Definition
 
 ```agda
+is-metric-ab-prop-Ab-Pseudometric-Structure :
+  {l1 l2 : Level} (G : Ab l1) (M : Pseudometric-Structure l2 (type-Ab G)) →
+  Prop (l1 ⊔ l2)
+is-metric-ab-prop-Ab-Pseudometric-Structure G M =
+  let
+    MS = (type-Ab G , M)
+  in
+    is-extensional-prop-Pseudometric-Space MS ∧
+    is-isometry-prop-Pseudometric-Space MS MS (neg-Ab G) ∧
+    Π-Prop
+      ( type-Ab G)
+      ( λ x → is-isometry-prop-Pseudometric-Space MS MS (add-Ab G x))
+
 Metric-Ab : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
 Metric-Ab l1 l2 =
   Σ ( Ab l1)
     ( λ G →
       Σ ( Pseudometric-Structure l2 (type-Ab G))
-        ( λ M →
-          let MS = (type-Ab G , M)
-          in
-            is-extensional-Pseudometric-Space MS ×
-            is-isometry-Pseudometric-Space MS MS (neg-Ab G) ×
-            ( (x : type-Ab G) →
-              is-isometry-Pseudometric-Space MS MS (add-Ab G x))))
+        ( λ M → type-Prop (is-metric-ab-prop-Ab-Pseudometric-Structure G M)))
 
 module _
   {l1 l2 : Level} (MG : Metric-Ab l1 l2)
diff --git a/src/analysis/series-complete-metric-abelian-groups.lagda.md b/src/analysis/series-complete-metric-abelian-groups.lagda.md
new file mode 100644
index 0000000000..bb936a8eb0
--- /dev/null
+++ b/src/analysis/series-complete-metric-abelian-groups.lagda.md
@@ -0,0 +1,49 @@
+# Series in complete metric abelian groups
+
+```agda
+module analysis.series-complete-metric-abelian-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.complete-metric-abelian-groups
+open import analysis.series-metric-abelian-groups
+
+open import foundation.universe-levels
+
+open import lists.sequences
+```
+
+</details>
+
+## Idea
+
+A [series](analysis.series-metric-abelian-groups.md) in a
+[complete metric abelian group](analysis.complete-metric-abelian-groups.md) is a
+series in the underlying
+[metric abelian group](analysis.metric-abelian-groups.md).
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (G : Complete-Metric-Ab l1 l2)
+  where
+
+  series-Complete-Metric-Ab : UU l1
+  series-Complete-Metric-Ab = series-Metric-Ab (metric-ab-Complete-Metric-Ab G)
+
+  series-terms-Complete-Metric-Ab :
+    sequence (type-Complete-Metric-Ab G) → series-Complete-Metric-Ab
+  series-terms-Complete-Metric-Ab = series-terms-Metric-Ab
+
+  term-series-Complete-Metric-Ab :
+    series-Complete-Metric-Ab → sequence (type-Complete-Metric-Ab G)
+  term-series-Complete-Metric-Ab = term-series-Metric-Ab
+
+  partial-sum-series-Complete-Metric-Ab :
+    series-Complete-Metric-Ab → sequence (type-Complete-Metric-Ab G)
+  partial-sum-series-Complete-Metric-Ab = partial-sum-series-Metric-Ab
+```
diff --git a/src/analysis/series-real-banach-spaces.lagda.md b/src/analysis/series-real-banach-spaces.lagda.md
new file mode 100644
index 0000000000..dc7d5b3651
--- /dev/null
+++ b/src/analysis/series-real-banach-spaces.lagda.md
@@ -0,0 +1,56 @@
+# Series in real Banach spaces
+
+```agda
+module analysis.series-real-banach-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.metric-abelian-groups-normed-real-vector-spaces
+open import analysis.series-metric-abelian-groups
+
+open import foundation.universe-levels
+
+open import linear-algebra.real-banach-spaces
+
+open import lists.sequences
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "series" Disambiguation="in a real Banach space" Agda=series-ℝ-Banach-Space}}
+is a [series](analysis.series-metric-abelian-groups.md) in the
+[metric abelian group](analysis.metric-abelian-groups.md)
+[associated](analysis.metric-abelian-groups-normed-real-vector-spaces.md) with
+the underlying
+[normed real vector space](linear-algebra.normed-real-vector-spaces.md).
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  where
+
+  series-ℝ-Banach-Space : UU l2
+  series-ℝ-Banach-Space =
+    series-Metric-Ab
+      ( metric-ab-Normed-ℝ-Vector-Space (normed-vector-space-ℝ-Banach-Space V))
+
+  series-terms-ℝ-Banach-Space :
+    sequence (type-ℝ-Banach-Space V) → series-ℝ-Banach-Space
+  series-terms-ℝ-Banach-Space = series-terms-Metric-Ab
+
+  term-series-ℝ-Banach-Space :
+    series-ℝ-Banach-Space → sequence (type-ℝ-Banach-Space V)
+  term-series-ℝ-Banach-Space = term-series-Metric-Ab
+
+  partial-sum-series-ℝ-Banach-Space :
+    series-ℝ-Banach-Space → sequence (type-ℝ-Banach-Space V)
+  partial-sum-series-ℝ-Banach-Space = partial-sum-series-Metric-Ab
+```
diff --git a/src/analysis/series-real-numbers.lagda.md b/src/analysis/series-real-numbers.lagda.md
new file mode 100644
index 0000000000..6b7455caa6
--- /dev/null
+++ b/src/analysis/series-real-numbers.lagda.md
@@ -0,0 +1,44 @@
+# Series in the real numbers
+
+```agda
+module analysis.series-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.series-complete-metric-abelian-groups
+open import analysis.series-metric-abelian-groups
+
+open import foundation.universe-levels
+
+open import lists.sequences
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.metric-additive-group-of-real-numbers
+```
+
+</details>
+
+## Idea
+
+A {{#concept "series" Disambiguation="of real numbers" Agda=series-ℝ}} in the
+[real numbers](real-numbers.dedekind-real-numbers.md) is a
+[series](analysis.series-metric-abelian-groups.md) in the
+[metric additive group of real numbers](real-numbers.metric-additive-group-of-real-numbers.md).
+
+## Definition
+
+```agda
+series-ℝ : (l : Level) → UU (lsuc l)
+series-ℝ l = series-Complete-Metric-Ab (complete-metric-ab-add-ℝ l)
+
+series-terms-ℝ : {l : Level} → sequence (ℝ l) → series-ℝ l
+series-terms-ℝ = series-terms-Metric-Ab
+
+term-series-ℝ : {l : Level} → series-ℝ l → sequence (ℝ l)
+term-series-ℝ = term-series-Metric-Ab
+
+partial-sum-series-ℝ : {l : Level} → series-ℝ l → sequence (ℝ l)
+partial-sum-series-ℝ {l} = partial-sum-series-Metric-Ab
+```
diff --git a/src/group-theory/abelian-groups.lagda.md b/src/group-theory/abelian-groups.lagda.md
index afd0152826..cd3e651b39 100644
--- a/src/group-theory/abelian-groups.lagda.md
+++ b/src/group-theory/abelian-groups.lagda.md
@@ -622,6 +622,52 @@ module _
   add-right-subtraction-Ab = mul-right-div-Group (group-Ab A)
 ```
 
+### `(-x) - (-y) = y - x`
+
+```agda
+module _
+  {l : Level} (A : Ab l)
+  where
+
+  abstract
+    right-subtraction-neg-Ab :
+      (x y : type-Ab A) →
+      right-subtraction-Ab A (neg-Ab A x) (neg-Ab A y) ＝
+      right-subtraction-Ab A y x
+    right-subtraction-neg-Ab x y =
+      equational-reasoning
+        right-subtraction-Ab A (neg-Ab A x) (neg-Ab A y)
+        ＝ add-Ab A (neg-Ab A x) y
+          by ap-add-Ab A refl (neg-neg-Ab A y)
+        ＝ right-subtraction-Ab A y x
+          by commutative-add-Ab A _ _
+```
+
+### `(x + y) - (x + z) = y - z`
+
+```agda
+module _
+  {l : Level} (A : Ab l)
+  where
+
+  abstract
+    right-subtraction-left-add-Ab :
+      (x y z : type-Ab A) →
+      right-subtraction-Ab A (add-Ab A x y) (add-Ab A x z) ＝
+      right-subtraction-Ab A y z
+    right-subtraction-left-add-Ab x y z =
+      equational-reasoning
+        right-subtraction-Ab A (add-Ab A x y) (add-Ab A x z)
+        ＝ add-Ab A (add-Ab A x y) (add-Ab A (neg-Ab A x) (neg-Ab A z))
+          by ap-add-Ab A refl (distributive-neg-add-Ab A x z)
+        ＝ add-Ab A (right-subtraction-Ab A x x) (right-subtraction-Ab A y z)
+          by interchange-add-add-Ab A _ _ _ _
+        ＝ add-Ab A (zero-Ab A) (right-subtraction-Ab A y z)
+          by ap-add-Ab A (right-inverse-law-add-Ab A x) refl
+        ＝ right-subtraction-Ab A y z
+          by left-unit-law-add-Ab A _
+```
+
 ### Conjugation is the identity function
 
 **Proof:** Consider two elements `x` and `y` of an abelian group. Then
diff --git a/src/linear-algebra/normed-real-vector-spaces.lagda.md b/src/linear-algebra/normed-real-vector-spaces.lagda.md
index de825ec122..c6d3cf3cb0 100644
--- a/src/linear-algebra/normed-real-vector-spaces.lagda.md
+++ b/src/linear-algebra/normed-real-vector-spaces.lagda.md
@@ -1,12 +1,15 @@
 # Normed real vector spaces
 
 ```agda
+{-# OPTIONS --lossy-unification #-}
+
 module linear-algebra.normed-real-vector-spaces where
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.logical-equivalences
@@ -22,9 +25,11 @@ 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.isometries-metric-spaces
 open import metric-spaces.located-metric-spaces
 open import metric-spaces.metric-spaces
 open import metric-spaces.metrics
+open import metric-spaces.metrics-of-metric-spaces
 
 open import real-numbers.absolute-value-real-numbers
 open import real-numbers.dedekind-real-numbers
@@ -93,6 +98,10 @@ module _
   vector-space-Normed-ℝ-Vector-Space : ℝ-Vector-Space l1 l2
   vector-space-Normed-ℝ-Vector-Space = pr1 V
 
+  ab-Normed-ℝ-Vector-Space : Ab l2
+  ab-Normed-ℝ-Vector-Space =
+    ab-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
+
   norm-Normed-ℝ-Vector-Space :
     norm-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
   norm-Normed-ℝ-Vector-Space = pr2 V
@@ -120,16 +129,65 @@ module _
   add-Normed-ℝ-Vector-Space =
     add-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
 
+  commutative-add-Normed-ℝ-Vector-Space :
+    (u v : type-Normed-ℝ-Vector-Space) →
+    add-Normed-ℝ-Vector-Space u v ＝ add-Normed-ℝ-Vector-Space v u
+  commutative-add-Normed-ℝ-Vector-Space =
+    commutative-add-Ab ab-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
 
+  neg-Normed-ℝ-Vector-Space :
+    type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space
+  neg-Normed-ℝ-Vector-Space =
+    neg-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
+
+  neg-neg-Normed-ℝ-Vector-Space :
+    (v : type-Normed-ℝ-Vector-Space) →
+    neg-Normed-ℝ-Vector-Space (neg-Normed-ℝ-Vector-Space v) ＝ v
+  neg-neg-Normed-ℝ-Vector-Space =
+    neg-neg-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
+
+  distributive-neg-add-Normed-ℝ-Vector-Space :
+    (v w : type-Normed-ℝ-Vector-Space) →
+    neg-Normed-ℝ-Vector-Space (add-Normed-ℝ-Vector-Space v w) ＝
+    add-Normed-ℝ-Vector-Space
+      ( neg-Normed-ℝ-Vector-Space v)
+      ( neg-Normed-ℝ-Vector-Space w)
+  distributive-neg-add-Normed-ℝ-Vector-Space =
+    distributive-neg-add-Ab ab-Normed-ℝ-Vector-Space
+
+  interchange-add-add-Normed-ℝ-Vector-Space :
+    (u v w x : type-Normed-ℝ-Vector-Space) →
+    add-Normed-ℝ-Vector-Space
+      ( add-Normed-ℝ-Vector-Space u v)
+      ( add-Normed-ℝ-Vector-Space w x) ＝
+    add-Normed-ℝ-Vector-Space
+      ( add-Normed-ℝ-Vector-Space u w)
+      ( add-Normed-ℝ-Vector-Space v x)
+  interchange-add-add-Normed-ℝ-Vector-Space =
+    interchange-add-add-Ab ab-Normed-ℝ-Vector-Space
+
   zero-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space
   zero-Normed-ℝ-Vector-Space =
     zero-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space
 
+  left-unit-law-add-Normed-ℝ-Vector-Space :
+    (v : type-Normed-ℝ-Vector-Space) →
+    add-Normed-ℝ-Vector-Space zero-Normed-ℝ-Vector-Space v ＝ v
+  left-unit-law-add-Normed-ℝ-Vector-Space =
+    left-unit-law-add-Ab ab-Normed-ℝ-Vector-Space
+
+  right-inverse-law-add-Normed-ℝ-Vector-Space :
+    (v : type-Normed-ℝ-Vector-Space) →
+    diff-Normed-ℝ-Vector-Space v v ＝ zero-Normed-ℝ-Vector-Space
+  right-inverse-law-add-Normed-ℝ-Vector-Space =
+    right-inverse-law-add-Ab ab-Normed-ℝ-Vector-Space
+
   map-norm-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space → ℝ l1
   map-norm-Normed-ℝ-Vector-Space = pr1 (pr1 norm-Normed-ℝ-Vector-Space)
 
@@ -149,20 +207,20 @@ module _
     nonnegative-dist-Seminormed-ℝ-Vector-Space
       ( seminormed-vector-space-Normed-ℝ-Vector-Space)
 
-  is-extensional-norm-Normed-ℝ-Metric-Space :
+  is-extensional-norm-Normed-ℝ-Vector-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-norm-Normed-ℝ-Vector-Space = pr2 norm-Normed-ℝ-Vector-Space
 
-  is-extensional-dist-Normed-ℝ-Metric-Space :
+  is-extensional-dist-Normed-ℝ-Vector-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 =
+  is-extensional-dist-Normed-ℝ-Vector-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
+      ( is-extensional-norm-Normed-ℝ-Vector-Space
         ( diff-Normed-ℝ-Vector-Space v w)
         ( |v-w|=0))
 
@@ -200,7 +258,7 @@ module _
       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
+        is-extensional-dist-Normed-ℝ-Vector-Space V v w
           ( eq-sim-ℝ
             ( transitive-sim-ℝ _ _ _
               ( sim-raise-ℝ l1 zero-ℝ)
@@ -241,6 +299,91 @@ abstract
       ( refl , λ d x y → inv-iff (neighborhood-iff-leq-dist-ℝ d x y))
 ```
 
+### Negation is an isometry in the metric space of a normed vector space
+
+```agda
+module _
+  {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2)
+  where
+
+  abstract
+    is-isometry-neg-Normed-ℝ-Vector-Space :
+      is-isometry-Metric-Space
+        ( metric-space-Normed-ℝ-Vector-Space V)
+        ( metric-space-Normed-ℝ-Vector-Space V)
+        ( neg-Normed-ℝ-Vector-Space V)
+    is-isometry-neg-Normed-ℝ-Vector-Space =
+      is-isometry-sim-metric-Metric-Space
+        ( metric-space-Normed-ℝ-Vector-Space V)
+        ( metric-space-Normed-ℝ-Vector-Space V)
+        ( nonnegative-dist-Normed-ℝ-Vector-Space V)
+        ( nonnegative-dist-Normed-ℝ-Vector-Space V)
+        ( is-metric-metric-space-Metric
+          ( set-Normed-ℝ-Vector-Space V)
+          ( metric-Normed-ℝ-Vector-Space V))
+        ( is-metric-metric-space-Metric
+          ( set-Normed-ℝ-Vector-Space V)
+          ( metric-Normed-ℝ-Vector-Space V))
+        ( neg-Normed-ℝ-Vector-Space V)
+        ( λ x y →
+          sim-eq-ℝ
+            ( inv
+              ( equational-reasoning
+                dist-Normed-ℝ-Vector-Space V
+                  ( neg-Normed-ℝ-Vector-Space V x)
+                  ( neg-Normed-ℝ-Vector-Space V y)
+                ＝ dist-Normed-ℝ-Vector-Space V y x
+                  by
+                    ap
+                      ( map-norm-Normed-ℝ-Vector-Space V)
+                      ( right-subtraction-neg-Ab
+                        ( ab-Normed-ℝ-Vector-Space V)
+                        ( _)
+                        ( _))
+                ＝ dist-Normed-ℝ-Vector-Space V x y
+                  by commutative-dist-Normed-ℝ-Vector-Space V y x)))
+```
+
+### Addition is an isometry in the metric space of a normed vector space
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : Normed-ℝ-Vector-Space l1 l2)
+  (u : type-Normed-ℝ-Vector-Space V)
+  where
+
+  abstract
+    is-isometry-left-add-Normed-ℝ-Vector-Space :
+      is-isometry-Metric-Space
+        ( metric-space-Normed-ℝ-Vector-Space V)
+        ( metric-space-Normed-ℝ-Vector-Space V)
+        ( add-Normed-ℝ-Vector-Space V u)
+    is-isometry-left-add-Normed-ℝ-Vector-Space =
+      is-isometry-sim-metric-Metric-Space
+        ( metric-space-Normed-ℝ-Vector-Space V)
+        ( metric-space-Normed-ℝ-Vector-Space V)
+        ( nonnegative-dist-Normed-ℝ-Vector-Space V)
+        ( nonnegative-dist-Normed-ℝ-Vector-Space V)
+        ( is-metric-metric-space-Metric
+          ( set-Normed-ℝ-Vector-Space V)
+          ( metric-Normed-ℝ-Vector-Space V))
+        ( is-metric-metric-space-Metric
+          ( set-Normed-ℝ-Vector-Space V)
+          ( metric-Normed-ℝ-Vector-Space V))
+        ( add-Normed-ℝ-Vector-Space V u)
+        ( λ v w →
+          sim-eq-ℝ
+            ( ap
+              ( map-norm-Normed-ℝ-Vector-Space V)
+              ( inv
+                ( right-subtraction-left-add-Ab
+                  ( ab-Normed-ℝ-Vector-Space V)
+                  ( u)
+                  ( v)
+                  ( w)))))
+```
+
 ## See also
 
 - [Real Banach spaces](linear-algebra.real-banach-spaces.md), normed real vector
diff --git a/src/linear-algebra/real-banach-spaces.lagda.md b/src/linear-algebra/real-banach-spaces.lagda.md
index 1ed7c36a32..bdcc30ac25 100644
--- a/src/linear-algebra/real-banach-spaces.lagda.md
+++ b/src/linear-algebra/real-banach-spaces.lagda.md
@@ -17,9 +17,16 @@ open import foundation.universe-levels
 
 open import linear-algebra.normed-real-vector-spaces
 
+open import lists.sequences
+
+open import metric-spaces.cauchy-sequences-complete-metric-spaces
+open import metric-spaces.cauchy-sequences-metric-spaces
 open import metric-spaces.complete-metric-spaces
+open import metric-spaces.limits-of-sequences-metric-spaces
+open import metric-spaces.metric-spaces
 
 open import real-numbers.cauchy-completeness-dedekind-real-numbers
+open import real-numbers.dedekind-real-numbers
 ```
 
 </details>
@@ -49,6 +56,59 @@ is-banach-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})
+
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  where
+
+  normed-vector-space-ℝ-Banach-Space : Normed-ℝ-Vector-Space l1 l2
+  normed-vector-space-ℝ-Banach-Space = pr1 V
+
+  metric-space-ℝ-Banach-Space : Metric-Space l2 l1
+  metric-space-ℝ-Banach-Space =
+    metric-space-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space
+
+  is-complete-metric-space-ℝ-Banach-Space :
+    is-complete-Metric-Space metric-space-ℝ-Banach-Space
+  is-complete-metric-space-ℝ-Banach-Space = pr2 V
+
+  complete-metric-space-ℝ-Banach-Space : Complete-Metric-Space l2 l1
+  complete-metric-space-ℝ-Banach-Space =
+    ( metric-space-ℝ-Banach-Space , is-complete-metric-space-ℝ-Banach-Space)
+
+  type-ℝ-Banach-Space : UU l2
+  type-ℝ-Banach-Space =
+    type-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space
+
+  map-norm-ℝ-Banach-Space : type-ℝ-Banach-Space → ℝ l1
+  map-norm-ℝ-Banach-Space =
+    map-norm-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space
+
+  cauchy-sequence-ℝ-Banach-Space : UU (l1 ⊔ l2)
+  cauchy-sequence-ℝ-Banach-Space =
+    cauchy-sequence-Metric-Space metric-space-ℝ-Banach-Space
+
+  is-cauchy-sequence-ℝ-Banach-Space :
+    sequence type-ℝ-Banach-Space → UU l1
+  is-cauchy-sequence-ℝ-Banach-Space =
+    is-cauchy-sequence-Metric-Space metric-space-ℝ-Banach-Space
+
+  map-cauchy-sequence-ℝ-Banach-Space :
+    cauchy-sequence-ℝ-Banach-Space → sequence type-ℝ-Banach-Space
+  map-cauchy-sequence-ℝ-Banach-Space = pr1
+
+  has-limit-sequence-ℝ-Banach-Space :
+    sequence type-ℝ-Banach-Space → UU (l1 ⊔ l2)
+  has-limit-sequence-ℝ-Banach-Space =
+    has-limit-sequence-Metric-Space metric-space-ℝ-Banach-Space
+
+  has-limit-cauchy-sequence-ℝ-Banach-Space :
+    (σ : cauchy-sequence-ℝ-Banach-Space) →
+    has-limit-sequence-ℝ-Banach-Space (map-cauchy-sequence-ℝ-Banach-Space σ)
+  has-limit-cauchy-sequence-ℝ-Banach-Space =
+    has-limit-cauchy-sequence-Complete-Metric-Space
+      ( complete-metric-space-ℝ-Banach-Space)
 ```
 
 ## Properties
diff --git a/src/metric-spaces/metrics-of-metric-spaces.lagda.md b/src/metric-spaces/metrics-of-metric-spaces.lagda.md
index a918f42c78..f3b1b5bcff 100644
--- a/src/metric-spaces/metrics-of-metric-spaces.lagda.md
+++ b/src/metric-spaces/metrics-of-metric-spaces.lagda.md
@@ -21,13 +21,17 @@ open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import metric-spaces.equality-of-metric-spaces
+open import metric-spaces.functions-metric-spaces
+open import metric-spaces.isometries-metric-spaces
 open import metric-spaces.located-metric-spaces
 open import metric-spaces.metric-spaces
 open import metric-spaces.metrics
+open import metric-spaces.short-functions-metric-spaces
 
 open import real-numbers.addition-nonnegative-real-numbers
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.inequality-nonnegative-real-numbers
+open import real-numbers.inequality-real-numbers
 open import real-numbers.nonnegative-real-numbers
 open import real-numbers.rational-real-numbers
 open import real-numbers.saturation-inequality-nonnegative-real-numbers
@@ -266,6 +270,109 @@ module _
         ( isometric-equiv-metric-is-metric-of-Metric-Space M ρ is-metric-M-ρ)
 ```
 
+### If `M` and `N` are metric spaces with metrics `dM` and `dN`, a function `f : M → N` is an isometry if and only if `dM x y` is similar to `dN (f x) (f y)` for all `x, y : M`
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  (M : Metric-Space l1 l2)
+  (N : Metric-Space l3 l4)
+  (dM : distance-function l5 (set-Metric-Space M))
+  (dN : distance-function l6 (set-Metric-Space N))
+  (is-metric-dM : is-metric-of-Metric-Space M dM)
+  (is-metric-dN : is-metric-of-Metric-Space N dN)
+  (f : type-function-Metric-Space M N)
+  where
+
+  abstract
+    is-isometry-sim-metric-Metric-Space :
+      ((x y : type-Metric-Space M) → sim-ℝ⁰⁺ (dM x y) (dN (f x) (f y))) →
+      is-isometry-Metric-Space M N f
+    is-isometry-sim-metric-Metric-Space H d x y =
+      logical-equivalence-reasoning
+        neighborhood-Metric-Space M d x y
+        ↔ leq-ℝ (real-ℝ⁰⁺ (dM x y)) (real-ℚ⁺ d)
+          by is-metric-dM d x y
+        ↔ leq-ℝ (real-ℝ⁰⁺ (dN (f x) (f y))) (real-ℚ⁺ d)
+          by leq-iff-left-sim-ℝ (H x y)
+        ↔ neighborhood-Metric-Space N d (f x) (f y)
+          by inv-iff (is-metric-dN d (f x) (f y))
+
+    sim-metric-is-isometry-Metric-Space :
+      is-isometry-Metric-Space M N f →
+      (x y : type-Metric-Space M) →
+      sim-ℝ⁰⁺ (dM x y) (dN (f x) (f y))
+    sim-metric-is-isometry-Metric-Space H x y =
+      sim-leq-same-positive-rational-ℝ⁰⁺
+        ( dM x y)
+        ( dN (f x) (f y))
+        ( λ d →
+          logical-equivalence-reasoning
+            leq-ℝ (real-ℝ⁰⁺ (dM x y)) (real-ℚ⁺ d)
+            ↔ neighborhood-Metric-Space M d x y
+              by inv-iff (is-metric-dM d x y)
+            ↔ neighborhood-Metric-Space N d (f x) (f y)
+              by H d x y
+            ↔ leq-ℝ (real-ℝ⁰⁺ (dN (f x) (f y))) (real-ℚ⁺ d)
+              by is-metric-dN d (f x) (f y))
+
+  is-isometry-iff-sim-metric-Metric-Space :
+    is-isometry-Metric-Space M N f ↔
+    ((x y : type-Metric-Space M) → sim-ℝ⁰⁺ (dM x y) (dN (f x) (f y)))
+  is-isometry-iff-sim-metric-Metric-Space =
+    ( sim-metric-is-isometry-Metric-Space ,
+      is-isometry-sim-metric-Metric-Space)
+```
+
+### If `M` and `N` are metric spaces with metrics `dM` and `dN`, a function `f : M → N` is short if and only if `dN (f x) (f y) ≤ dM x y` for all `x, y : M`
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  (M : Metric-Space l1 l2)
+  (N : Metric-Space l3 l4)
+  (dM : distance-function l5 (set-Metric-Space M))
+  (dN : distance-function l6 (set-Metric-Space N))
+  (is-metric-dM : is-metric-of-Metric-Space M dM)
+  (is-metric-dN : is-metric-of-Metric-Space N dN)
+  (f : type-function-Metric-Space M N)
+  where
+
+  abstract
+    is-short-function-leq-metric-Metric-Space :
+      ((x y : type-Metric-Space M) → leq-ℝ⁰⁺ (dN (f x) (f y)) (dM x y)) →
+      is-short-function-Metric-Space M N f
+    is-short-function-leq-metric-Metric-Space H d x y Ndxy =
+      backward-implication
+        ( is-metric-dN d (f x) (f y))
+        ( transitive-leq-ℝ
+          ( real-ℝ⁰⁺ (dN (f x) (f y)))
+          ( real-ℝ⁰⁺ (dM x y))
+          ( real-ℚ⁺ d)
+          ( forward-implication (is-metric-dM d x y) Ndxy)
+          ( H x y))
+
+    leq-metric-is-short-function-Metric-Space :
+      is-short-function-Metric-Space M N f →
+      (x y : type-Metric-Space M) →
+      leq-ℝ⁰⁺ (dN (f x) (f y)) (dM x y)
+    leq-metric-is-short-function-Metric-Space H x y =
+      leq-leq-positive-rational-ℝ⁰⁺
+        ( dN (f x) (f y))
+        ( dM x y)
+        ( λ d dMxy≤d →
+          forward-implication
+            ( is-metric-dN d (f x) (f y))
+            ( H d x y (backward-implication (is-metric-dM d x y) dMxy≤d)))
+
+  is-short-function-iff-leq-metric-Metric-Space :
+    is-short-function-Metric-Space M N f ↔
+    ((x y : type-Metric-Space M) → leq-ℝ⁰⁺ (dN (f x) (f y)) (dM x y))
+  is-short-function-iff-leq-metric-Metric-Space =
+    ( leq-metric-is-short-function-Metric-Space ,
+      is-short-function-leq-metric-Metric-Space)
+```
+
 ## See also
 
 - [Metrics of metric spaces are uniformly continuous](metric-spaces.metrics-of-metric-spaces-are-uniformly-continuous.md)
diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md
index 9fb6e1249d..3ad9872822 100644
--- a/src/real-numbers.lagda.md
+++ b/src/real-numbers.lagda.md
@@ -22,7 +22,6 @@ open import real-numbers.binary-minimum-real-numbers public
 open import real-numbers.cauchy-completeness-dedekind-real-numbers public
 open import real-numbers.cauchy-sequences-real-numbers public
 open import real-numbers.closed-intervals-real-numbers public
-open import real-numbers.convergent-series-real-numbers public
 open import real-numbers.dedekind-real-numbers public
 open import real-numbers.difference-real-numbers public
 open import real-numbers.distance-real-numbers public
@@ -59,7 +58,7 @@ open import real-numbers.maximum-finite-families-real-numbers public
 open import real-numbers.maximum-inhabited-finitely-enumerable-subsets-real-numbers public
 open import real-numbers.maximum-lower-dedekind-real-numbers public
 open import real-numbers.maximum-upper-dedekind-real-numbers public
-open import real-numbers.metric-abelian-group-of-real-numbers public
+open import real-numbers.metric-additive-group-of-real-numbers public
 open import real-numbers.metric-space-of-nonnegative-real-numbers public
 open import real-numbers.metric-space-of-real-numbers public
 open import real-numbers.minimum-finite-families-real-numbers public
@@ -93,7 +92,6 @@ open import real-numbers.real-numbers-from-upper-dedekind-real-numbers public
 open import real-numbers.real-sequences-approximating-zero public
 open import real-numbers.saturation-inequality-nonnegative-real-numbers public
 open import real-numbers.saturation-inequality-real-numbers public
-open import real-numbers.series-real-numbers public
 open import real-numbers.short-function-binary-maximum-real-numbers public
 open import real-numbers.short-function-binary-minimum-real-numbers public
 open import real-numbers.similarity-nonnegative-real-numbers public
diff --git a/src/real-numbers/cauchy-sequences-real-numbers.lagda.md b/src/real-numbers/cauchy-sequences-real-numbers.lagda.md
index 6876201386..a7d81021a9 100644
--- a/src/real-numbers/cauchy-sequences-real-numbers.lagda.md
+++ b/src/real-numbers/cauchy-sequences-real-numbers.lagda.md
@@ -11,6 +11,8 @@ module real-numbers.cauchy-sequences-real-numbers where
 ```agda
 open import foundation.universe-levels
 
+open import lists.sequences
+
 open import metric-spaces.cartesian-products-metric-spaces
 open import metric-spaces.cauchy-sequences-complete-metric-spaces
 open import metric-spaces.cauchy-sequences-metric-spaces
@@ -39,6 +41,9 @@ is a [Cauchy sequence](metric-spaces.cauchy-sequences-metric-spaces.md) in the
 ## Definition
 
 ```agda
+is-cauchy-sequence-ℝ : {l : Level} → sequence (ℝ l) → UU l
+is-cauchy-sequence-ℝ {l} = is-cauchy-sequence-Metric-Space (metric-space-ℝ l)
+
 cauchy-sequence-ℝ : (l : Level) → UU (lsuc l)
 cauchy-sequence-ℝ l = cauchy-sequence-Metric-Space (metric-space-ℝ l)
 ```
diff --git a/src/real-numbers/convergent-series-real-numbers.lagda.md b/src/real-numbers/convergent-series-real-numbers.lagda.md
deleted file mode 100644
index 9c8b3bd2db..0000000000
--- a/src/real-numbers/convergent-series-real-numbers.lagda.md
+++ /dev/null
@@ -1,40 +0,0 @@
-# Convergent series of real numbers
-
-```agda
-{-# OPTIONS --lossy-unification #-}
-
-module real-numbers.convergent-series-real-numbers where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import analysis.convergent-series-metric-abelian-groups
-
-open import foundation.propositions
-open import foundation.universe-levels
-
-open import real-numbers.dedekind-real-numbers
-open import real-numbers.series-real-numbers
-```
-
-</details>
-
-## Idea
-
-A [series](real-numbers.series-real-numbers.md) of
-[real numbers](real-numbers.dedekind-real-numbers.md)
-{{#concept "converges" Disambiguation="series of real numbers" Agda=is-sum-series-ℝ}}
-to `x` if the sequence of its partial sums
-[converges](metric-spaces.limits-of-sequences-metric-spaces.md) to `x` in the
-[standard metric space of real numbers](real-numbers.metric-space-of-real-numbers.md).
-
-## Definition
-
-```agda
-is-sum-prop-series-ℝ : {l : Level} → series-ℝ l → ℝ l → Prop l
-is-sum-prop-series-ℝ = is-sum-prop-series-Metric-Ab
-
-is-sum-series-ℝ : {l : Level} → series-ℝ l → ℝ l → UU l
-is-sum-series-ℝ = is-sum-series-Metric-Ab
-```
diff --git a/src/real-numbers/geometric-sequences-real-numbers.lagda.md b/src/real-numbers/geometric-sequences-real-numbers.lagda.md
index a868836657..f5625e7f4e 100644
--- a/src/real-numbers/geometric-sequences-real-numbers.lagda.md
+++ b/src/real-numbers/geometric-sequences-real-numbers.lagda.md
@@ -9,6 +9,9 @@ module real-numbers.geometric-sequences-real-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import analysis.convergent-series-real-numbers
+open import analysis.series-real-numbers
+
 open import commutative-algebra.geometric-sequences-commutative-rings
 
 open import elementary-number-theory.natural-numbers
@@ -27,7 +30,6 @@ open import metric-spaces.uniformly-continuous-functions-metric-spaces
 
 open import real-numbers.absolute-value-real-numbers
 open import real-numbers.apartness-real-numbers
-open import real-numbers.convergent-series-real-numbers
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.difference-real-numbers
 open import real-numbers.isometry-difference-real-numbers
@@ -41,7 +43,6 @@ open import real-numbers.nonzero-real-numbers
 open import real-numbers.powers-real-numbers
 open import real-numbers.raising-universe-levels-real-numbers
 open import real-numbers.rational-real-numbers
-open import real-numbers.series-real-numbers
 open import real-numbers.similarity-real-numbers
 open import real-numbers.strict-inequality-real-numbers
 open import real-numbers.uniformly-continuous-functions-real-numbers
diff --git a/src/real-numbers/inequality-real-numbers.lagda.md b/src/real-numbers/inequality-real-numbers.lagda.md
index 1d9d46febf..d44ee49da3 100644
--- a/src/real-numbers/inequality-real-numbers.lagda.md
+++ b/src/real-numbers/inequality-real-numbers.lagda.md
@@ -328,6 +328,21 @@ module _
     preserves-leq-right-sim-ℝ : leq-ℝ z x → leq-ℝ z y
     preserves-leq-right-sim-ℝ z≤x q q<z = pr1 x~y q (z≤x q q<z)
 
+module _
+  {l1 l2 l3 : Level} {z : ℝ l1} {x : ℝ l2} {y : ℝ l3} (x~y : sim-ℝ x y)
+  where
+
+  abstract
+    leq-iff-left-sim-ℝ : leq-ℝ x z ↔ leq-ℝ y z
+    leq-iff-left-sim-ℝ =
+      ( preserves-leq-left-sim-ℝ x~y ,
+        preserves-leq-left-sim-ℝ (symmetric-sim-ℝ x~y))
+
+    leq-iff-right-sim-ℝ : leq-ℝ z x ↔ leq-ℝ z y
+    leq-iff-right-sim-ℝ =
+      ( preserves-leq-right-sim-ℝ x~y ,
+        preserves-leq-right-sim-ℝ (symmetric-sim-ℝ x~y))
+
 module _
   {l1 l2 l3 l4 : Level}
   {x1 : ℝ l1} {x2 : ℝ l2} {y1 : ℝ l3} {y2 : ℝ l4}
diff --git a/src/real-numbers/metric-abelian-group-of-real-numbers.lagda.md b/src/real-numbers/metric-additive-group-of-real-numbers.lagda.md
similarity index 71%
rename from src/real-numbers/metric-abelian-group-of-real-numbers.lagda.md
rename to src/real-numbers/metric-additive-group-of-real-numbers.lagda.md
index 3402489495..db74d26fd0 100644
--- a/src/real-numbers/metric-abelian-group-of-real-numbers.lagda.md
+++ b/src/real-numbers/metric-additive-group-of-real-numbers.lagda.md
@@ -3,12 +3,13 @@
 ```agda
 {-# OPTIONS --lossy-unification #-}
 
-module real-numbers.metric-abelian-group-of-real-numbers where
+module real-numbers.metric-additive-group-of-real-numbers where
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
+open import analysis.complete-metric-abelian-groups
 open import analysis.metric-abelian-groups
 
 open import foundation.dependent-pair-types
@@ -16,6 +17,7 @@ open import foundation.universe-levels
 
 open import metric-spaces.pseudometric-spaces
 
+open import real-numbers.cauchy-completeness-dedekind-real-numbers
 open import real-numbers.isometry-addition-real-numbers
 open import real-numbers.isometry-negation-real-numbers
 open import real-numbers.large-additive-group-of-real-numbers
@@ -34,11 +36,16 @@ The [Dedekind real numbers](real-numbers.dedekind-real-numbers.md) form a
 ## Definition
 
 ```agda
-metric-ab-ℝ : (l : Level) → Metric-Ab (lsuc l) l
-metric-ab-ℝ l =
+metric-ab-add-ℝ : (l : Level) → Metric-Ab (lsuc l) l
+metric-ab-add-ℝ l =
   ( ab-add-ℝ l ,
     structure-Pseudometric-Space (pseudometric-space-ℝ l) ,
     is-extensional-pseudometric-space-ℝ ,
     is-isometry-neg-ℝ ,
     is-isometry-left-add-ℝ)
+
+complete-metric-ab-add-ℝ : (l : Level) → Complete-Metric-Ab (lsuc l) l
+complete-metric-ab-add-ℝ l =
+  ( metric-ab-add-ℝ l ,
+    is-complete-metric-space-ℝ l)
 ```
diff --git a/src/real-numbers/series-real-numbers.lagda.md b/src/real-numbers/series-real-numbers.lagda.md
deleted file mode 100644
index f3d0ecf21e..0000000000
--- a/src/real-numbers/series-real-numbers.lagda.md
+++ /dev/null
@@ -1,42 +0,0 @@
-# Series of real numbers
-
-```agda
-{-# OPTIONS --lossy-unification #-}
-
-module real-numbers.series-real-numbers where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import analysis.series-metric-abelian-groups
-
-open import foundation.universe-levels
-
-open import lists.sequences
-
-open import real-numbers.dedekind-real-numbers
-open import real-numbers.metric-abelian-group-of-real-numbers
-```
-
-</details>
-
-## Idea
-
-A {{#concept "series" Disambiguation="of real numbers" Agda=series-ℝ}} of
-[real numbers](real-numbers.dedekind-real-numbers.md) is an infinite sum
-$$∑_{n=0}^∞ a_n$$, which is evaluated for convergence in the
-[metric abelian group of real numbers](real-numbers.metric-abelian-group-of-real-numbers.md).
-
-## Definition
-
-```agda
-series-ℝ : (l : Level) → UU (lsuc l)
-series-ℝ l = series-Metric-Ab (metric-ab-ℝ l)
-
-series-terms-ℝ : {l : Level} → sequence (ℝ l) → series-ℝ l
-series-terms-ℝ = series-terms-Metric-Ab
-
-terms-series-ℝ : {l : Level} → series-ℝ l → sequence (ℝ l)
-terms-series-ℝ = term-series-Metric-Ab
-```