Cauchy sequences in metric spaces (#1347)

Gives us the ability to go back and forth between Cauchy sequences and
Cauchy approximations, and their limits.

Naturally, this is going to be necessary for a lot of analysis built on
series and sequences.

Depends on #1345.

Author: lowasser

src/elementary-number-theory/nonzero-natural-numbers.lagda.md

@@ -17,7 +17,11 @@ open import elementary-number-theory.strict-inequality-natural-numbers
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
+open import foundation.equality-dependent-pair-types
 open import foundation.identity-types
+open import foundation.negated-equality
+open import foundation.propositions
+open import foundation.sections
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 ```
@@ -57,6 +61,9 @@ nat-ℕ⁺ = nat-nonzero-ℕ
 
 is-nonzero-nat-nonzero-ℕ : (n : nonzero-ℕ) → is-nonzero-ℕ (nat-nonzero-ℕ n)
 is-nonzero-nat-nonzero-ℕ = pr2
+
+eq-nonzero-ℕ : {m n : nonzero-ℕ} → nat-nonzero-ℕ m ＝ nat-nonzero-ℕ n → m ＝ n
+eq-nonzero-ℕ m=n = eq-pair-Σ m=n (eq-is-prop is-prop-nonequal)
 ```
 
 ### The nonzero natural number `1`
@@ -86,6 +93,24 @@ pr1 (succ-nonzero-ℕ' n) = succ-ℕ n
 pr2 (succ-nonzero-ℕ' n) = is-nonzero-succ-ℕ n
 ```
 
+### The predecessor function from the nonzero natural numbers to the natural numbers
+
+```agda
+pred-nonzero-ℕ : nonzero-ℕ → ℕ
+pred-nonzero-ℕ (succ-ℕ n , _) = n
+pred-nonzero-ℕ (zero-ℕ , H) = ex-falso (H refl)
+
+pred-ℕ⁺ : nonzero-ℕ → ℕ
+pred-ℕ⁺ = pred-nonzero-ℕ
+
+is-section-succ-nonzero-ℕ' : is-section succ-nonzero-ℕ' pred-nonzero-ℕ
+is-section-succ-nonzero-ℕ' (zero-ℕ , H) = ex-falso (H refl)
+is-section-succ-nonzero-ℕ' (succ-ℕ n , _) = eq-nonzero-ℕ refl
+
+is-section-pred-nonzero-ℕ : is-section pred-nonzero-ℕ succ-nonzero-ℕ'
+is-section-pred-nonzero-ℕ n = refl
+```
+
 ### The quotient of a nonzero natural number by a divisor
 
 ```agda
@@ -146,3 +171,13 @@ le-left-add-nat-ℕ⁺ m (n , n≠0) =
     ( right-unit-law-add-ℕ m)
     ( preserves-le-left-add-ℕ m zero-ℕ n (le-is-nonzero-ℕ n n≠0))
 ```
+
+### The predecessor function from the nonzero natural numbers reflects inequality
+
+```agda
+reflects-leq-pred-nonzero-ℕ :
+  (m n : ℕ⁺) → leq-ℕ (pred-ℕ⁺ m) (pred-ℕ⁺ n) → leq-ℕ⁺ m n
+reflects-leq-pred-nonzero-ℕ (succ-ℕ m , _) (succ-ℕ n , _) m≤n = m≤n
+reflects-leq-pred-nonzero-ℕ (zero-ℕ , H) _ = ex-falso (H refl)
+reflects-leq-pred-nonzero-ℕ (succ-ℕ _ , _) (zero-ℕ , H) = ex-falso (H refl)
+```

src/elementary-number-theory/positive-rational-numbers.lagda.md

@@ -468,6 +468,19 @@ is-prop-le-ℚ⁺ : (x y : ℚ⁺) → is-prop (le-ℚ⁺ x y)
 is-prop-le-ℚ⁺ x y = is-prop-type-Prop (le-prop-ℚ⁺ x y)
 ```
 
+### The inequality on positive rational numbers
+
+```agda
+leq-prop-ℚ⁺ : ℚ⁺ → ℚ⁺ → Prop lzero
+leq-prop-ℚ⁺ x y = leq-ℚ-Prop (rational-ℚ⁺ x) (rational-ℚ⁺ y)
+
+leq-ℚ⁺ : ℚ⁺ → ℚ⁺ → UU lzero
+leq-ℚ⁺ x y = type-Prop (leq-prop-ℚ⁺ x y)
+
+is-prop-leq-ℚ⁺ : (x y : ℚ⁺) → is-prop (leq-ℚ⁺ x y)
+is-prop-leq-ℚ⁺ x y = is-prop-type-Prop (leq-prop-ℚ⁺ x y)
+```
+
 ### The sum of two positive rational numbers is greater than each of them
 
 ```agda
@@ -685,10 +698,10 @@ module _
 
 ```agda
 abstract
-  double-le-ℚ⁺ :
+  bound-double-le-ℚ⁺ :
     (p : ℚ⁺) →
-    exists ℚ⁺ (λ q → le-prop-ℚ⁺ (q +ℚ⁺ q) p)
-  double-le-ℚ⁺ p = unit-trunc-Prop dependent-pair-result
+    Σ ℚ⁺ (λ q → le-ℚ⁺ (q +ℚ⁺ q) p)
+  bound-double-le-ℚ⁺ p = dependent-pair-result
     where
     q : ℚ⁺
     q = left-summand-split-ℚ⁺ p
@@ -710,6 +723,11 @@ abstract
           { rational-ℚ⁺ r}
           ( le-left-min-ℚ⁺ q r)
           ( le-right-min-ℚ⁺ q r))
+
+  double-le-ℚ⁺ :
+    (p : ℚ⁺) →
+    exists ℚ⁺ (λ q → le-prop-ℚ⁺ (q +ℚ⁺ q) p)
+  double-le-ℚ⁺ p = unit-trunc-Prop (bound-double-le-ℚ⁺ p)
 ```
 
 ### Addition with a positive rational number is an increasing map

src/metric-spaces.lagda.md

@@ -49,6 +49,8 @@ open import metric-spaces.category-of-metric-spaces-and-isometries public
 open import metric-spaces.category-of-metric-spaces-and-short-functions public
 open import metric-spaces.cauchy-approximations-metric-spaces public
 open import metric-spaces.cauchy-approximations-premetric-spaces public
+open import metric-spaces.cauchy-sequences-complete-metric-spaces public
+open import metric-spaces.cauchy-sequences-metric-spaces public
 open import metric-spaces.closed-premetric-structures public
 open import metric-spaces.complete-metric-spaces public
 open import metric-spaces.convergent-cauchy-approximations-metric-spaces public

src/metric-spaces/cauchy-sequences-complete-metric-spaces.lagda.md

@@ -0,0 +1,127 @@
+# Cauchy sequences in complete metric spaces
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module metric-spaces.cauchy-sequences-complete-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.universe-levels
+
+open import metric-spaces.cauchy-approximations-metric-spaces
+open import metric-spaces.cauchy-sequences-metric-spaces
+open import metric-spaces.complete-metric-spaces
+open import metric-spaces.convergent-cauchy-approximations-metric-spaces
+open import metric-spaces.metric-spaces
+```
+
+</details>
+
+## Idea
+
+A [Cauchy sequence](metric-spaces.cauchy-sequences-metric-spaces.md) in a
+[complete metric space](metric-spaces.complete-metric-spaces.md) is a Cauchy
+sequence in the underlying [metric space](metric-spaces.metric-spaces.md).
+Cauchy sequences in complete metric spaces always have a limit.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} (M : Complete-Metric-Space l1 l2)
+  where
+
+  cauchy-sequence-Complete-Metric-Space : UU (l1 ⊔ l2)
+  cauchy-sequence-Complete-Metric-Space =
+    cauchy-sequence-Metric-Space (metric-space-Complete-Metric-Space M)
+
+  is-limit-cauchy-sequence-Complete-Metric-Space :
+    cauchy-sequence-Complete-Metric-Space → type-Complete-Metric-Space M → UU l2
+  is-limit-cauchy-sequence-Complete-Metric-Space x l =
+    is-limit-cauchy-sequence-Metric-Space
+      ( metric-space-Complete-Metric-Space M)
+      ( x)
+      ( l)
+```
+
+## Properties
+
+### Every Cauchy sequence in a complete metric space has a limit
+
+```agda
+module _
+  {l1 l2 : Level} (M : Complete-Metric-Space l1 l2)
+  (x : cauchy-sequence-Complete-Metric-Space M)
+  where
+
+  limit-cauchy-sequence-Complete-Metric-Space : type-Complete-Metric-Space M
+  limit-cauchy-sequence-Complete-Metric-Space =
+    pr1
+      ( is-complete-metric-space-Complete-Metric-Space
+        ( M)
+        ( cauchy-approximation-cauchy-sequence-Metric-Space
+          ( metric-space-Complete-Metric-Space M)
+          ( x)))
+
+  is-limit-limit-cauchy-sequence-Complete-Metric-Space :
+    is-limit-cauchy-sequence-Complete-Metric-Space
+      ( M)
+      ( x)
+      ( limit-cauchy-sequence-Complete-Metric-Space)
+  is-limit-limit-cauchy-sequence-Complete-Metric-Space =
+    is-limit-cauchy-sequence-limit-cauchy-approximation-cauchy-sequence-Metric-Space
+      ( metric-space-Complete-Metric-Space M)
+      ( x)
+      ( limit-cauchy-sequence-Complete-Metric-Space)
+      ( pr2
+        ( is-complete-metric-space-Complete-Metric-Space
+          ( M)
+          ( cauchy-approximation-cauchy-sequence-Metric-Space
+            ( metric-space-Complete-Metric-Space M)
+            ( x))))
+
+  has-limit-cauchy-sequence-Complete-Metric-Space :
+    has-limit-cauchy-sequence-Metric-Space
+      ( metric-space-Complete-Metric-Space M)
+      ( x)
+  has-limit-cauchy-sequence-Complete-Metric-Space =
+    limit-cauchy-sequence-Complete-Metric-Space ,
+    is-limit-limit-cauchy-sequence-Complete-Metric-Space
+```
+
+### If every Cauchy sequence has a limit in a metric space, the metric space is complete
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  where
+
+  cauchy-sequences-have-limits-Metric-Space : UU (l1 ⊔ l2)
+  cauchy-sequences-have-limits-Metric-Space =
+    (x : cauchy-sequence-Metric-Space M) →
+    has-limit-cauchy-sequence-Metric-Space M x
+
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  (H : cauchy-sequences-have-limits-Metric-Space M)
+  where
+
+  is-complete-metric-space-cauchy-sequences-have-limits-Metric-Space :
+    is-complete-Metric-Space M
+  is-complete-metric-space-cauchy-sequences-have-limits-Metric-Space x =
+    tot
+      ( is-limit-cauchy-approximation-limit-cauchy-sequence-cauchy-approximation-Metric-Space
+        ( M)
+        ( x))
+      ( H (cauchy-sequence-cauchy-approximation-Metric-Space M x))
+
+  complete-metric-space-cauchy-sequences-have-limits-Metric-Space :
+    Complete-Metric-Space l1 l2
+  complete-metric-space-cauchy-sequences-have-limits-Metric-Space =
+    M , is-complete-metric-space-cauchy-sequences-have-limits-Metric-Space
+```