Metric spaces (#1162)

This PR introduces the concept of metric spaces.

We introduce a new module `metric-spaces` with the following submodules:

### Premetric spaces

- `premetric-structures`: premetric structures on a type and basic
properties;
- `reflexive-premetric-structures`;
- `symmetric-premetric-structures`;
- `monotonic-premetric-structures`: premetrics with upper-stable
neighborhoods;
- `triangular-premetric-structures`: premetrics that satisfy a
triangular inequality;
- `extensional-premetric-structures`: premetrics here
indistinguishability characterizes equality;
- `closed-premetric-structures`: premetrics with closed neighborhoods;
- `discrete-premetric-structures`: premetric structure defined by mere
equality;
- `induced-premetric-structures-on-preimages`: premetric induced on the
domain of a map by a premetric on its codomain;
- `ordering-premetric-structures`: a partial ordering on the premetric
structures on a type;
- `premetric-spaces`: types equipped with a premetric structure;
- `short-functions-premetric-spaces`: functions between premetric spaces
that preserve neighborhoods;
- `isometries-premetric-spaces`: functions between premetric spaces that
identify neighborhoods;
- `equality-of-premetric-spaces`: identity principle for the type of
premetric spaces;
- `invertible-isometries-premetric-spaces`: another characterization of
equality of premetric spaces;
- `isometric-equivalences-premetric-spaces`: another characterization of
equality of premetric spaces;
- `cauchy-approximations-premetric-spaces`: the type of Cauchy
approximations in a premetric space;
- `limits-of-cauchy-approximations-in-premetric-spaces`;

### Pseudometric spaces

- `pseudometric-structures`: reflexive, symmetric, and triangular
premetrics;
- `pseudometric-spaces`: types equipped with a pseudometric structure;

### Metric spaces

- `metric-structures`: reflexive, symmetric, triangular, and local
premetrics;
- `metric-spaces`: types equipped with a metric structure;
- `saturated-metric-spaces`: metric spaces with closed premetrics;
- `subspaces-metric-spaces`: metric structure induced on subsets of
metric spaces;
- `dependent-products-metric-spaces`: metric structure on dependent
families of metric spaces;
- `functions-metric-spaces`: functions between carrier types of metric
spaces;
- `short-functions-metric-spaces`: short functions between the
underlying premetric spaces of metric spaces;
- `isometries-metric-spaces`: isometries between the underlying
premetric spaces of metric spaces;
- `equality-of-metric-spaces`: identity principle in the type of metric
spaces;
- `cauchy-approximations-metric-spaces`: the type of Cauchy
approximations in a metric space;
- `convergent-cauchy-approximations-metric-spaces`: the type of
convergent Cauchy approximations in a metric space;
- `complete-metric-spaces`: the type of metric spaces where all Cauchy
approximations are convergent;

### Example of metric spaces

- `metric-space-of-cauchy-approximations-in-a-metric-space`;
- `metric-space-of-convergent-cauchy-approximations-in-a-metric-space`;
- `metric-space-of-rational-numbers`;
- `metric-space-of-rational-numbers-with-open-neighborhoods`;

### Categories of metric spaces and functors between them

- `precategory-of-metric-spaces-and-functions`;
- `precategory-of-metric-spaces-and-isometries`;
- `precategory-of-metric-spaces-and-short-functions`;
- `category-of-metric-spaces-and-isometries`;
- `category-of-metric-spaces-and-short-functions`;
- `functor-category-set-functions-isometry-metric-spaces`;
- `functor-category-short-isometry-metric-spaces`.

We also introduce the standard metric structure on the real numbers in
`real-numbers.metric-space-of-real-numbers` and a few miscellaneous
lemmas in
`elementary-number-theory` and `foundation`.

---------

Co-authored-by: Fredrik Bakke <[email protected]>

references.bib

@@ -51,6 +51,14 @@ @online{BdJR24
   keywords    = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Category Theory}
 }
 
+@phdthesis{Booij20PhD,
+  title        = {Analysis in univalent type theory},
+  author       = {Booij, Auke Bart},
+  year         = {2020},
+  school       = {University of Birmingham},
+  url          = {https://etheses.bham.ac.uk/id/eprint/10411/7/Booij20PhD.pdf}
+}
+
 @book{BSCS05,
   title     = {Absztrakt algebrai feladatok},
   author    = {Bálintné Szendrei, Mária and Czédli, Gábor and Szendrei, Ágnes},

src/elementary-number-theory/inequality-integer-fractions.lagda.md

@@ -7,6 +7,7 @@ module elementary-number-theory.inequality-integer-fractions where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-integer-fractions
 open import elementary-number-theory.addition-integers
 open import elementary-number-theory.addition-positive-and-negative-integers
 open import elementary-number-theory.cross-multiplication-difference-integer-fractions
@@ -124,3 +125,72 @@ transitive-leq-fraction-ℤ p q r H H' =
             ( H'))))
     ( is-positive-denominator-fraction-ℤ q)
 ```
+
+### Chaining rules for similarity and inequality on the integer fractions
+
+```agda
+module _
+  (p q r : fraction-ℤ)
+  where
+
+  concatenate-sim-leq-fraction-ℤ :
+    sim-fraction-ℤ p q →
+    leq-fraction-ℤ q r →
+    leq-fraction-ℤ p r
+  concatenate-sim-leq-fraction-ℤ H H' =
+    is-nonnegative-right-factor-mul-ℤ
+      ( is-nonnegative-eq-ℤ
+        ( lemma-left-sim-cross-mul-diff-fraction-ℤ p q r H)
+        ( is-nonnegative-mul-ℤ
+          ( is-nonnegative-is-positive-ℤ (is-positive-denominator-fraction-ℤ p))
+          ( H')))
+      ( is-positive-denominator-fraction-ℤ q)
+
+  concatenate-leq-sim-fraction-ℤ :
+    leq-fraction-ℤ p q →
+    sim-fraction-ℤ q r →
+    leq-fraction-ℤ p r
+  concatenate-leq-sim-fraction-ℤ H H' =
+    is-nonnegative-right-factor-mul-ℤ
+      ( is-nonnegative-eq-ℤ
+        ( inv (lemma-right-sim-cross-mul-diff-fraction-ℤ p q r H'))
+        ( is-nonnegative-mul-ℤ
+          ( is-nonnegative-is-positive-ℤ (is-positive-denominator-fraction-ℤ r))
+          ( H)))
+      ( is-positive-denominator-fraction-ℤ q)
+```
+
+### The similarity of integer fractions preserves inequality
+
+```agda
+module _
+  (p q p' q' : fraction-ℤ) (H : sim-fraction-ℤ p p') (K : sim-fraction-ℤ q q')
+  where
+
+  preserves-leq-sim-fraction-ℤ : leq-fraction-ℤ p q → leq-fraction-ℤ p' q'
+  preserves-leq-sim-fraction-ℤ I =
+    concatenate-sim-leq-fraction-ℤ p' p q'
+      ( symmetric-sim-fraction-ℤ p p' H)
+      ( concatenate-leq-sim-fraction-ℤ p q q' I K)
+```
+
+### `x ≤ y` if and only if `0 ≤ y - x`
+
+```agda
+module _
+  (x y : fraction-ℤ)
+  where
+
+  eq-translate-diff-leq-zero-fraction-ℤ :
+    leq-fraction-ℤ zero-fraction-ℤ (y +fraction-ℤ (neg-fraction-ℤ x)) ＝
+    leq-fraction-ℤ x y
+  eq-translate-diff-leq-zero-fraction-ℤ =
+    ap
+      ( is-nonnegative-ℤ)
+      ( ( cross-mul-diff-zero-fraction-ℤ (y +fraction-ℤ (neg-fraction-ℤ x))) ∙
+        ( ap
+          ( add-ℤ ( (numerator-fraction-ℤ y) *ℤ (denominator-fraction-ℤ x)))
+          ( left-negative-law-mul-ℤ
+            ( numerator-fraction-ℤ x)
+            ( denominator-fraction-ℤ y))))
+```

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

@@ -7,8 +7,11 @@ module elementary-number-theory.inequality-rational-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-integer-fractions
+open import elementary-number-theory.addition-rational-numbers
 open import elementary-number-theory.cross-multiplication-difference-integer-fractions
 open import elementary-number-theory.difference-integers
+open import elementary-number-theory.difference-rational-numbers
 open import elementary-number-theory.inequality-integer-fractions
 open import elementary-number-theory.inequality-integers
 open import elementary-number-theory.integer-fractions
@@ -19,7 +22,9 @@ open import elementary-number-theory.nonpositive-integers
 open import elementary-number-theory.positive-and-negative-integers
 open import elementary-number-theory.positive-integers
 open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.reduced-integer-fractions
 
+open import foundation.action-on-identifications-functions
 open import foundation.cartesian-product-types
 open import foundation.conjunction
 open import foundation.coproduct-types
@@ -28,8 +33,10 @@ open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.functoriality-coproduct-types
 open import foundation.identity-types
+open import foundation.logical-equivalences
 open import foundation.negation
 open import foundation.propositions
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import order-theory.posets
@@ -151,6 +158,176 @@ module _
 ℚ-Poset = (ℚ-Preorder , antisymmetric-leq-ℚ)
 ```
 
+### The canonical map from integer fractions to the rational numbers preserves inequality
+
+```agda
+module _
+  (p q : fraction-ℤ)
+  where
+
+  preserves-leq-rational-fraction-ℤ :
+    leq-fraction-ℤ p q → leq-ℚ (rational-fraction-ℤ p) (rational-fraction-ℤ q)
+  preserves-leq-rational-fraction-ℤ =
+    preserves-leq-sim-fraction-ℤ
+      ( p)
+      ( q)
+      ( reduce-fraction-ℤ p)
+      ( reduce-fraction-ℤ q)
+      ( sim-reduced-fraction-ℤ p)
+      ( sim-reduced-fraction-ℤ q)
+
+module _
+  (x : ℚ) (p : fraction-ℤ)
+  where
+
+  preserves-leq-right-rational-fraction-ℤ :
+    leq-fraction-ℤ (fraction-ℚ x) p → leq-ℚ x (rational-fraction-ℤ p)
+  preserves-leq-right-rational-fraction-ℤ H =
+    concatenate-leq-sim-fraction-ℤ
+      ( fraction-ℚ x)
+      ( p)
+      ( fraction-ℚ ( rational-fraction-ℤ p))
+      ( H)
+      ( sim-reduced-fraction-ℤ p)
+
+  reflects-leq-right-rational-fraction-ℤ :
+    leq-ℚ x (rational-fraction-ℤ p) → leq-fraction-ℤ (fraction-ℚ x) p
+  reflects-leq-right-rational-fraction-ℤ H =
+    concatenate-leq-sim-fraction-ℤ
+      ( fraction-ℚ x)
+      ( reduce-fraction-ℤ p)
+      ( p)
+      ( H)
+      ( symmetric-sim-fraction-ℤ
+        ( p)
+        ( reduce-fraction-ℤ p)
+        ( sim-reduced-fraction-ℤ p))
+
+  iff-leq-right-rational-fraction-ℤ :
+    leq-fraction-ℤ (fraction-ℚ x) p ↔ leq-ℚ x (rational-fraction-ℤ p)
+  pr1 iff-leq-right-rational-fraction-ℤ =
+    preserves-leq-right-rational-fraction-ℤ
+  pr2 iff-leq-right-rational-fraction-ℤ = reflects-leq-right-rational-fraction-ℤ
+
+  preserves-leq-left-rational-fraction-ℤ :
+    leq-fraction-ℤ p (fraction-ℚ x) → leq-ℚ (rational-fraction-ℤ p) x
+  preserves-leq-left-rational-fraction-ℤ =
+    concatenate-sim-leq-fraction-ℤ
+      ( fraction-ℚ ( rational-fraction-ℤ p))
+      ( p)
+      ( fraction-ℚ x)
+      ( symmetric-sim-fraction-ℤ
+        ( p)
+        ( fraction-ℚ ( rational-fraction-ℤ p))
+        ( sim-reduced-fraction-ℤ p))
+
+  reflects-leq-left-rational-fraction-ℤ :
+    leq-ℚ (rational-fraction-ℤ p) x → leq-fraction-ℤ p (fraction-ℚ x)
+  reflects-leq-left-rational-fraction-ℤ =
+    concatenate-sim-leq-fraction-ℤ
+      ( p)
+      ( reduce-fraction-ℤ p)
+      ( fraction-ℚ x)
+      ( sim-reduced-fraction-ℤ p)
+
+  iff-leq-left-rational-fraction-ℤ :
+    leq-fraction-ℤ p (fraction-ℚ x) ↔ leq-ℚ (rational-fraction-ℤ p) x
+  pr1 iff-leq-left-rational-fraction-ℤ = preserves-leq-left-rational-fraction-ℤ
+  pr2 iff-leq-left-rational-fraction-ℤ = reflects-leq-left-rational-fraction-ℤ
+```
+
+### `x ≤ y` if and only if `0 ≤ y - x`
+
+```agda
+module _
+  (x y : ℚ)
+  where
+
+  iff-translate-diff-leq-zero-ℚ : leq-ℚ zero-ℚ (y -ℚ x) ↔ leq-ℚ x y
+  iff-translate-diff-leq-zero-ℚ =
+    logical-equivalence-reasoning
+      leq-ℚ zero-ℚ (y -ℚ x)
+      ↔ leq-fraction-ℤ
+        ( zero-fraction-ℤ)
+        ( add-fraction-ℤ (fraction-ℚ y) (neg-fraction-ℤ (fraction-ℚ x)))
+        by
+          inv-iff
+            ( iff-leq-right-rational-fraction-ℤ
+              ( zero-ℚ)
+              ( add-fraction-ℤ (fraction-ℚ y) (neg-fraction-ℤ (fraction-ℚ x))))
+      ↔ leq-ℚ x y
+        by
+          inv-tr
+            ( _↔ leq-ℚ x y)
+            ( eq-translate-diff-leq-zero-fraction-ℤ
+              ( fraction-ℚ x)
+              ( fraction-ℚ y))
+            ( id-iff)
+```
+
+### Inequality on the rational numbers is invariant by translation
+
+```agda
+module _
+  (z x y : ℚ)
+  where
+
+  iff-translate-left-leq-ℚ : leq-ℚ (z +ℚ x) (z +ℚ y) ↔ leq-ℚ x y
+  iff-translate-left-leq-ℚ =
+    logical-equivalence-reasoning
+      leq-ℚ (z +ℚ x) (z +ℚ y)
+      ↔ leq-ℚ zero-ℚ ((z +ℚ y) -ℚ (z +ℚ x))
+        by (inv-iff (iff-translate-diff-leq-zero-ℚ (z +ℚ x) (z +ℚ y)))
+      ↔ leq-ℚ zero-ℚ (y -ℚ x)
+        by
+          ( inv-tr
+            ( _↔ leq-ℚ zero-ℚ (y -ℚ x))
+            ( ap (leq-ℚ zero-ℚ) (left-translation-diff-ℚ y x z))
+            ( id-iff))
+      ↔ leq-ℚ x y
+        by (iff-translate-diff-leq-zero-ℚ x y)
+
+  iff-translate-right-leq-ℚ : leq-ℚ (x +ℚ z) (y +ℚ z) ↔ leq-ℚ x y
+  iff-translate-right-leq-ℚ =
+    logical-equivalence-reasoning
+      leq-ℚ (x +ℚ z) (y +ℚ z)
+      ↔ leq-ℚ zero-ℚ ((y +ℚ z) -ℚ (x +ℚ z))
+        by (inv-iff (iff-translate-diff-leq-zero-ℚ (x +ℚ z) (y +ℚ z)))
+      ↔ leq-ℚ zero-ℚ (y -ℚ x)
+        by
+          ( inv-tr
+            ( _↔ leq-ℚ zero-ℚ (y -ℚ x))
+            ( ap (leq-ℚ zero-ℚ) (right-translation-diff-ℚ y x z))
+            ( id-iff))
+      ↔ leq-ℚ x y by (iff-translate-diff-leq-zero-ℚ x y)
+
+  preserves-leq-left-add-ℚ : leq-ℚ x y → leq-ℚ (x +ℚ z) (y +ℚ z)
+  preserves-leq-left-add-ℚ = backward-implication iff-translate-right-leq-ℚ
+
+  preserves-leq-right-add-ℚ : leq-ℚ x y → leq-ℚ (z +ℚ x) (z +ℚ y)
+  preserves-leq-right-add-ℚ = backward-implication iff-translate-left-leq-ℚ
+
+  reflects-leq-left-add-ℚ : leq-ℚ (x +ℚ z) (y +ℚ z) → leq-ℚ x y
+  reflects-leq-left-add-ℚ = forward-implication iff-translate-right-leq-ℚ
+
+  reflects-leq-right-add-ℚ : leq-ℚ (z +ℚ x) (z +ℚ y) → leq-ℚ x y
+  reflects-leq-right-add-ℚ = forward-implication iff-translate-left-leq-ℚ
+```
+
+### Addition on the rational numbers preserves inequality
+
+```agda
+preserves-leq-add-ℚ :
+  {a b c d : ℚ} → leq-ℚ a b → leq-ℚ c d → leq-ℚ (a +ℚ c) (b +ℚ d)
+preserves-leq-add-ℚ {a} {b} {c} {d} H K =
+  transitive-leq-ℚ
+    ( a +ℚ c)
+    ( b +ℚ c)
+    ( b +ℚ d)
+    ( preserves-leq-right-add-ℚ b c d K)
+    ( preserves-leq-left-add-ℚ c a b H)
+```
+
 ## See also
 
 - The decidable total order on the rational numbers is defined in

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

@@ -83,6 +83,14 @@ leq-right-leq-max-ℕ k (succ-ℕ m) zero-ℕ H = star
 leq-right-leq-max-ℕ (succ-ℕ k) (succ-ℕ m) (succ-ℕ n) H =
   leq-right-leq-max-ℕ k m n H
 
+left-leq-max-ℕ : (m n : ℕ) → leq-ℕ m (max-ℕ m n)
+left-leq-max-ℕ m n =
+  leq-left-leq-max-ℕ (max-ℕ m n) m n (refl-leq-ℕ (max-ℕ m n))
+
+right-leq-max-ℕ : (m n : ℕ) → leq-ℕ n (max-ℕ m n)
+right-leq-max-ℕ m n =
+  leq-right-leq-max-ℕ (max-ℕ m n) m n (refl-leq-ℕ (max-ℕ m n))
+
 is-least-upper-bound-max-ℕ :
   (m n : ℕ) → is-least-binary-upper-bound-Poset ℕ-Poset m n (max-ℕ m n)
 is-least-upper-bound-max-ℕ m n =
@@ -91,8 +99,7 @@ is-least-upper-bound-max-ℕ m n =
     { m}
     { n}
     { max-ℕ m n}
-    ( leq-left-leq-max-ℕ (max-ℕ m n) m n (refl-leq-ℕ (max-ℕ m n)) ,
-      leq-right-leq-max-ℕ (max-ℕ m n) m n (refl-leq-ℕ (max-ℕ m n)))
+    ( left-leq-max-ℕ m n , right-leq-max-ℕ m n)
     ( λ x (H , K) → leq-max-ℕ x m n H K)
 ```