Andrew Sneap, 11 November 2021, Updated 3 May 2023

In this file I define the types of complete metric spaces, along with
Cauchy and convergent sequences.

\begin{code}
{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan renaming (_+_ to _βˆ”_)

open import Naturals.Order
open import Notation.Order
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import Rationals.Positive

module MetricSpaces.Type
  (fe : Fun-Ext)
  (pe : Prop-Ext)
  (pt : propositional-truncations-exist)
 where

open PropositionalTruncation pt

m1a : (X : 𝓀 Μ‡ ) β†’ (B : X β†’ X β†’ β„šβ‚Š β†’ 𝓀₀ Μ‡ ) β†’ 𝓀 Μ‡
m1a X B = (x y : X) β†’ ((Ξ΅ : β„šβ‚Š) β†’ B x y Ξ΅) β†’ x ＝ y

m1b : (X : 𝓀 Μ‡ ) β†’ (B : X β†’ X β†’ β„šβ‚Š β†’ 𝓀₀ Μ‡ ) β†’ 𝓀 Μ‡
m1b X B = (x : X) β†’ (Ξ΅ : β„šβ‚Š) β†’ B x x Ξ΅

m2 : (X : 𝓀 Μ‡ ) β†’ (B : X β†’ X β†’ β„šβ‚Š β†’ 𝓀₀ Μ‡ ) β†’ 𝓀 Μ‡
m2 X B = (x y : X) β†’ (Ξ΅ : β„šβ‚Š) β†’ B x y Ξ΅ β†’ B y x Ξ΅

m3 : (X : 𝓀 Μ‡ ) β†’ (B : X β†’ X β†’ β„šβ‚Š β†’ 𝓀₀ Μ‡ ) β†’ 𝓀 Μ‡
m3 X B = (x y : X) β†’ (Ρ₁ Ξ΅β‚‚ : β„šβ‚Š)
                   β†’ Ρ₁ < Ξ΅β‚‚
                   β†’ B x y Ρ₁
                   β†’ B x y Ξ΅β‚‚

m4 : (X : 𝓀 Μ‡ ) β†’ (B : X β†’ X β†’ β„šβ‚Š β†’ 𝓀₀ Μ‡ ) β†’ 𝓀 Μ‡
m4 X B = (x y z : X) β†’ (Ρ₁ Ξ΅β‚‚ : β„šβ‚Š)
                     β†’ B x y Ρ₁
                     β†’ B y z Ξ΅β‚‚
                     β†’ B x z (Ρ₁ + Ξ΅β‚‚)

metric-space : (X : 𝓀 Μ‡ ) β†’ 𝓀₁ βŠ” 𝓀 Μ‡
metric-space X =
 Ξ£ B κž‰ (X β†’ X β†’ β„šβ‚Š β†’ 𝓀₀ Μ‡ ) , m1a X B Γ— m1b X B Γ— m2 X B Γ— m3 X B Γ— m4 X B

\end{code}

A space is a complete metric space if every cauchy sequence in a metric space is
also a convergent sequence. Convergent and Cauchy Sequences are also defined
below. In a metric space, all convergent sequences are cauchy sequences.

\begin{code}

bounded-sequence : (X : 𝓀 Μ‡ ) β†’ metric-space X β†’ (S : β„• β†’ X) β†’ 𝓀₀ Μ‡
bounded-sequence X (B , _) S = βˆƒ K κž‰ β„šβ‚Š , ((x y : β„•) β†’ B (S x) (S y) K)

bounded-sequence-is-prop : (X : 𝓀 Μ‡ )
                         β†’ (m : metric-space X)
                         β†’ (S : β„• β†’ X)
                         β†’ is-prop (bounded-sequence X m S)
bounded-sequence-is-prop X m S = βˆƒ-is-prop

convergent-sequence : (X : 𝓀 Μ‡ ) β†’ metric-space X β†’ (S : β„• β†’ X) β†’ 𝓀 Μ‡
convergent-sequence X (B , _) S
 = βˆƒ x κž‰ X , ((Ξ΅ : β„šβ‚Š) β†’ Ξ£ N κž‰ β„• , ((n : β„•) β†’ N < n β†’ B x (S n) Ξ΅))

cauchy-sequence : (X : 𝓀 Μ‡ ) β†’ metric-space X β†’ (S : β„• β†’ X) β†’ 𝓀₀ Μ‡
cauchy-sequence X (B , _) S
 = (Ξ΅ : β„šβ‚Š) β†’ Ξ£ N κž‰ β„• , ((m n : β„•) β†’ N ≀ m β†’ N ≀ n β†’ B (S m) (S n) Ξ΅)

convergentβ†’cauchy : (X : 𝓀 Μ‡ ) β†’ (m : metric-space X) β†’ (S : β„• β†’ X) β†’ 𝓀 Μ‡
convergent→cauchy X m S = convergent-sequence X m S → cauchy-sequence X m S

cauchyβ†’convergent : (X : 𝓀 Μ‡ ) β†’ metric-space X β†’ (S : β„• β†’ X) β†’ 𝓀 Μ‡
cauchy→convergent X m S = cauchy-sequence X m S → convergent-sequence X m S

complete-metric-space : (X : 𝓀 Μ‡ ) β†’ 𝓀₁ βŠ” 𝓀 Μ‡
complete-metric-space X
 = Ξ£ m κž‰ metric-space X , ((S : β„• β†’ X) β†’ cauchyβ†’convergent X m S)

\end{code}