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.

[malarbol]

I started a review the other day and then forgot to post my comments. Here they are anyways 😅

funny story: I've been answering your questions for days, or asked for direction and such, but instead of commenting I had apparently "Started a review" that I never committed... so all these comments never got to be published 🙃 .

Thanks a lot for you review. I'll try to address all these as soon as possible and answer the remaining pending questions.

[fredrik-bakke]

I did it! I got through the whole PR!

[fredrik-bakke]

You're so close to done!

[fredrik-bakke]

Hey! Im on my phone and can't find the right comment, but regarding "being isometric" vs. "being an isometry". I wonder if the issue is that when one says that "something is isometric", rather than, say, an "isometric equivalence". The word is understood as "isometric in relation to some other object". So I will concede you can say "my equivalence is an isometric equivalence", but I am very unsure if you should say "my equivalence is isometric".

[fredrik-bakke]

Maybe a better conjugation is to say "my equivalence is isometrical"?

[fredrik-bakke]

We should definitely find an English language reference for this

[fredrik-bakke]

So, I didn't find a good reference on the distinction between "-ic" and "-ical" endings online in the context of math, so I asked an LLM for their input, and here is what it had to say. I'll let you decide based on what you judge from it.

The distinction between the -ic and -ical suffixes can indeed be subtle, but it often relates to the difference between a property in the abstract (-ic) versus the broader context or structure in which that property is involved (-ical). Let's delve into the specific examples you're interested in, focusing on homotopy and isometry.

Homotopy: "Homotopic" vs. "Homotopical"

• Homotopic: This term is generally used to describe a relationship between two objects, specifically in the context of homotopy. For instance, two maps ( f ) and ( g ) are homotopic if there exists a homotopy between them. The word refers to the specific condition of "being homotopic" to something else. It's more of a relational term.

• Homotopical: On the other hand, homotopical is used when something pertains to homotopy theory or involves homotopy concepts in a broader sense. When we describe something as homotopical, like a homotopical functor, we're referring to it as related to the general framework of homotopy, without needing to specify a homotopy relation between two objects. It indicates that the functor behaves in a way compatible with homotopy theory.

Isometry: "Isometric" vs. "Isometrical"

• Isometric: Similar to homotopic, isometric is the more concrete term. It refers to objects (such as spaces, maps, or transformations) that preserve distances. For example, two spaces are isometric if there exists an isometry (a distance-preserving map) between them. It’s a specific condition of having or preserving a property related to isometries.

• Isometrical: This term is not used as commonly, but if it were, it would follow the same pattern as homotopical. It would refer to something pertaining to or structured around the concept of isometry in a broader sense. For instance, an isometrical transformation could refer to a class of transformations that preserve distance, but it doesn’t necessarily specify a direct isometry between two particular objects.

General Pattern

In general:

• -ic tends to indicate a specific relationship or property (as in homotopic or isometric).
• -ical indicates a broader conceptual or theoretical context (as in homotopical or, potentially, isometrical).

For your examples, this explains why you would say that a functor is homotopical (because it participates in or respects the structure of homotopy theory) but only homotopic if it is specifically homotopic to another functor. The same reasoning could be extended to isometries, though "isometrical" is much less common. You’re more likely to encounter "isometric" than "isometrical," since the concept of isometry is often used in a very direct sense.

[fredrik-bakke]

I pushed a suggestion for an introductory section to metric spaces. I'd like it to mention why one should care about metric spaces and maybe some interesting properties of them, but I don't know what to say about that right now.

[fredrik-bakke]

I haven't done a final read-through, but I think this PR is safe to merge. When you give the go-ahead I'll merge it

[fredrik-bakke]

I don't think you should call the locality property that for pseudometrics, btw. It is really extensionality of pseudometrics, while locality is more of a technical condition that happens to coincide with extensionality for pseudometrics.

[fredrik-bakke]

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:

• it is descriptive and intuitive
• it signalizes that the concept is less structured, in contrast to "premetric"
• it gives the concept, which is very distinct from pseudometrics and metrics, a name that is also more distinct from them.
• it avoids the misinterpretation that "metrics are premetrics which are extensional"

Regarding Premetric-Space, an appropriate name would be Type-With-Neighborhoods, again signalizing that there may not be any coherence between the type and the neighborhoods, in contrast to the former.

[fredrik-bakke]

Saying that a neighborhood relation is a premetric is like saying a binary relation on a type is a preorder structure

[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:

• it is descriptive and intuitive
• it signalizes that the concept is less structured, in contrast to "premetric"
• it gives the concept, which is very distinct from pseudometrics and metrics, a name that is also more distinct from them.
• it avoids the misinterpretation that "metrics are premetrics which are extensional"

Regarding Premetric-Space, an appropriate name would be Type-With-Neighborhoods, again signalizing that there may not be any coherence between the type and the neighborhoods, in contrast to the former.

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).

[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!