large premetric spaces

[malarbol]

[malarbol]

There's still a lot to do but is it the kind of things you had in mind @fredrik-bakke ? This also serves as suggestions for renaming/removing things of standard metric spaces (e.g. rename Premetric to Rational-Neighborhood, remove Pseudometric-Space and only keep premetric and metric spaces etc.

[fredrik-bakke]

This looks great!

[fredrik-bakke]

Maybe call it a rational neighborhood relation or rational neighborhood structure?

[fredrik-bakke]

We also should'nt have inconsistent naming between the small and large setup though, but Im okay with leaving the second renaming for a second pr, to slice things up

[fredrik-bakke]

And then a (old) premetric space is Type-With-Rational-Neighborhoods

[malarbol]

We also should'nt have inconsistent naming between the small and large setup though,

of course! But instead of rewriting the small setup directly I thought I could try to write the large setup with the new naming scheme, until we all agree, and then adapt the small setup to the new names.

but Im okay with leaving the second renaming for a second pr, to slice things up

yeah, this mass renaming has me a bit concerned. I guess we could do it in parallel PRs and merge them when they're both ready.

[malarbol]

And then a (old) premetric space is Type-With-Rational-Neighborhoods

TBH I'm not a big fan of this name. It's like calling a magma a "Type-With-Binary-Operation"; it's descriptive, but it's not a name, it's a description. I think we could actually do without, e.g.

• Rational-Neighborhood-Relation;
• Premetric-Structure (Rational-Neighborhood-Relation with some properties);
• Premetric-Space (type with a Premetric-Structure);
• Metric-Space (Premetric-Space with some properties).