Cauchy precompletions of pseudometric spaces

[malarbol]

This PR introduces the following concepts:

• metric extensions of pseudometric spaces: a metric space with an isometry from the pseudometric space into it;
• complete metric extensions of pseudometric spaces: metric extensions where the target space is complete;
• Cauchy dense metric extensions of pseudometric spaces: metric extensions where all the points of the target space are limits of images of Cauchy approximations in the pseudometric space;
• Cauchy precompletions of pseudometric spaces: the metric quotient of the Cauchy pseudocompletion of the pseudometric space.

The Cauchy precompletion of a pseudometric space is Cauchy dense and any metric extension into a complete metric
space factors through its Cauchy precompletion.

[malarbol]

This is my follow up on #1458. As I commented before, this Cauchy precompletion is the closest to a Cauchy completion I could get.
There's still room to define the Cauchy completion as a metric extension that is both complete and Cauchy dense and I believe any such metric space should be isometrically equivalent to the Cauchy precompletion, but I haven't worked it all yet.

[fredrik-bakke]

Suggested change

	map-isometry-cauchy-approximation-Pseudometric-Space :
	map-cauchy-approximation-isometry-Pseudometric-Space :

[malarbol]

Re-drafting this PR to split in and formalize a few results about metric extensions before talking about Cauchy precompletions. And maybe rework a bit the construction of metric-quotients-of-pseudometric-spaces: I think the construction there can be seen as the initial metric extension of a pseudometric space which corresponds to universal property I was looking for. Similarly, the Cauchy precompletion seems to play a special role among metric extensions of a given pseudometric space.