Universal property of Cauchy pseudocompletions and short maps of pseudometric spaces (#1818)

This PR introduces the concept of **precomplete** short maps `f : P → M`
from a pseudometric space in a metric space: short maps such that for
all Cauchy approximation `u : C P`, `Cf u` is convergent in `M`.
Precomplete short maps extend along the unit map of Cauchy
pseudocompletions `κ : P → C P`: if `f` is precomplete, there exists
some `g : C P → M` such that `f ~ g ∘ κ`.

Then, we prove the universal property of Cauchy pseudocompletions of
pseudometric spaces w.r.t. short maps to metric spaces:

Given a metric space `M` and a pseudometric space `P`, precomposition
with the unit map of Cauchy pseudocompletions `κ : P → C P` maps short
maps `g : C P → M` to short maps `g ∘ κ : P → M`. For any Cauchy
approximation `u : C P`, its pointwise image `C(g ∘ κ) u : C M`
converges to `g u` so `g` is determined by its restriction to `P`, `g ∘
κ`, which is precomplete. Therefore, extensions of short maps `f : P →
M` along the unit map of Cauchy pseudocompletions `κ : P → C P` are
unique and exist iff `f` is **precomplete**.

In particular, a metric space `M` is _complete_ if and only if the unit
map `κ : M → C M` has a short retraction, i.e. a short map `lim : C M →
M` such that `lim ∘ κ ~ id`.

Author: malarbol

src/metric-spaces.lagda.md

@@ -163,6 +163,7 @@ open import metric-spaces.poset-of-rational-neighborhood-relations public
 open import metric-spaces.precategory-of-metric-spaces-and-isometries public
 open import metric-spaces.precategory-of-metric-spaces-and-maps public
 open import metric-spaces.precategory-of-metric-spaces-and-short-maps public
+open import metric-spaces.precomplete-short-maps-pseudometric-spaces public
 open import metric-spaces.preimages-rational-neighborhood-relations public
 open import metric-spaces.pseudometric-spaces public
 open import metric-spaces.rational-approximations-of-zero public
@@ -186,6 +187,7 @@ open import metric-spaces.uniform-limit-theorem-uniformly-continuous-maps-metric
 open import metric-spaces.uniformly-continuous-maps-metric-spaces public
 open import metric-spaces.unit-map-metric-quotients-of-pseudometric-spaces public
 open import metric-spaces.universal-property-isometries-metric-quotients-of-pseudometric-spaces public
+open import metric-spaces.universal-property-short-maps-cauchy-pseudocompletions-of-pseudometric-spaces public
 open import metric-spaces.universal-property-short-maps-metric-quotients-of-pseudometric-spaces public
 ```
 

src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md

@@ -110,11 +110,19 @@ module _
 
 ```agda
 module _
-  { l1 l2 : Level} (A : Metric-Space l1 l2)
-  { f g : cauchy-approximation-Metric-Space A}
-  ( f~g :
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  (f g : cauchy-approximation-Metric-Space A)
+  where
+
+  htpy-map-cauchy-approximation-Metric-Space : UU l1
+  htpy-map-cauchy-approximation-Metric-Space =
     map-cauchy-approximation-Metric-Space A f ~
-    map-cauchy-approximation-Metric-Space A g)
+    map-cauchy-approximation-Metric-Space A g
+
+module _
+  {l1 l2 : Level} (A : Metric-Space l1 l2)
+  {f g : cauchy-approximation-Metric-Space A}
+  (f~g : htpy-map-cauchy-approximation-Metric-Space A f g)
   where
 
   eq-htpy-cauchy-approximation-Metric-Space : f ＝ g

src/metric-spaces/cauchy-approximations-pseudometric-spaces.lagda.md

@@ -108,14 +108,23 @@ module _
 
 ```agda
 module _
-  { l1 l2 : Level} (A : Pseudometric-Space l1 l2)
-  { f g : cauchy-approximation-Pseudometric-Space A}
-  ( f~g :
+  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
+  (f g : cauchy-approximation-Pseudometric-Space A)
+  where
+
+  htpy-map-cauchy-approximation-Pseudometric-Space : UU l1
+  htpy-map-cauchy-approximation-Pseudometric-Space =
     map-cauchy-approximation-Pseudometric-Space A f ~
-    map-cauchy-approximation-Pseudometric-Space A g)
+    map-cauchy-approximation-Pseudometric-Space A g
+
+module _
+  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
+  {f g : cauchy-approximation-Pseudometric-Space A}
+  (f~g : htpy-map-cauchy-approximation-Pseudometric-Space A f g)
   where
 
-  eq-htpy-cauchy-approximation-Pseudometric-Space : f ＝ g
+  eq-htpy-cauchy-approximation-Pseudometric-Space :
+    f ＝ g
   eq-htpy-cauchy-approximation-Pseudometric-Space =
     eq-type-subtype
       ( is-cauchy-approximation-prop-Pseudometric-Space A)