Metric properties of real negation, absolute value, addition and maximum (#1398)

This PRs proves the following metric properties of real operations:

- `raise-ℝ` is an isometry;
- `neg-ℝ` is an isometry;
- `abs-ℝ` is a short function;
- `add-ℝ` is an isometry from `ℝ` to the metric space of isometries `ℝ →
ℝ`;
- `max-ℝ` is a short function from `ℝ` to the metric space of short
functions `ℝ → ℝ`.

It also introduces the following concepts:

- the metric space of functions between metric spaces;
- the metric space of short functions between metric spaces;
- the metric space of isometries between metric spaces.

Author: malarbol

src/metric-spaces.lagda.md

@@ -78,8 +78,11 @@ open import metric-spaces.metric-space-of-cauchy-approximations-metric-spaces pu
 open import metric-spaces.metric-space-of-cauchy-approximations-saturated-complete-metric-spaces public
 open import metric-spaces.metric-space-of-convergent-cauchy-approximations-metric-spaces public
 open import metric-spaces.metric-space-of-convergent-sequences-metric-spaces public
+open import metric-spaces.metric-space-of-functions-metric-spaces public
+open import metric-spaces.metric-space-of-isometries-metric-spaces public
 open import metric-spaces.metric-space-of-rational-numbers public
 open import metric-spaces.metric-space-of-rational-numbers-with-open-neighborhoods public
+open import metric-spaces.metric-space-of-short-functions-metric-spaces public
 open import metric-spaces.metric-spaces public
 open import metric-spaces.metric-structures public
 open import metric-spaces.monotonic-premetric-structures public

src/metric-spaces/dependent-products-metric-spaces.lagda.md

@@ -8,12 +8,18 @@ module metric-spaces.dependent-products-metric-spaces where
 
 ```agda
 open import foundation.dependent-pair-types
+open import foundation.evaluation-functions
 open import foundation.function-extensionality
+open import foundation.function-types
 open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
 
+open import metric-spaces.cauchy-approximations-metric-spaces
+open import metric-spaces.complete-metric-spaces
+open import metric-spaces.convergent-cauchy-approximations-metric-spaces
 open import metric-spaces.extensional-premetric-structures
+open import metric-spaces.limits-of-cauchy-approximations-premetric-spaces
 open import metric-spaces.metric-spaces
 open import metric-spaces.metric-structures
 open import metric-spaces.monotonic-premetric-structures
@@ -126,14 +132,14 @@ module _
     is-short-function-Metric-Space
       ( Π-Metric-Space A P)
       ( P a)
-      ( λ f → f a)
+      ( ev a)
   is-short-ev-Π-Metric-Space ε x y H = H a
 
   short-ev-Π-Metric-Space :
     short-function-Metric-Space
       ( Π-Metric-Space A P)
       ( P a)
-  short-ev-Π-Metric-Space = (λ f → f a) , (is-short-ev-Π-Metric-Space)
+  short-ev-Π-Metric-Space = (ev a) , (is-short-ev-Π-Metric-Space)
 ```
 
 ### Dependent products of saturated metric spaces are saturated
@@ -149,3 +155,110 @@ module _
   is-saturated-Π-is-saturated-Metric-Space ε x y H a =
     Π-saturated a ε (x a) (y a) (λ d → H d a)
 ```
+
+### The partial applications of a Cauchy approximation in a dependent product metric space are Cauchy approximations
+
+```agda
+module _
+  {l l1 l2 : Level} (A : UU l) (P : A → Metric-Space l1 l2)
+  (f : cauchy-approximation-Metric-Space (Π-Metric-Space A P))
+  where
+
+  ev-cauchy-approximation-Π-Metric-Space :
+    (x : A) → cauchy-approximation-Metric-Space (P x)
+  ev-cauchy-approximation-Π-Metric-Space x =
+    map-short-function-cauchy-approximation-Metric-Space
+      ( Π-Metric-Space A P)
+      ( P x)
+      ( short-ev-Π-Metric-Space A P x)
+      ( f)
+```
+
+### A dependent map is the limit of a Cauchy approximation in a dependent product of metric spaces if and only if it is the pointwise limit of its partial applications
+
+```agda
+module _
+  {l l1 l2 : Level} (A : UU l) (P : A → Metric-Space l1 l2)
+  (f : cauchy-approximation-Metric-Space (Π-Metric-Space A P))
+  (g : type-Π-Metric-Space A P)
+  where
+
+  is-pointwise-limit-is-limit-cauchy-approximation-Π-Metric-Space :
+    is-limit-cauchy-approximation-Metric-Space
+      ( Π-Metric-Space A P)
+      ( f)
+      ( g) →
+    (x : A) →
+    is-limit-cauchy-approximation-Metric-Space
+      ( P x)
+      ( ev-cauchy-approximation-Π-Metric-Space A P f x)
+      ( g x)
+  is-pointwise-limit-is-limit-cauchy-approximation-Π-Metric-Space L x ε δ =
+    L ε δ x
+
+  is-limit-is-pointwise-limit-cauchy-approximation-Π-Metric-Space :
+    ( (x : A) →
+      is-limit-cauchy-approximation-Metric-Space
+        ( P x)
+        ( ev-cauchy-approximation-Π-Metric-Space A P f x)
+        ( g x)) →
+    is-limit-cauchy-approximation-Metric-Space
+      ( Π-Metric-Space A P)
+      ( f)
+      ( g)
+  is-limit-is-pointwise-limit-cauchy-approximation-Π-Metric-Space L ε δ x =
+    L x ε δ
+```
+
+### A product of complete metric spaces is complete
+
+```agda
+module _
+  {l l1 l2 : Level} (A : UU l) (P : A → Metric-Space l1 l2)
+  (Π-complete : (x : A) → is-complete-Metric-Space (P x))
+  where
+
+  limit-cauchy-approximation-Π-is-complete-Metric-Space :
+    cauchy-approximation-Metric-Space (Π-Metric-Space A P) →
+    type-Π-Metric-Space A P
+  limit-cauchy-approximation-Π-is-complete-Metric-Space u x =
+    limit-cauchy-approximation-Complete-Metric-Space
+      ( P x , Π-complete x)
+      ( ev-cauchy-approximation-Π-Metric-Space A P u x)
+
+  is-limit-limit-cauchy-approximation-Π-is-complete-Metric-Space :
+    (u : cauchy-approximation-Metric-Space (Π-Metric-Space A P)) →
+    is-limit-cauchy-approximation-Metric-Space
+      ( Π-Metric-Space A P)
+      ( u)
+      ( limit-cauchy-approximation-Π-is-complete-Metric-Space u)
+  is-limit-limit-cauchy-approximation-Π-is-complete-Metric-Space u ε δ x =
+    is-limit-limit-cauchy-approximation-Complete-Metric-Space
+      ( P x , Π-complete x)
+      ( ev-cauchy-approximation-Π-Metric-Space A P u x)
+      ( ε)
+      ( δ)
+
+  is-complete-Π-Metric-Space :
+    is-complete-Metric-Space (Π-Metric-Space A P)
+  is-complete-Π-Metric-Space u =
+    limit-cauchy-approximation-Π-is-complete-Metric-Space u ,
+    is-limit-limit-cauchy-approximation-Π-is-complete-Metric-Space u
+```
+
+### The complete product of complete metric spaces
+
+```agda
+module _
+  {l l1 l2 : Level} (A : UU l) (C : A → Complete-Metric-Space l1 l2)
+  where
+
+  Π-Complete-Metric-Space : Complete-Metric-Space (l ⊔ l1) (l ⊔ l2)
+  pr1 Π-Complete-Metric-Space =
+    Π-Metric-Space A (metric-space-Complete-Metric-Space ∘ C)
+  pr2 Π-Complete-Metric-Space =
+    is-complete-Π-Metric-Space
+      ( A)
+      ( metric-space-Complete-Metric-Space ∘ C)
+      ( is-complete-metric-space-Complete-Metric-Space ∘ C)
+```

src/metric-spaces/isometries-metric-spaces.lagda.md

@@ -237,7 +237,7 @@ module _
       ( λ x → refl)
 ```
 
-### Associatity of composition of isometries between metric spaces
+### Associativity of composition of isometries between metric spaces
 
 ```agda
 module _

src/metric-spaces/metric-space-of-functions-metric-spaces.lagda.md

@@ -0,0 +1,117 @@
+# The metric space of functions between metric spaces
+
+```agda
+module metric-spaces.metric-space-of-functions-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import metric-spaces.cauchy-approximations-metric-spaces
+open import metric-spaces.convergent-cauchy-approximations-metric-spaces
+open import metric-spaces.dependent-products-metric-spaces
+open import metric-spaces.functions-metric-spaces
+open import metric-spaces.isometries-metric-spaces
+open import metric-spaces.metric-spaces
+```
+
+</details>
+
+## Idea
+
+[Functions](metric-spaces.functions-metric-spaces.md) between
+[metric spaces](metric-spaces.metric-spaces.md) inherit the
+[product metric structure](metric-spaces.dependent-products-metric-spaces.md) of
+their codomain. This defines the
+{{#concept "metric space of functions between metric spaces" Agda=metric-space-of-functions-Metric-Space}}.
+
+## Definitions
+
+### The metric space of functions between metric spaces
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space l1 l2) (B : Metric-Space l1' l2')
+  where
+
+  metric-space-of-functions-Metric-Space : Metric-Space (l1 ⊔ l1') (l1 ⊔ l2')
+  metric-space-of-functions-Metric-Space =
+    Π-Metric-Space (type-Metric-Space A) (λ _ → B)
+```
+
+## Properties
+
+### The partial applications of a Cauchy approximation of functions form a Cauchy approximation
+
+```agda
+module _
+  { l1 l2 l1' l2' : Level}
+  ( A : Metric-Space l1 l2) (B : Metric-Space l1' l2')
+  ( f :
+    cauchy-approximation-Metric-Space
+      ( metric-space-of-functions-Metric-Space A B))
+  ( x : type-Metric-Space A)
+  where
+
+  ev-cauchy-approximation-function-Metric-Space :
+    cauchy-approximation-Metric-Space B
+  ev-cauchy-approximation-function-Metric-Space =
+    ev-cauchy-approximation-Π-Metric-Space
+      ( type-Metric-Space A)
+      ( λ _ → B)
+      ( f)
+      ( x)
+```
+
+### A function is the limit of a Cauchy approximation of functions if and only if it is the pointwise limit of its partial applications
+
+```agda
+module _
+  { l1 l2 l1' l2' : Level}
+  ( A : Metric-Space l1 l2) (B : Metric-Space l1' l2')
+  ( f :
+    cauchy-approximation-Metric-Space
+      ( metric-space-of-functions-Metric-Space A B))
+  ( g : map-type-Metric-Space A B)
+  where
+
+  is-pointwise-limit-is-limit-cauchy-approximation-function-Metric-Space :
+    is-limit-cauchy-approximation-Metric-Space
+      ( metric-space-of-functions-Metric-Space A B)
+      ( f)
+      ( g) →
+    (x : type-Metric-Space A) →
+    is-limit-cauchy-approximation-Metric-Space
+      ( B)
+      ( ev-cauchy-approximation-function-Metric-Space A B f x)
+      ( g x)
+  is-pointwise-limit-is-limit-cauchy-approximation-function-Metric-Space =
+    is-pointwise-limit-is-limit-cauchy-approximation-Π-Metric-Space
+      ( type-Metric-Space A)
+      ( λ _ → B)
+      ( f)
+      ( g)
+
+  is-limit-is-pointwise-limit-cauchy-approximation-function-Metric-Space :
+    ( (x : type-Metric-Space A) →
+      is-limit-cauchy-approximation-Metric-Space
+        ( B)
+        ( ev-cauchy-approximation-function-Metric-Space A B f x)
+        ( g x)) →
+    is-limit-cauchy-approximation-Metric-Space
+      ( metric-space-of-functions-Metric-Space A B)
+      ( f)
+      ( g)
+  is-limit-is-pointwise-limit-cauchy-approximation-function-Metric-Space =
+    is-limit-is-pointwise-limit-cauchy-approximation-Π-Metric-Space
+      ( type-Metric-Space A)
+      ( λ _ → B)
+      ( f)
+      ( g)
+```

src/metric-spaces/metric-space-of-isometries-metric-spaces.lagda.md

@@ -0,0 +1,45 @@
+# The metric space of isometries between metric spaces
+
+```agda
+module metric-spaces.metric-space-of-isometries-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import metric-spaces.isometries-metric-spaces
+open import metric-spaces.metric-space-of-functions-metric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.subspaces-metric-spaces
+```
+
+</details>
+
+## Idea
+
+[Isometries](metric-spaces.isometries-metric-spaces.md) between
+[metric spaces](metric-spaces.metric-spaces.md) inherit the
+[metric subspace](metric-spaces.subspaces-metric-spaces.md) structure of the
+[function metric space](metric-spaces.metric-space-of-functions-metric-spaces.md).
+This defines the
+{{#concept "metric space of isometries between metric spaces" Agda=metric-space-of-isometries-Metric-Space}}.
+
+## Definitions
+
+### The metric space of isometries between metric spaces
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space l1 l2) (B : Metric-Space l1' l2')
+  where
+
+  metric-space-of-isometries-Metric-Space :
+    Metric-Space (l1 ⊔ l2 ⊔ l1' ⊔ l2') (l1 ⊔ l2')
+  metric-space-of-isometries-Metric-Space =
+    subspace-Metric-Space
+      ( metric-space-of-functions-Metric-Space A B)
+      ( is-isometry-prop-Metric-Space A B)
+```

src/metric-spaces/metric-space-of-short-functions-metric-spaces.lagda.md

@@ -0,0 +1,45 @@
+# The metric space of short functions between metric spaces
+
+```agda
+module metric-spaces.metric-space-of-short-functions-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import metric-spaces.metric-space-of-functions-metric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.short-functions-metric-spaces
+open import metric-spaces.subspaces-metric-spaces
+```
+
+</details>
+
+## Idea
+
+[Short functions](metric-spaces.short-functions-metric-spaces.md) between
+[metric spaces](metric-spaces.metric-spaces.md) inherit the
+[metric subspace](metric-spaces.subspaces-metric-spaces.md) structure of the
+[function metric space](metric-spaces.metric-space-of-functions-metric-spaces.md).
+This defines the
+{{#concept "metric space of short functions between metric spaces" Agda=metric-space-of-short-functions-Metric-Space}}.
+
+## Definitions
+
+### The metric space of short functions between metric spaces
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space l1 l2) (B : Metric-Space l1' l2')
+  where
+
+  metric-space-of-short-functions-Metric-Space :
+    Metric-Space (l1 ⊔ l2 ⊔ l1' ⊔ l2') (l1 ⊔ l2')
+  metric-space-of-short-functions-Metric-Space =
+    subspace-Metric-Space
+      ( metric-space-of-functions-Metric-Space A B)
+      ( is-short-function-prop-Metric-Space A B)
+```