Metric spaces

[malarbol]

This PR introduces the concept of metric spaces.

We introduce a new module metric-spaces with the following submodules:

Premetric spaces

• premetric-structures: premetric structures on a type and basic properties;
• reflexive-premetric-structures;
• symmetric-premetric-structures;
• monotonic-premetric-structures: premetrics with upper-stable neighborhoods;
• triangular-premetric-structures: premetrics that satisfy a triangular inequality;
• extensional-premetric-structures: premetrics here indistinguishability characterizes equality;
• closed-premetric-structures: premetrics with closed neighborhoods;
• discrete-premetric-structures: premetric structure defined by mere equality;
• induced-premetric-structures-on-preimages: premetric induced on the domain of a map by a premetric on its codomain;
• ordering-premetric-structures: a partial ordering on the premetric structures on a type;
• premetric-spaces: types equipped with a premetric structure;
• short-functions-premetric-spaces: functions between premetric spaces that preserve neighborhoods;
• isometries-premetric-spaces: functions between premetric spaces that identify neighborhoods;
• equality-of-premetric-spaces: identity principle for the type of premetric spaces;
• invertible-isometries-premetric-spaces: another characterization of equality of premetric spaces;
• isometric-equivalences-premetric-spaces: another characterization of equality of premetric spaces;
• cauchy-approximations-premetric-spaces: the type of Cauchy approximations in a premetric space;
• limits-of-cauchy-approximations-in-premetric-spaces;

Pseudometric spaces

• pseudometric-structures: reflexive, symmetric, and triangular premetrics;
• pseudometric-spaces: types equipped with a pseudometric structure;

Metric spaces

• metric-structures: reflexive, symmetric, triangular, and local premetrics;
• metric-spaces: types equipped with a metric structure;
• saturated-metric-spaces: metric spaces with closed premetrics;
• subspaces-metric-spaces: metric structure induced on subsets of metric spaces;
• dependent-products-metric-spaces: metric structure on dependent families of metric spaces;
• functions-metric-spaces: functions between carrier types of metric spaces;
• short-functions-metric-spaces: short functions between the underlying premetric spaces of metric spaces;
• isometries-metric-spaces: isometries between the underlying premetric spaces of metric spaces;
• equality-of-metric-spaces: identity principle in the type of metric spaces;
• cauchy-approximations-metric-spaces: the type of Cauchy approximations in a metric space;
• convergent-cauchy-approximations-metric-spaces: the type of convergent Cauchy approximations in a metric space;
• complete-metric-spaces: the type of metric spaces where all Cauchy approximations are convergent;

Example of metric spaces

• metric-space-of-cauchy-approximations-in-a-metric-space;
• metric-space-of-convergent-cauchy-approximations-in-a-metric-space;
• metric-space-of-rational-numbers;
• metric-space-of-rational-numbers-with-open-neighborhoods;

Categories of metric spaces and functors between them

• precategory-of-metric-spaces-and-functions;
• precategory-of-metric-spaces-and-isometries;
• precategory-of-metric-spaces-and-short-functions;
• category-of-metric-spaces-and-isometries;
• category-of-metric-spaces-and-short-functions;
• functor-category-set-functions-isometry-metric-spaces;
• functor-category-short-isometry-metric-spaces.

We also introduce the standard metric structure on the real numbers in
real-numbers.metric-space-of-real-numbers and a few miscellaneous lemmas in
elementary-number-theory and foundation.

[fredrik-bakke]

ok. Give me some time to think of a new name scheme and I'll come back to you with suggestions, before making any drastic changes this time. (sorry for the mess about isometry/isometric, I think I hadn't really understood what you wanted).

I realized I hadn't been entirely clear in what I meant, so I figured it would be easier to just implement what I meant myself.

[malarbol]

I still believe premetric structures is a terrible name for that concept, and would again like to lobby for changing it. I believe the term neighborhood relation is much more fitting for a couple of reasons:

I'm starting to think it's not a good concept at all (at least for this module), and that we should only consider neighborhood relations that are reflexive, monotonic families $\mathbb{Q}^{+} \rightarrow M \rightarrow M \rightarrow Prop~l$.

reflexivity and monotonicity are the basic properties that fit the distance/neighborhood interpretation:

• any point is a neighbor of itself
• enlarging neighborhoods doesn't forget neighbors

Reflexivity is used for almost all interesting properties of "premetrics", and gives a minimal notion of coherence between the neighborhood structure to the carrier type (making it a real structure more than just a "decorator"). Monotonicity is also used a lot; and adding it kind of justifies the use of $\mathbb{Q}^{+}$ instead of just any families $X \rightarrow M \rightarrow M \rightarrow Prop~l$: we want the type family of relations to also be "structured by $\mathbb{Q}^{+}$" to be called a neighborhood relation.

Then Neighborhood-Space would be type of "type equipped with a neighborhood structure" and the other structures would be substructures of this one. We could rename pseudometric spaces to premetric spaces (maybe explaining why we disagree with wikipedia) and metric space would now be "extensional premetric spaces" as they always should have.

[malarbol]

And I wonder if we should include "symmetry" in the definition of neighborhood relation too. It's also useful for many interesting properties, and, as mentioned before, there's a canonical "symmetrization" of a neighborhood relation, characterized as the minimal symmetric neighborhood relation coarser that it (just define B' d x y = product-Prop (B d x y) (B d y x)) and the "symmetrization" acts functorially on isometries, short maps, and such.

It looks like you can actually do something similar with reflexivity (define B' d x y = (trunc-Prop (x ＝ y)) ∨ B d x y) and for monotonicity (define B' d x y = ∃ ℚ⁺ (λ r → product-Prop (leq-prop-ℚ⁺ r d) (B r x y))) so we might as well just assume them all from the beginning.

[malarbol]

non-reflexive or non-monotonic families of relations are probably interesting too, but maybe not in the metric-spaces module.

[fredrik-bakke]

Hmm, does Auke not prove anything useful/interesting about premetrics in his thesis?

[fredrik-bakke]

reflexivity and monotonicity are the basic properties that fit the distance/neighborhood interpretation:

• any point is a neighbor of itself
• enlarging neighborhoods doesn't forget neighbors

Sounds like you like filters :)

[fredrik-bakke]

And I wonder if we should include "symmetry" in the definition of neighborhood relation too. It's also useful for many interesting properties, and, as mentioned before, there's a canonical "symmetrization" of a neighborhood relation, characterized as the minimal symmetric neighborhood relation coarser that it (just define B' d x y = (B d x y) ∨ (B d y x)) and the "symmetrization" acts functorially on isometries, short maps, and such.

It looks like you can actually do something similar with reflexivity (define B' d x y = (trunc-Prop (x ＝ y)) ∨ B d x y) and for monotonicity (define B' d x y = ∃ ℚ⁺ (λ r → product-Prop (leq-prop-ℚ⁺ r d) (B r x y))) so we might as well just assume them all from the beginning.

This sounds like a good argument for disregarding premetrics, yes. You could provide a series of modules that, given a neighborhood relation in the end give the universal pseudometric, and then after that always operate with pseudometrics.

EDIT: This depends a bit on whether the theory has applications to things that don't satisfy all of these properties, though.

[fredrik-bakke]

We could rename pseudometric spaces to premetric spaces (maybe explaining why we disagree with wikipedia) and metric space would now be "extensional premetric spaces" as they always should have.

I'm a bit hesitant to agree with this suggestion. "Pseudometric" seems to be pretty widely used. And "premetric" is at times used for weaker concepts than pseudometrics evidently.

[malarbol]

We could rename pseudometric spaces to premetric spaces (maybe explaining why we disagree with wikipedia) and metric space would now be "extensional premetric spaces" as they always should have.

I'm a bit hesitant to agree with this suggestion. "Pseudometric" seems to be pretty widely used. And "premetric" is at times used for weaker concepts than pseudometrics evidently.

Ok, I probably went too far. So maybe nothing could be called a premetric space for now, since there's no real consensus on what it should mean?

[malarbol]

Hmm, does Auke not prove anything useful/interesting about premetrics in his thesis?

It's mostly about real numbers, so the standard premetrics on $\mathbb{Q}$, $\mathbb{R}$, Cauchy structures, etc. I don't know if there are results on generic premetrics. They does mention the following (p.81-82):

Note the outright lack of natural conditions one might put on∼: our premetric spaces
are a very wild notion. In fact, having few conditions here is a good thing, as any conditions
introduced now would need to be respected later by the induction principle in Definition 4.5.12,
thus making that induction principle harder to use.

but I'm not sure what to make of it.

[malarbol]

it's also related to what Martín Escardó calls generalized-metric-space (here, with $R = (\mathbb{Q}^{+} \rightarrow Prop~l)$ ).

I don't know if it can help us. Like maybe I should write things on generalized-metric-space and then apply them to the case $(\mathbb{Q}^{+} \rightarrow Prop~l)$ ?

[malarbol]

and here: https://www.researchgate.net/publication/343732184_Completion_of_premetric_spaces/fulltext/5f3c92fc92851cd302037f27/Completion-of-premetric-spaces.pdf they call premetric space what I call a saturated metric space, which doesn't really help neither.

[malarbol]

and here: https://www.researchgate.net/publication/343732184_Completion_of_premetric_spaces/fulltext/5f3c92fc92851cd302037f27/Completion-of-premetric-spaces.pdf they call premetric space what I call a saturated metric space, which doesn't really help neither.

and, BTW, they also call our isometries, isometric embeddings and reserve the term isometry for isometric equivalences. Should we rename our isometries, isometric-map-Metric-Space?

[fredrik-bakke]

it's also related to what Martín Escardó calls generalized-metric-space (here, with R = ( Q + → P r o p   l ) ).

I don't know if it can help us. Like maybe I should write things on generalized-metric-space and then apply them to the case ( Q + → P r o p   l ) ?

At that point I don't see why you wouldn't use some other even more general concept like filters instead of "metrics" in a generalized sense. You have to decide what your fundament for study is at some point. Unless you give a good reason why you want to generalize the concept right now, I don't see a reason to do this.

[fredrik-bakke]

and here: https://www.researchgate.net/publication/343732184_Completion_of_premetric_spaces/fulltext/5f3c92fc92851cd302037f27/Completion-of-premetric-spaces.pdf they call premetric space what I call a saturated metric space, which doesn't really help neither.

I think we can safely establish that "premetric" is both a bad term and an overloaded one. Again, we should conclude that we shouldn't use the term

[fredrik-bakke]

and here: https://www.researchgate.net/publication/343732184_Completion_of_premetric_spaces/fulltext/5f3c92fc92851cd302037f27/Completion-of-premetric-spaces.pdf they call premetric space what I call a saturated metric space, which doesn't really help neither.

and, BTW, they also call our isometries, isometric embeddings and reserve the term isometry for isometric equivalences. Should we rename our isometries, isometric-map-Metric-Space?

You're talking about a paper with 0 citations. I see no reason to make an effort to make our terminology cohere with theirs

[fredrik-bakke]

I just wanted to get this PR merged with a simple naming change for premetrics. I don't understand why we have to reconsider the basis of the contribution so late in the review process

[malarbol]

I just wanted to get this PR merged with a simple naming change for premetrics. I don't understand why we have to reconsider the basis of the contribution so late in the review process

I'm really sorry. I think I got some last-minute doubts about my contribution. As I said some other times, I don't wan't to contaminate the library with some bad concepts, abstractions, etc. We'll fix these name problems and get it merged.

I realized I hadn't been entirely clear in what I meant, so I figured it would be easier to just implement what I meant myself.

have you started working on new names for Neighborhood-Relation, Type-With-Neighborhoods, etc. or do you want me to give it a try?

[malarbol]

This sounds like a good argument for disregarding premetrics, yes. You could provide a series of modules that, given a neighborhood relation in the end give the universal pseudometric, and then after that always operate with pseudometrics.

EDIT: This depends a bit on whether the theory has applications to things that don't satisfy all of these properties, though.

I'll definitely give it some thoughts but I won't include anything more in this PR.

[EgbertRijke]

Hi! I just had a quick glance at your pull request, in particular at the file about premetric structures. Let me note that:

• The concept seems sensible: It predicates whether two elements are at most the distance of a given positive rational number apart. I'm happy to have it included in the library.
• As I understand it, there is some debate about whether to use the name "premetric" for this concept. Fredrik has a point that it is not a generally accepted name for this concept, and the article that was cited isn't referenced. I agree with this, but I am in favor of keeping the name "premetric" for now.
• I am extremely grateful to see some developments in this direction. It is very important for agda-unimath to have a development in this direction. When writing infrastructure for a new area of mathematics, it should not be expected that we get it 100% right at the first time. The metric spaces formalization will get better over time, with more people using it. So I am not worried that there is a notion of premetric in this PR, and don't think the PR should be held up because of it.

Thank you so much for this huge contribution, and for all your time and effort that went into this. This is a very worthwhile pull request that opens a new direction of formalization for agda-unimath. If you are happy with it, let's merge it.

Thanks also to @fredrik-bakke for his extensive reviewing!

[fredrik-bakke]

have you started working on new names for Neighborhood-Relation, Type-With-Neighborhoods, etc. or do you want me to give it a try?

I don't see anything wrong with these names. But I also agree with Egbert that it is time to merge this PR - sooner rather than later.

[fredrik-bakke]

As I understand it, there is some debate about whether to use the name "premetric" for this concept. Fredrik has a point that it is not a generally accepted name for this concept, and the article that was cited isn't referenced. I agree with this, but I am in favor of keeping the name "premetric" for now.

To my understanding we all agree there should be a better name for this concept. As Francois points out, the cited article uses "premetric" to mean something else

[fredrik-bakke]

I also concur with Egbert that this is a contribution of very high quality that will indeed improve the overall quality of the library.

[malarbol]

Thanks a lot for your kind comments.

I don't see anything wrong with these names. But I also agree with Egbert that it is time to merge this PR - sooner rather than later.

I think I mixed-up some comments and, for some moment, I thought you had also started to implement this new name scheme (your comment was actually about isometry/isometric).

If you are ok with it, we can merge it as it is now, and open a new issue where we could discuss better names.

[fredrik-bakke]

Very good! Since every conversation has been resolved, let's merge this PR. Further changes can be considered in a subsequent PR. Thanks again for this huge contribution!