diff --git a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda
index 0ba8d9539c..6448881947 100644
--- a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda
+++ b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda
@@ -12,7 +12,7 @@ open import Codata.Guarded.Stream as Stream using (Stream; head; tail)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Function.Base using (_∘_; _on_)
 open import Level using (Level; _⊔_)
-open import Relation.Binary.Core using (REL; _⇒_)
+open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions
   using (Reflexive; Sym; Trans; Antisym; Symmetric; Transitive)
@@ -104,6 +104,43 @@ drop⁺ : ∀ n → Pointwise R ⇒ (Pointwise R on Stream.drop n)
 drop⁺ zero    as≈bs = as≈bs
 drop⁺ (suc n) as≈bs = drop⁺ n (as≈bs .tail)
 
+------------------------------------------------------------------------
+-- Algebraic properties
+
+module _ {A : Set a} {_≈_ : Rel A ℓ} where
+
+  open import Algebra.Definitions
+
+  private
+    variable
+      _∙_ : A → A → A
+      _⁻¹ : A → A
+      ε : A
+
+  assoc : Associative _≈_ _∙_ → Associative (Pointwise _≈_) (Stream.zipWith _∙_)
+  head (assoc assoc₁ xs ys zs) = assoc₁ (head xs) (head ys) (head zs)
+  tail (assoc assoc₁ xs ys zs) = assoc assoc₁ (tail xs) (tail ys) (tail zs)
+
+  comm : Commutative _≈_ _∙_ → Commutative (Pointwise _≈_) (Stream.zipWith _∙_)
+  head (comm comm₁ xs ys) = comm₁ (head xs) (head ys)
+  tail (comm comm₁ xs ys) = comm comm₁ (tail xs) (tail ys)
+
+  identityˡ : LeftIdentity _≈_ ε _∙_ → LeftIdentity (Pointwise _≈_) (Stream.repeat ε) (Stream.zipWith _∙_)
+  head (identityˡ identityˡ₁ xs) = identityˡ₁ (head xs)
+  tail (identityˡ identityˡ₁ xs) = identityˡ identityˡ₁ (tail xs)
+
+  identityʳ : RightIdentity _≈_ ε _∙_ → RightIdentity (Pointwise _≈_) (Stream.repeat ε) (Stream.zipWith _∙_)
+  head (identityʳ identityʳ₁ xs) = identityʳ₁ (head xs)
+  tail (identityʳ identityʳ₁ xs) = identityʳ identityʳ₁ (tail xs)
+
+  inverseˡ : LeftInverse _≈_ ε _⁻¹ _∙_ → LeftInverse (Pointwise _≈_) (Stream.repeat ε) (Stream.map _⁻¹) (Stream.zipWith _∙_)
+  head (inverseˡ inverseˡ₁ xs) = inverseˡ₁ (head xs)
+  tail (inverseˡ inverseˡ₁ xs) = inverseˡ inverseˡ₁ (tail xs)
+
+  inverseʳ : RightInverse _≈_ ε _⁻¹ _∙_ → RightInverse (Pointwise _≈_) (Stream.repeat ε) (Stream.map _⁻¹) (Stream.zipWith _∙_)
+  head (inverseʳ inverseʳ₁ xs) = inverseʳ₁ (head xs)
+  tail (inverseʳ inverseʳ₁ xs) = inverseʳ inverseʳ₁ (tail xs)
+
 ------------------------------------------------------------------------
 -- Pointwise Equality as a Bisimilarity
 
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index fb186be08d..dae045f50a 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -49,6 +49,7 @@ open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′; _⊎_)
 import Data.Sign.Base as Sign
 open import Function.Base using (_∘_; _∘′_; _∘₂_; _$_; flip)
 open import Function.Definitions using (Injective)
+open import Function.Metric.Rational as Metric hiding (Symmetric)
 open import Level using (0ℓ)
 open import Relation.Binary
 open import Relation.Binary.Morphism.Structures
@@ -1012,6 +1013,12 @@ neg-distrib-+ = +-Monomorphism.⁻¹-distrib-∙ ℚᵘ.+-0-isAbelianGroup (ℚ
 +-monoʳ-≤ : ∀ r → (_+_ r) Preserves _≤_ ⟶ _≤_
 +-monoʳ-≤ r p≤q = +-mono-≤ (≤-refl {r}) p≤q
 
+nonNeg+nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p + q)
+nonNeg+nonNeg⇒nonNeg p q = nonNegative $ +-mono-≤ (nonNegative⁻¹ p) (nonNegative⁻¹ q)
+
+nonPos+nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonPositive (p + q)
+nonPos+nonPos⇒nonPos p q = nonPositive $ +-mono-≤ (nonPositive⁻¹ p) (nonPositive⁻¹ q)
+
 ------------------------------------------------------------------------
 -- Properties of _+_ and _<_
 
@@ -1035,6 +1042,24 @@ neg-distrib-+ = +-Monomorphism.⁻¹-distrib-∙ ℚᵘ.+-0-isAbelianGroup (ℚ
 +-monoʳ-< : ∀ r → (_+_ r) Preserves _<_ ⟶ _<_
 +-monoʳ-< r p<q = +-mono-≤-< (≤-refl {r}) p<q
 
+pos+nonNeg⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : NonNegative q}} → Positive (p + q)
+pos+nonNeg⇒pos p q = positive $ +-mono-<-≤ (positive⁻¹ p) (nonNegative⁻¹ q)
+
+nonNeg+pos⇒pos : ∀ p .{{_ : NonNegative p}} q .{{_ : Positive q}} → Positive (p + q)
+nonNeg+pos⇒pos p q = positive $ +-mono-≤-< (nonNegative⁻¹ p) (positive⁻¹ q)
+
+pos+pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p + q)
+pos+pos⇒pos p q = positive $ +-mono-< (positive⁻¹ p) (positive⁻¹ q)
+
+neg+nonPos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : NonPositive q}} → Negative (p + q)
+neg+nonPos⇒neg p q = negative $ +-mono-<-≤ (negative⁻¹ p) (nonPositive⁻¹ q)
+
+nonPos+neg⇒neg : ∀ p .{{_ : NonPositive p}} q .{{_ : Negative q}} → Negative (p + q)
+nonPos+neg⇒neg p q = negative $ +-mono-≤-< (nonPositive⁻¹ p) (negative⁻¹ q)
+
+neg+neg⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Negative (p + q)
+neg+neg⇒neg p q = negative $ +-mono-< (negative⁻¹ p) (negative⁻¹ q)
+
 ------------------------------------------------------------------------
 -- Properties of _*_
 ------------------------------------------------------------------------
@@ -1340,6 +1365,34 @@ module _ where
 *-cancelˡ-≤-neg : ∀ r .{{_ : Negative r}} → r * p ≤ r * q → p ≥ q
 *-cancelˡ-≤-neg {p} {q} r rewrite *-comm r p | *-comm r q = *-cancelʳ-≤-neg r
 
+nonNeg*nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p * q)
+nonNeg*nonNeg⇒nonNeg p q = nonNegative $ begin
+  0ℚ     ≡⟨ *-zeroʳ p ⟨
+  p * 0ℚ ≤⟨ *-monoˡ-≤-nonNeg p (nonNegative⁻¹ q) ⟩
+  p * q  ∎
+  where open ≤-Reasoning
+
+nonNeg*nonPos⇒nonPos : ∀ p .{{_ : NonNegative p}} q .{{_ : NonPositive q}} → NonPositive (p * q)
+nonNeg*nonPos⇒nonPos p q = nonPositive $ begin
+  p * q  ≤⟨ *-monoˡ-≤-nonNeg p (nonPositive⁻¹ q) ⟩
+  p * 0ℚ ≡⟨ *-zeroʳ p ⟩
+  0ℚ     ∎
+  where open ≤-Reasoning
+
+nonPos*nonNeg⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonNegative q}} → NonPositive (p * q)
+nonPos*nonNeg⇒nonPos p q = nonPositive $ begin
+  p * q  ≤⟨ *-monoˡ-≤-nonPos p (nonNegative⁻¹ q) ⟩
+  p * 0ℚ ≡⟨ *-zeroʳ p ⟩
+  0ℚ     ∎
+  where open ≤-Reasoning
+
+nonPos*nonPos⇒nonNeg : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonNegative (p * q)
+nonPos*nonPos⇒nonNeg p q = nonNegative $ begin
+  0ℚ     ≡⟨ *-zeroʳ p ⟨
+  p * 0ℚ ≤⟨ *-monoˡ-≤-nonPos p (nonPositive⁻¹ q) ⟩
+  p * q  ∎
+  where open ≤-Reasoning
+
 ------------------------------------------------------------------------
 -- Properties of _*_ and _<_
 
@@ -1387,6 +1440,34 @@ module _ where
 *-cancelʳ-<-nonPos : ∀ r .{{_ : NonPositive r}} → p * r < q * r → p > q
 *-cancelʳ-<-nonPos {p} {q} r rewrite *-comm p r | *-comm q r = *-cancelˡ-<-nonPos r
 
+pos*pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p * q)
+pos*pos⇒pos p q = positive $ begin-strict
+  0ℚ     ≡⟨ *-zeroʳ p ⟨
+  p * 0ℚ <⟨ *-monoʳ-<-pos p (positive⁻¹ q) ⟩
+  p * q  ∎
+  where open ≤-Reasoning
+
+pos*neg⇒neg : ∀ p .{{_ : Positive p}} q .{{_ : Negative q}} → Negative (p * q)
+pos*neg⇒neg p q = negative $ begin-strict
+  p * q  <⟨ *-monoʳ-<-pos p (negative⁻¹ q) ⟩
+  p * 0ℚ ≡⟨ *-zeroʳ p ⟩
+  0ℚ     ∎
+  where open ≤-Reasoning
+
+neg*pos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Positive q}} → Negative (p * q)
+neg*pos⇒neg p q = negative $ begin-strict
+  p * q  <⟨ *-monoʳ-<-neg p (positive⁻¹ q) ⟩
+  p * 0ℚ ≡⟨ *-zeroʳ p ⟩
+  0ℚ     ∎
+  where open ≤-Reasoning
+
+neg*neg⇒pos : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Positive (p * q)
+neg*neg⇒pos p q = positive $ begin-strict
+  0ℚ     ≡⟨ *-zeroʳ p ⟨
+  p * 0ℚ <⟨ *-monoʳ-<-neg p (negative⁻¹ q) ⟩
+  p * q  ∎
+  where open ≤-Reasoning
+
 ------------------------------------------------------------------------
 -- Properties of _⊓_
 ------------------------------------------------------------------------
@@ -1719,6 +1800,89 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl
 ∣∣p∣∣≡∣p∣ : ∀ p → ∣ ∣ p ∣ ∣ ≡ ∣ p ∣
 ∣∣p∣∣≡∣p∣ p = 0≤p⇒∣p∣≡p (0≤∣p∣ p)
 
+------------------------------------------------------------------------
+-- Metric space
+------------------------------------------------------------------------
+
+private
+  d : ℚ → ℚ → ℚ
+  d p q = ∣ p - q ∣
+
+d-cong : Congruent _≡_ d
+d-cong = cong₂ _
+
+d-nonNegative : ∀ {p q} → 0ℚ ≤ d p q
+d-nonNegative {p} {q} = nonNegative⁻¹ _ {{∣-∣-nonNeg (p - q)}}
+
+d-definite : Definite _≡_ d
+d-definite {p} refl = cong ∣_∣ (+-inverseʳ p)
+
+d-indiscernable : Indiscernable _≡_ d
+d-indiscernable {p} {q} ∣p-q∣≡0 = begin
+  p               ≡⟨ +-identityʳ p ⟨
+  p - 0ℚ          ≡⟨ cong (_-_ p) (∣p∣≡0⇒p≡0 (p - q) ∣p-q∣≡0) ⟨
+  p - (p - q)     ≡⟨ cong (_+_ p) (neg-distrib-+ p (- q)) ⟩
+  p + (- p - - q) ≡⟨ +-assoc p (- p) (- - q) ⟨
+  (p - p) - - q   ≡⟨ cong₂ _+_ (+-inverseʳ p) (⁻¹-involutive q) ⟩
+  0ℚ + q          ≡⟨ +-identityˡ q ⟩
+  q               ∎
+  where
+    open ≡-Reasoning
+    open GroupProperties +-0-group
+
+d-sym : Metric.Symmetric d
+d-sym p q = begin
+  ∣ p - q ∣     ≡˘⟨ ∣-p∣≡∣p∣ (p - q) ⟩
+  ∣ - (p - q) ∣ ≡⟨ cong ∣_∣ (⁻¹-anti-homo-// p q) ⟩
+  ∣ q - p ∣     ∎
+  where
+    open ≡-Reasoning
+    open GroupProperties +-0-group
+
+d-triangle : TriangleInequality d
+d-triangle p q r = begin
+  ∣ p - r ∣             ≡⟨ cong (λ # → ∣ # - r ∣) (+-identityʳ p) ⟨
+  ∣ p + 0ℚ - r ∣        ≡⟨ cong (λ # → ∣ p + # - r ∣) (+-inverseˡ q) ⟨
+  ∣ p + (- q + q) - r ∣ ≡⟨ cong (λ # → ∣ # - r ∣) (+-assoc p (- q) q) ⟨
+  ∣ ((p - q) + q) - r ∣ ≡⟨ cong ∣_∣ (+-assoc (p - q) q (- r)) ⟩
+  ∣ (p - q) + (q - r) ∣ ≤⟨ ∣p+q∣≤∣p∣+∣q∣ (p - q) (q - r) ⟩
+  ∣ p - q ∣ + ∣ q - r ∣ ∎
+  where open ≤-Reasoning
+
+d-isProtoMetric : IsProtoMetric _≡_ d
+d-isProtoMetric = record
+  { isPartialOrder = ≤-isPartialOrder
+  ; ≈-isEquivalence = isEquivalence
+  ; cong = cong₂ _
+  ; nonNegative = λ {p q} → d-nonNegative {p} {q}
+  }
+
+d-isPreMetric : IsPreMetric _≡_ d
+d-isPreMetric = record
+  { isProtoMetric = d-isProtoMetric
+  ; ≈⇒0 = d-definite
+  }
+
+d-isQuasiSemiMetric : IsQuasiSemiMetric _≡_ d
+d-isQuasiSemiMetric = record
+  { isPreMetric = d-isPreMetric
+  ; 0⇒≈ = d-indiscernable
+  }
+
+d-isSemiMetric : IsSemiMetric _≡_ d
+d-isSemiMetric = record
+  { isQuasiSemiMetric = d-isQuasiSemiMetric
+  ; sym = d-sym
+  }
+
+d-isMetric : IsMetric _≡_ d
+d-isMetric = record
+  { isSemiMetric = d-isSemiMetric
+  ; triangle = d-triangle
+  }
+
+d-metric : Metric _ _
+d-metric = record { isMetric = d-isMetric }
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda
new file mode 100644
index 0000000000..0da5045fc9
--- /dev/null
+++ b/src/Data/Real/Base.agda
@@ -0,0 +1,217 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Real numbers
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible --guardedness #-}
+
+module Data.Real.Base where
+
+open import Codata.Guarded.Stream
+open import Codata.Guarded.Stream.Properties
+open import Data.Integer.Base using (+<+)
+open import Data.Nat.Base as ℕ using (z≤n; s≤s)
+import Data.Nat.Properties as ℕ
+open import Data.Product.Base hiding (map)
+open import Data.Rational.Base as ℚ hiding (_+_; -_)
+open import Data.Rational.Properties
+open import Data.Rational.Solver
+open import Data.Rational.Unnormalised using (*<*)
+open import Function.Base using (_$_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
+open import Relation.Nullary
+
+open import Function.Metric.Rational.CauchySequence d-metric public renaming (CauchySequence to ℝ)
+
+fromℚ : ℚ → ℝ
+fromℚ = embed
+
+0ℝ : ℝ
+0ℝ = fromℚ 0ℚ
+
+_+_ : ℝ → ℝ → ℝ
+sequence (x + y) = zipWith ℚ._+_ (sequence x) (sequence y)
+isCauchy (x + y) ε = proj₁ [x] ℕ.+ proj₁ [y] , λ {m} {n} m≥N n≥N → begin-strict
+  ∣ lookup (zipWith ℚ._+_ (sequence x) (sequence y)) m - lookup (zipWith ℚ._+_ (sequence x) (sequence y)) n ∣
+    ≡⟨ cong₂ (λ a b → ∣ a - b ∣)
+      (lookup-zipWith m ℚ._+_ (sequence x) (sequence y))
+      (lookup-zipWith n ℚ._+_ (sequence x) (sequence y))
+    ⟩
+  ∣ (lookup (sequence x) m ℚ.+ lookup (sequence y) m) - (lookup (sequence x) n ℚ.+ lookup (sequence y) n) ∣
+    ≡⟨ cong ∣_∣ (lemma (lookup (sequence x) m) (lookup (sequence y) m) (lookup (sequence x) n) (lookup (sequence y) n)) ⟩
+  ∣ (lookup (sequence x) m - lookup (sequence x) n) ℚ.+ (lookup (sequence y) m - lookup (sequence y) n) ∣
+    ≤⟨ ∣p+q∣≤∣p∣+∣q∣
+      (lookup (sequence x) m - lookup (sequence x) n)
+      (lookup (sequence y) m - lookup (sequence y) n)
+    ⟩
+  ∣ lookup (sequence x) m - lookup (sequence x) n ∣ ℚ.+ ∣ lookup (sequence y) m - lookup (sequence y) n ∣
+    <⟨ +-mono-<
+      (proj₂ [x]
+        (ℕ.≤-trans (ℕ.m≤m+n (proj₁ [x]) (proj₁ [y])) m≥N)
+        (ℕ.≤-trans (ℕ.m≤m+n (proj₁ [x]) (proj₁ [y])) n≥N)
+      )
+      (proj₂ [y]
+        (ℕ.≤-trans (ℕ.m≤n+m (proj₁ [y]) (proj₁ [x])) m≥N)
+        (ℕ.≤-trans (ℕ.m≤n+m (proj₁ [y]) (proj₁ [x])) n≥N)
+      )
+    ⟩
+  ½ * ε ℚ.+ ½ * ε
+    ≡⟨ *-distribʳ-+ ε ½ ½ ⟨
+  1ℚ * ε
+    ≡⟨ *-identityˡ ε ⟩
+  ε ∎
+  where
+    open ≤-Reasoning
+    instance _ : Positive (½ * ε)
+    _ = pos*pos⇒pos ½ ε
+    [x] = isCauchy x (½ * ε)
+    [y] = isCauchy y (½ * ε)
+
+    lemma : ∀ a b c d → (a ℚ.+ b) - (c ℚ.+ d) ≡ (a - c) ℚ.+ (b - d)
+    lemma = solve 4 (λ a b c d → ((a :+ b) :- (c :+ d)) , ((a :- c) :+ (b :- d))) refl
+      where open +-*-Solver
+
+-_ : ℝ → ℝ
+sequence (- x) = map ℚ.-_ (sequence x)
+isCauchy (- x) ε = proj₁ (isCauchy x ε) , λ {m} {n} m≥N n≥N → begin-strict
+  ∣ lookup (map ℚ.-_ (sequence x)) m - lookup (map ℚ.-_ (sequence x)) n ∣
+    ≡⟨ cong₂ (λ a b → ∣ a - b ∣) (lookup-map m ℚ.-_ (sequence x)) (lookup-map n ℚ.-_ (sequence x)) ⟩
+  ∣ ℚ.- lookup (sequence x) m - ℚ.- lookup (sequence x) n ∣
+    ≡⟨ cong ∣_∣ (lemma (lookup (sequence x) m) (lookup (sequence x) n)) ⟩
+  ∣ ℚ.- (lookup (sequence x) m - lookup (sequence x) n) ∣
+    ≡⟨ ∣-p∣≡∣p∣ (lookup (sequence x) m - lookup (sequence x) n) ⟩
+  ∣ lookup (sequence x) m - lookup (sequence x) n ∣
+    <⟨ proj₂ (isCauchy x ε) m≥N n≥N ⟩
+  ε ∎
+  where
+    open ≤-Reasoning
+    lemma : ∀ a b → ℚ.- a - ℚ.- b ≡ ℚ.- (a - b)
+    lemma = solve 2 (λ a b → (:- a) :- (:- b) , (:- (a :- b))) refl
+      where open +-*-Solver
+
+_*ₗ_ : ℚ → ℝ → ℝ
+sequence (p *ₗ x) = map (p *_) (sequence x)
+isCauchy (p *ₗ x) ε with p ≟ 0ℚ
+... | yes p≡0 = 0 , λ {m} {n} _ _ → begin-strict
+  ∣ lookup (map (p *_) (sequence x)) m - lookup (map (p *_) (sequence x)) n ∣
+    ≡⟨ cong₂ (λ a b → ∣ a - b ∣) (lookup-map m (p *_) (sequence x)) (lookup-map n (p *_) (sequence x)) ⟩
+  ∣ p * lookup (sequence x) m - p * lookup (sequence x) n ∣
+    ≡⟨ cong (λ # → ∣ p * lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (lookup (sequence x) n)) ⟩
+  ∣ p * lookup (sequence x) m ℚ.+ p * ℚ.- lookup (sequence x) n ∣
+    ≡⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (ℚ.- lookup (sequence x) n)) ⟨
+  ∣ p * (lookup (sequence x) m - lookup (sequence x) n) ∣
+    ≡⟨ cong (λ # → ∣ # * (lookup (sequence x) m - lookup (sequence x) n) ∣) p≡0 ⟩
+  ∣ 0ℚ * (lookup (sequence x) m - lookup (sequence x) n) ∣
+    ≡⟨ cong ∣_∣ (*-zeroˡ (lookup (sequence x) m - lookup (sequence x) n)) ⟩
+  ∣ 0ℚ ∣
+    ≡⟨⟩
+  0ℚ
+    <⟨ positive⁻¹ ε ⟩
+  ε ∎
+  where open ≤-Reasoning
+... | no  p≢0 = proj₁ (isCauchy x (1/ ∣ p ∣ * ε)) , λ {m} {n} m≥N n≥N → begin-strict
+  ∣ lookup (map (p *_) (sequence x)) m - lookup (map (p *_) (sequence x)) n ∣
+    ≡⟨ cong₂ (λ a b → ∣ a - b ∣) (lookup-map m (p *_) (sequence x)) (lookup-map n (p *_) (sequence x)) ⟩
+  ∣ p * lookup (sequence x) m - p * lookup (sequence x) n ∣
+    ≡⟨ cong (λ # → ∣ p * lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (lookup (sequence x) n)) ⟩
+  ∣ p * lookup (sequence x) m ℚ.+ p * ℚ.- lookup (sequence x) n ∣
+    ≡⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (ℚ.- lookup (sequence x) n)) ⟨
+  ∣ p * (lookup (sequence x) m - lookup (sequence x) n) ∣
+    ≡⟨ ∣p*q∣≡∣p∣*∣q∣ p (lookup (sequence x) m - lookup (sequence x) n) ⟩
+  ∣ p ∣ * ∣ lookup (sequence x) m - lookup (sequence x) n ∣
+    <⟨ *-monoʳ-<-pos ∣ p ∣ (proj₂ (isCauchy x (1/ ∣ p ∣ * ε)) m≥N n≥N) ⟩
+  ∣ p ∣ * (1/ ∣ p ∣ * ε)
+    ≡⟨ *-assoc ∣ p ∣ (1/ ∣ p ∣) ε ⟨
+  (∣ p ∣ * 1/ ∣ p ∣) * ε
+    ≡⟨ cong (_* ε) (*-inverseʳ ∣ p ∣) ⟩
+  1ℚ * ε
+    ≡⟨ *-identityˡ ε ⟩
+  ε ∎
+  where
+    open ≤-Reasoning
+    instance _ : NonZero ∣ p ∣
+    _ = ≢-nonZero {∣ p ∣} λ ∣p∣≡0 → p≢0 (∣p∣≡0⇒p≡0 p ∣p∣≡0)
+    instance _ : Positive ∣ p ∣
+    _ = nonNeg∧nonZero⇒pos ∣ p ∣ {{∣-∣-nonNeg p}}
+    instance _ : Positive (1/ ∣ p ∣)
+    _ = 1/pos⇒pos ∣ p ∣
+    instance _ : Positive (1/ ∣ p ∣ * ε)
+    _ = pos*pos⇒pos (1/ ∣ p ∣) ε
+
+square : ℝ → ℝ
+sequence (square x) = map (λ p → p * p) (sequence x)
+isCauchy (square x) ε = B ℕ.⊔ proj₁ (isCauchy x (1/ (b ℚ.+ b) * ε)) , λ {m} {n} m≥N n≥N → begin-strict
+  ∣ lookup (map (λ p → p * p) (sequence x)) m - lookup (map (λ p → p * p) (sequence x)) n ∣
+    ≡⟨ cong₂ (λ a b → ∣ a - b ∣) (lookup-map m _ (sequence x)) (lookup-map n _ (sequence x)) ⟩
+  ∣ lookup (sequence x) m * lookup (sequence x) m - lookup (sequence x) n * lookup (sequence x) n ∣
+    ≡⟨ cong ∣_∣ (lemma (lookup (sequence x) m) (lookup (sequence x) n)) ⟩
+  ∣ (lookup (sequence x) m ℚ.+ lookup (sequence x) n) * (lookup (sequence x) m - lookup (sequence x) n) ∣
+    ≡⟨ ∣p*q∣≡∣p∣*∣q∣ (lookup (sequence x) m ℚ.+ lookup (sequence x) n) (lookup (sequence x) m - lookup (sequence x) n) ⟩
+  ∣ lookup (sequence x) m ℚ.+ lookup (sequence x) n ∣ * ∣ lookup (sequence x) m - lookup (sequence x) n ∣
+    ≤⟨ *-monoʳ-≤-nonNeg ∣ lookup (sequence x) m - lookup (sequence x) n ∣
+      {{∣-∣-nonNeg (lookup (sequence x) m - lookup (sequence x) n)}}
+      (∣p+q∣≤∣p∣+∣q∣ (lookup (sequence x) m) (lookup (sequence x) n))
+    ⟩
+  (∣ lookup (sequence x) m ∣ ℚ.+ ∣ lookup (sequence x) n ∣) * ∣ lookup (sequence x) m - lookup (sequence x) n ∣
+    ≤⟨ *-monoʳ-≤-nonNeg ∣ lookup (sequence x) m - lookup (sequence x) n ∣
+      {{∣-∣-nonNeg (lookup (sequence x) m - lookup (sequence x) n)}}
+      (<⇒≤ (+-mono-<
+        (b-prop (ℕ.≤-trans (ℕ.m≤m⊔n B (proj₁ (isCauchy x (1/ (b ℚ.+ b) * ε)))) m≥N))
+        (b-prop (ℕ.≤-trans (ℕ.m≤m⊔n B (proj₁ (isCauchy x (1/ (b ℚ.+ b) * ε)))) n≥N))
+      ))
+    ⟩
+  (b ℚ.+ b) * ∣ lookup (sequence x) m - lookup (sequence x) n ∣
+    <⟨ *-monoʳ-<-pos (b ℚ.+ b) (proj₂ (isCauchy x (1/ (b ℚ.+ b) * ε))
+      (ℕ.≤-trans (ℕ.m≤n⊔m B (proj₁ (isCauchy x (1/ (b ℚ.+ b) * ε)))) m≥N)
+      (ℕ.≤-trans (ℕ.m≤n⊔m B (proj₁ (isCauchy x (1/ (b ℚ.+ b) * ε)))) n≥N)
+    ) ⟩
+  (b ℚ.+ b) * (1/ (b ℚ.+ b) * ε)
+    ≡⟨ *-assoc (b ℚ.+ b) (1/ (b ℚ.+ b)) ε ⟨
+  ((b ℚ.+ b) * 1/ (b ℚ.+ b)) * ε
+    ≡⟨ cong (_* ε) (*-inverseʳ (b ℚ.+ b)) ⟩
+  1ℚ * ε
+    ≡⟨ *-identityˡ ε ⟩
+  ε ∎
+  where
+    open ≤-Reasoning
+
+    B : ℕ.ℕ
+    B = proj₁ (isCauchy x 1ℚ)
+
+    b : ℚ
+    b = 1ℚ ℚ.+ ∣ lookup (sequence x) B ∣
+
+    instance _ : Positive b
+    _ = pos+nonNeg⇒pos 1ℚ ∣ lookup (sequence x) B ∣ {{∣-∣-nonNeg (lookup (sequence x) B)}}
+
+    instance _ : NonZero b
+    _ = pos⇒nonZero b
+
+    instance _ : Positive (b ℚ.+ b)
+    _ = pos+pos⇒pos b b
+
+    instance _ : NonZero (b ℚ.+ b)
+    _ = pos⇒nonZero (b ℚ.+ b)
+
+    instance _ : Positive (1/ (b ℚ.+ b) * ε)
+    _ = pos*pos⇒pos (1/ (b ℚ.+ b)) {{1/pos⇒pos (b ℚ.+ b)}} ε
+
+    b-prop : ∀ {n} → n ℕ.≥ B → ∣ lookup (sequence x) n ∣ < b
+    b-prop {n} n≥B = begin-strict
+     ∣ lookup (sequence x) n ∣
+       ≡⟨ cong ∣_∣ (+-identityʳ (lookup (sequence x) n)) ⟨
+     ∣ lookup (sequence x) n ℚ.+ 0ℚ ∣
+       ≡⟨ cong (λ # → ∣ lookup (sequence x) n ℚ.+ # ∣) (+-inverseˡ (lookup (sequence x) B)) ⟨
+     ∣ lookup (sequence x) n ℚ.+ (ℚ.- lookup (sequence x) B ℚ.+ lookup (sequence x) B) ∣
+       ≡⟨ cong ∣_∣ (+-assoc (lookup (sequence x) n) (ℚ.- lookup (sequence x) B) (lookup (sequence x) B)) ⟨
+     ∣ (lookup (sequence x) n - lookup (sequence x) B) ℚ.+ lookup (sequence x) B ∣
+       ≤⟨ ∣p+q∣≤∣p∣+∣q∣ (lookup (sequence x) n - lookup (sequence x) B) (lookup (sequence x) B) ⟩
+     ∣ lookup (sequence x) n - lookup (sequence x) B ∣ ℚ.+ ∣ lookup (sequence x) B ∣
+       <⟨ +-monoˡ-< ∣ lookup (sequence x) B ∣ (proj₂ (isCauchy x 1ℚ) n≥B ℕ.≤-refl) ⟩
+     1ℚ ℚ.+ ∣ lookup (sequence x) B ∣ ≡⟨⟩
+     b ∎
+
+    lemma : ∀ a b → a * a - b * b ≡ (a ℚ.+ b) * (a - b)
+    lemma = solve 2 (λ a b → (a :* a :- b :* b) , ((a :+ b) :* (a :- b))) refl
+      where open +-*-Solver
diff --git a/src/Data/Real/Properties.agda b/src/Data/Real/Properties.agda
new file mode 100644
index 0000000000..66e6abda91
--- /dev/null
+++ b/src/Data/Real/Properties.agda
@@ -0,0 +1,80 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of real numbers
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible --guardedness #-}
+
+module Data.Real.Properties where
+
+open import Data.Real.Base
+
+open import Algebra.Definitions _≈_
+open import Codata.Guarded.Stream
+open import Codata.Guarded.Stream.Properties
+import Codata.Guarded.Stream.Relation.Binary.Pointwise as PW
+open import Data.Product.Base
+import Data.Integer.Base as ℤ
+import Data.Nat.Base as ℕ
+import Data.Nat.Properties as ℕ
+import Data.Rational.Base as ℚ
+import Data.Rational.Properties as ℚ
+open import Data.Rational.Solver
+open import Function.Base using (_$_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
+
++-cong : Congruent₂ _+_
++-cong {x} {y} {u} {v} x≈y u≈v ε = proj₁ (x≈y (ℚ.½ ℚ.* ε)) ℕ.⊔ proj₁ (u≈v (ℚ.½ ℚ.* ε)) , λ {n} n≥N → begin-strict
+  ℚ.∣ lookup (zipWith ℚ._+_ (sequence x) (sequence u)) n ℚ.- lookup (zipWith ℚ._+_ (sequence y) (sequence v)) n ∣
+    ≡⟨ cong₂ (λ a b → ℚ.∣ a ℚ.- b ∣) (lookup-zipWith n ℚ._+_ (sequence x) (sequence u)) (lookup-zipWith n ℚ._+_ (sequence y) (sequence v)) ⟩
+  ℚ.∣ (lookup (sequence x) n ℚ.+ lookup (sequence u) n) ℚ.- (lookup (sequence y) n ℚ.+ lookup (sequence v) n) ∣
+    ≡⟨ cong ℚ.∣_∣ (lemma (lookup (sequence x) n) (lookup (sequence u) n) (lookup (sequence y) n) (lookup (sequence v) n)) ⟩
+  ℚ.∣ (lookup (sequence x) n ℚ.- lookup (sequence y) n) ℚ.+ (lookup (sequence u) n ℚ.- lookup (sequence v) n) ∣
+    ≤⟨ ℚ.∣p+q∣≤∣p∣+∣q∣ (lookup (sequence x) n ℚ.- lookup (sequence y) n) (lookup (sequence u) n ℚ.- lookup (sequence v) n) ⟩
+  ℚ.∣ lookup (sequence x) n ℚ.- lookup (sequence y) n ∣ ℚ.+ ℚ.∣ lookup (sequence u) n ℚ.- lookup (sequence v) n ∣
+    <⟨ ℚ.+-mono-<
+      (proj₂ (x≈y (ℚ.½ ℚ.* ε)) (ℕ.≤-trans (ℕ.m≤m⊔n (proj₁ (x≈y (ℚ.½ ℚ.* ε))) (proj₁ (u≈v (ℚ.½ ℚ.* ε)))) n≥N))
+      (proj₂ (u≈v (ℚ.½ ℚ.* ε)) (ℕ.≤-trans (ℕ.m≤n⊔m (proj₁ (x≈y (ℚ.½ ℚ.* ε))) (proj₁ (u≈v (ℚ.½ ℚ.* ε)))) n≥N))
+    ⟩
+  ℚ.½ ℚ.* ε ℚ.+ ℚ.½ ℚ.* ε
+    ≡˘⟨ ℚ.*-distribʳ-+ ε ℚ.½ ℚ.½ ⟩
+  ℚ.1ℚ ℚ.* ε
+    ≡⟨ ℚ.*-identityˡ ε ⟩
+  ε ∎
+  where
+    open ℚ.≤-Reasoning
+    instance _ : ℚ.Positive (ℚ.½ ℚ.* ε)
+    _ = ℚ.pos*pos⇒pos ℚ.½ ε
+
+    lemma : ∀ a b c d → (a ℚ.+ b) ℚ.- (c ℚ.+ d) ≡ (a ℚ.- c) ℚ.+ (b ℚ.- d)
+    lemma = solve 4 (λ a b c d → ((a :+ b) :- (c :+ d)) , ((a :- c) :+ (b :- d))) refl
+      where open +-*-Solver
+
++-assoc : Associative _+_
++-assoc x y z ε = 0 , λ {n} _ → begin-strict
+  ℚ.∣ lookup (zipWith ℚ._+_ (zipWith ℚ._+_ (sequence x) (sequence y)) (sequence z)) n ℚ.- lookup (zipWith ℚ._+_ (sequence x) (zipWith ℚ._+_ (sequence y) (sequence z))) n ∣
+    ≡⟨ ℚ.d-definite (cong-lookup (PW.assoc ℚ.+-assoc (sequence x) (sequence y) (sequence z)) n) ⟩
+  ℚ.0ℚ
+    <⟨ ℚ.positive⁻¹ ε ⟩
+  ε ∎
+  where open ℚ.≤-Reasoning
+
++-comm : Commutative _+_
++-comm x y ε = 0 , λ {n} _ → begin-strict
+  ℚ.∣ lookup (zipWith ℚ._+_ (sequence x) (sequence y)) n ℚ.- lookup (zipWith ℚ._+_ (sequence y) (sequence x)) n ∣
+    ≡⟨ ℚ.d-definite (cong-lookup (PW.comm ℚ.+-comm (sequence x) (sequence y)) n) ⟩
+  ℚ.0ℚ
+    <⟨ ℚ.positive⁻¹ ε ⟩
+  ε ∎
+  where open ℚ.≤-Reasoning
+
++-identityˡ : LeftIdentity 0ℝ _+_
++-identityˡ x ε = 0 , λ {n} _ → begin-strict
+  ℚ.∣ lookup (zipWith ℚ._+_ (repeat ℚ.0ℚ) (sequence x)) n ℚ.- lookup (sequence x) n ∣
+    ≡⟨ ℚ.d-definite (cong-lookup (PW.identityˡ ℚ.+-identityˡ (sequence x)) n) ⟩
+  ℚ.0ℚ
+    <⟨ ℚ.positive⁻¹ ε ⟩
+  ε ∎
+  where open ℚ.≤-Reasoning
+
diff --git a/src/Function/Metric/Rational/CauchySequence.agda b/src/Function/Metric/Rational/CauchySequence.agda
new file mode 100644
index 0000000000..b82ac55c92
--- /dev/null
+++ b/src/Function/Metric/Rational/CauchySequence.agda
@@ -0,0 +1,80 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Cauchy sequences on a metric over the rationals
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible --guardedness #-}
+
+open import Function.Metric.Rational.Bundles
+
+module Function.Metric.Rational.CauchySequence {a ℓ} (M : Metric a ℓ) where
+
+open Metric M hiding (_≈_)
+
+open import Codata.Guarded.Stream
+open import Codata.Guarded.Stream.Properties
+open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s)
+import Data.Nat.Properties as ℕ
+open import Data.Integer.Base using (+<+)
+open import Data.Product.Base
+open import Data.Rational.Base
+open import Data.Rational.Properties
+open import Function.Base
+open import Level
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality using (cong₂)
+
+record CauchySequence : Set a where
+  field
+    sequence : Stream Carrier
+    isCauchy : ∀ ε → .{{Positive ε}} → Σ[ N ∈ ℕ ] ∀ {m n} → m ℕ.≥ N → n ℕ.≥ N → d (lookup sequence m) (lookup sequence n) < ε
+
+open CauchySequence public
+
+_≈_ : Rel CauchySequence zero
+x ≈ y = ∀ ε → .{{Positive ε}} → Σ[ N ∈ ℕ ] (∀ {n} → n ℕ.≥ N → d (lookup (sequence x) n) (lookup (sequence y) n) < ε)
+
+≈-refl : Reflexive _≈_
+≈-refl {x} ε = 0 , λ {n} _ → begin-strict
+  d (lookup (sequence x) n) (lookup (sequence x) n) ≡⟨ ≈⇒0 EqC.refl ⟩
+  0ℚ                                                <⟨ positive⁻¹ ε ⟩
+  ε                                                 ∎
+  where open ≤-Reasoning
+
+≈-sym : Symmetric _≈_
+≈-sym {x} {y} p ε = proj₁ (p ε) , λ {n} n≥N → begin-strict
+  d (lookup (sequence y) n) (lookup (sequence x) n) ≡⟨ sym (lookup (sequence y) n) (lookup (sequence x) n) ⟩
+  d (lookup (sequence x) n) (lookup (sequence y) n) <⟨ proj₂ (p ε) n≥N ⟩
+  ε                                                 ∎
+  where open ≤-Reasoning
+
+≈-trans : Transitive _≈_
+≈-trans {x} {y} {z} p q ε = proj₁ (p (½ * ε)) ℕ.⊔ proj₁ (q (½ * ε)) , λ {n} n≥N → begin-strict
+  d (lookup (sequence x) n) (lookup (sequence z) n)
+    ≤⟨ triangle (lookup (sequence x) n) (lookup (sequence y) n) (lookup (sequence z) n) ⟩
+  d (lookup (sequence x) n) (lookup (sequence y) n) + d (lookup (sequence y) n) (lookup (sequence z) n)
+    <⟨ +-mono-<
+      (proj₂ (p (½ * ε)) (ℕ.≤-trans (ℕ.m≤m⊔n (proj₁ (p (½ * ε))) (proj₁ (q (½ * ε)))) n≥N))
+      (proj₂ (q (½ * ε)) (ℕ.≤-trans (ℕ.m≤n⊔m (proj₁ (p (½ * ε))) (proj₁ (q (½ * ε)))) n≥N))
+    ⟩
+  ½ * ε + ½ * ε
+    ≡˘⟨ *-distribʳ-+ ε ½ ½ ⟩
+  1ℚ * ε
+    ≡⟨ *-identityˡ ε ⟩
+  ε
+    ∎
+  where
+    open ≤-Reasoning
+    instance _ : Positive (½ * ε)
+    _ = pos*pos⇒pos ½ ε
+
+embed : Carrier → CauchySequence
+embed x = record
+  { sequence = repeat x
+  ; isCauchy = λ ε → 0 , λ {m n} _ _ → begin-strict
+    d (lookup (repeat x) m) (lookup (repeat x) n) ≡⟨ cong₂ d (lookup-repeat m x) (lookup-repeat n x) ⟩
+    d x x                                         ≡⟨ ≈⇒0 EqC.refl ⟩
+    0ℚ                                            <⟨ positive⁻¹ ε ⟩
+    ε                                             ∎
+  } where open ≤-Reasoning