Refactor metric spaces #1450
Refactor metric spaces #1450
Conversation
…ions is an isometric equivalence
…y approximations (constant cauchy approximations)
| ( Eq-map-inv-eq-tr-Rational-Neighborhood-Relation B e S) | ||
| ``` | ||
|
|
||
| ### The similarity relation induced by a rational neighborhood relation |
There was a problem hiding this comment.
I'm not sure I feel a great need to define this for arbitrary rational neighborhood relations, as opposed to pseudometric spaces, where Wikipedia gives it a name: the metric identification. (We also can skip the "both-sidedness" equivalence there.)
There was a problem hiding this comment.
I'm not sure I feel a great need to define this for arbitrary rational neighborhood relations,
this is the "present reference" of the "future reference" mentioned in #1421 (comment).
This seems to be the natural equivalence relation to consider, w.r.t. the structure induced by rational neighborhoods relations.
as opposed to pseudometric spaces, where Wikipedia gives it a name: the [metric identification]> (https://en.wikipedia.org/wiki/Pseudometric_space#Metric_identification). (We also can skip the "both-sidedness" equivalence there.)
It would be weird to call this the metric identification without actually constructing the metric quotient. I guess there could be another module metric-identification-pseudometric-spaces, referencing to this wikipedia page, where we construct the metric quotient of a pseudometric space under the metric identification.
I think it would fit better in another PR; I don't want to include too many new result in this one, this is only supposed to be a refactoring of the current metric-sapaces module, hopefully making future results, like this one, easier to formalize.
src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md
Outdated
Show resolved
Hide resolved
src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md
Outdated
Show resolved
Hide resolved
| ``` | ||
|
|
||
| ### The type of metric spaces | ||
|
|
||
| ```agda | ||
| Metric-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) | ||
| Metric-Space l1 l2 = | ||
| type-subtype (is-metric-prop-Premetric-Space {l1} {l2}) | ||
| Σ (UU l1) (Metric-Structure l2) |
There was a problem hiding this comment.
I have mixed feelings about whether we should do it this way, or if we should just actually define a metric space as an extensional pseudometric space, i.e. a Pseudometric-Space with an extensionality rule.
There was a problem hiding this comment.
I have mixed feelings about whether we should do it this way, or if we should just actually define a metric space as an extensional pseudometric space, i.e. a Pseudometric-Space with an extensionality rule.
I tried this way too, but ended up falling back to this definition. It makes the identity principle in equality-of-metric-spaces more direct, without having to define everything on pseudometric spaces first.
| ( symmetric-sim-Pseudometric-Space A) , | ||
| ( transitive-sim-Pseudometric-Space A) | ||
|
|
||
| equivalence-sim-Pseudometric-Space : |
There was a problem hiding this comment.
As much as I dislike the added verbosity, this might need to be equivalence-relation, just because of how many overloadings of the word "equivalence" are present in Unimath.
There was a problem hiding this comment.
As much as I dislike the added verbosity, this might need to be
equivalence-relation, just because of how many overloadings of the word "equivalence" are present in Unimath.
yes, I don't like to be too verbose either. I think equivalence-relation-sim-XXX is a bit to much, since relation and sim represent the same concept in this context. Moreover, in the context of "equivalence" referring to equivalences between types, names usually use equiv instead equivalence so equiv-sim-Pseudometric-Space (whatever it would be), would be a different thing.
As usual, I'm just trying to explain/defend my naming choices. I'll be happy to change it that doesn't convince anybody.
Refactoring the metric space module (#1421)
remove the notion of
Premetric/Premetric-Space:as we discussed, the term "premetric" has too many different meanings to be reliably used in this library. What was called a
Premetricis now aRational-Neighborhood-Relationand we only focus on (pseudo)metric spaces.all (pseudo)metric spaces are saturated:
including saturation in the definition of pseudometric space is coherent with the definition of Richman premetric spaces and makes a lot of things easier (e.g.: the limit map is short, the metric space of Cauchy approximations in a complete metric space is complete, etc.).
simplify hierarchy in concepts (define things for for metric spaces first, instead of the splitting premetric>pseudometric>metric):
although a lot of concepts only depend on the underlying neighborhood relation, they are principally useful for (pseudo)metric spaces. We prioritized definitions on metric spaces, which is where they're the most useful; if we need the corresponding concepts for pseudometric spaces, we can add them later. (e.g. we'll probably want
isometry-Pseudometric-Spaceat some point but I think this PR is already big enough).