Metric extensions of pseudometric spaces

[malarbol]

This PR introduces the concept of metric extension of pseudometric spaces: a metric space with an isometry from the pseudometric space into it.

[fredrik-bakke]

Thank you for splitting up your other PR unprompted! It was a bit daunting to begin reviewing it 😅

[fredrik-bakke]

Overall the naming choices and structuring of your code is very good. I can see that you've taken extra care to comply with library guidelines this time around, thank you for spending the extra effort on that!

[fredrik-bakke]

I realize it is not clear how to extend this to metric extensions of metric spaces, wouldn't that be called the same thing? Perhaps Metric-Extension-Of-Pseudometric-Space is better?

[fredrik-bakke]

oh, that would be called extension-Metric-Space, or Extension-Metric-Space I presume

[fredrik-bakke]

then perhaps the better name to use here is Metric-Extension-Pseudometric-Space?

[malarbol]

then perhaps the better name to use here is Metric-Extension-Pseudometric-Space?

I was afraid we might come to this but I find this name too long and verbose.

I think to extend this to metric extensions of metric spaces, extension-Metric-Space would be better; we're staying in the realm of metric spaces unlike the case introduced here. Moreover, metric spaces and isometries form a category so the same construction between metric spaces could also be understood as a coslice in this category (modulo Level problems) so this might as well be called coslice-isometry-Metric-Space. Either way, I don't think Metric-Extension-Metric-Space would be a good name, and neither Metric-Extension-Pseudometric-Space.

Now, this would not be the first time I'm wrong about names. If you really think Metric-Extension-Pseudometric-Space and Metric-Extension-Metric-Space are better, I'll abide.

[malarbol]

The more I work with the concept (see #1726 or #1729) the more it feels like a new namespace between Pseudometric-Space and Metric-Space instead of something that should be declined as Metric-Extension-Pseudometric-Space and Metric-Extension-Metric-Space. I'm not sure how the name should extend to metric extensions of metric spaces but neither I am that we really need to.

[malarbol]

Maybe this file should be called isometries-metric-extensions.lagda.md to follow the names of isometries-metric-spaces.lagda.md and isometries-pseudometric-spaces.lagda.md, etc. Then we'd have "the category of metric extensions and isometries" and stuff like that.

[malarbol]

Or maybe the type Metric-Extension is wrong and the definition should be

module _
  {l1 l2 l3 l4 : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l3 l4)
  where

  Metric-Extension : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  Metric-Extension =
    isometry-Pseudometric-Space P (pseudometric-Metric-Space M)

and then consider the types Metric-Extension P for a given (P : Pseudometric-Space l1 l2), etc.?

[malarbol]

I think my suggestion of #1724 (comment) is actually better. I'm closing this PR and try this new way.