Cauchy pseudocompletions of (pseudo)metric spaces (#1619)

This PR introduces the following concepts:

- the **Cauchy pseudocompletion** of a pseudometric space `M`: the
pseudometric space of Cauchy approximations in `M` where two Cauchy
approximations `x` and `y` are in a `d`-neighborhood of one another if
for all `δ ε : ℚ⁺`, `x δ` and `y ε` are in a `δ + ε + d`-neighborhood of
one another in `M`;

- the **Cauchy pseudocompletion** of a metric space: the Cauchy
pseudocompletion of its underlying pseudometric space.

Cauchy approximations in a Cauchy pseudocompletion have a limit; any
complete metric space is a retract of its Cauchy pseudocompletion.

Co-authored-by: Louis Wasserman <wasserman.louis@gmail.com>

Author: malarbol

src/metric-spaces.lagda.md

@@ -64,6 +64,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-pseudometric-spaces public
+open import metric-spaces.cauchy-pseudocompletion-of-metric-spaces public
+open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-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-subsets-located-metric-spaces public