Cauchy metric extensions of pseudometric spaces

[malarbol]

Built on top of #1726.

This PR introduces the concept of Cauchy metric extensions of a pseudometric spaces: metric extensions f : P → M such that there exists some g : C P → M satisfying

  g ∘ κ ~ f

where C P is the cauchy pseudocompletion of P and κ : P → C P the natural isometry of cauchy pseudocompletions.

Any such g is unique and Cauchy metric extensions are equivalent to metric extensions of Cauchy pseudocompletions.