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.