Refactor `metric-spaces` module

[malarbol]

Recent contributions in the metric-spaces modules raise concerns about the names of some concepts in the metric-spaces module.

TODO

• The divide metric space/metric structure seems a bit over the top. I suggest we factor these to be contained in the same files (and same for premetrics and pseudometrics and any other such divides in this namespace).

• The concept of indistinguishability should be factored to separate files, called similarty-of-elements-metric-spaces and so on. This is consistent with other notions of similarity in the library.

• The definition of indistinguishability in premetric spaces is not the correct one, it only applies to (reflexive?) symmetric premetric spaces. I propose we forget the non pseudo- case and only first define similarity for pseudometric spaces.

• Find a good name for metric spaces where all elements are at bounded distance

  • total
  • indiscrete

Related PRs

• Refactor metric spaces #1432
• large premetric spaces #1426

[fredrik-bakke]

Here's a couple more points:

• The divide metric space/metric structure seems a bit over the top. I suggest we factor these to be contained in the same files (and same for premetrics and pseudometrics and any other such divides in this namespace).
• The concept of indistinguishability should be factored to separate files, called similarty-of-elements-metric-spaces and so on. This is consistent with other notions of similarity in the library.
• The definition of indistinguishability in premetric spaces is not the correct one, it only applies to (reflexive?) symmetric premetric spaces. I propose we forget the non pseudo- case and only first define similarity for pseudometric spaces.

[fredrik-bakke]

For future reference, the correct similarity relation on premetric spaces is probably

(x ≍ y) :=
  ((ε : ℚ⁺) → (B ε x x ↔ B ε y y)) ×
  ((ε : ℚ⁺) (z : A) → (B ε x z ↔ B ε y z)) ×
  ((ε : ℚ⁺) (z : A) → (B ε z x ↔ B ε z y))

[malarbol]

For future reference, the correct similarity relation on premetric spaces is probably

(x ≍ y) :=
  ((ε : ℚ⁺) → (B ε x x ↔ B ε y y)) ×
  ((ε : ℚ⁺) (z : A) → (B ε x z ↔ B ε y z)) ×
  ((ε : ℚ⁺) (z : A) → (B ε z x ↔ B ε z y))

After a few weeks I finally understood this comment. But I'm pretty sure the first condition is redundant as it's a consequence of the other two.

[fredrik-bakke]

For future reference, the correct similarity relation on premetric spaces is probably

(x ≍ y) :=
  ((ε : ℚ⁺) → (B ε x x ↔ B ε y y)) ×
  ((ε : ℚ⁺) (z : A) → (B ε x z ↔ B ε y z)) ×
  ((ε : ℚ⁺) (z : A) → (B ε z x ↔ B ε z y))

After a few weeks I finally understood this comment. But I'm pretty sure the first condition is redundant as it's a consequence of the other two.

Is it? Don't you need triangularity for that?

[malarbol]

I've been working on this in #1432; obviously there's still a lot to do but I'm trying to set-up a new name-scheme and hierarchy (replace premetric/pseudometric/metric with just premetric/metric) where "metric spaces are extensional premetric spaces" so if you want to have a look and comment anything, it would be nice before I go further.

One of my main concern is rewriting the identity principle for metric spaces but I hope I can get it right.

[malarbol]

For future reference, the correct similarity relation on premetric spaces is probably

(x ≍ y) :=
  ((ε : ℚ⁺) → (B ε x x ↔ B ε y y)) ×
  ((ε : ℚ⁺) (z : A) → (B ε x z ↔ B ε y z)) ×
  ((ε : ℚ⁺) (z : A) → (B ε z x ↔ B ε z y))

After a few weeks I finally understood this comment. But I'm pretty sure the first condition is redundant as it's a consequence of the other two.

Is it? Don't you need triangularity for that?

Unless I missed something, I don't think so. It's there (lines 231+) :

module _ {l1 l2 : Level} {A : UU l1} (N : Rational-Neighborhood-Relation l2 A)
  where

  sim-prop-Rational-Neighborhood-Relation : Relation-Prop (l1 ⊔ l2) A
  sim-prop-Rational-Neighborhood-Relation x y =
    Π-Prop
      ( ℚ⁺)
      ( λ d →
        Π-Prop
          ( A)
          ( λ z →
            product-Prop
              ( N d x z ⇔ N d y z)
              ( N d z x ⇔ N d z y)))

  sim-Rational-Neighborhood-Relation : Relation (l1 ⊔ l2) A
  sim-Rational-Neighborhood-Relation x y =
    type-Prop (sim-prop-Rational-Neighborhood-Relation x y)

  [...]

  iff-left-neighbor-sim-Rational-Neighborhood-Relation :
    {x y : A} →
    sim-Rational-Neighborhood-Relation x y →
    (d : ℚ⁺) (z : A) →
    neighborhood-Rational-Neighborhood-Relation N d x z ↔
    neighborhood-Rational-Neighborhood-Relation N d y z
  iff-left-neighbor-sim-Rational-Neighborhood-Relation x≍y d z =
    pr1 (x≍y d z)

  iff-right-neighbor-sim-Rational-Neighborhood-Relation :
    {x y : A} →
    sim-Rational-Neighborhood-Relation x y →
    (d : ℚ⁺) (z : A) →
    neighborhood-Rational-Neighborhood-Relation N d z x ↔
    neighborhood-Rational-Neighborhood-Relation N d z y
  iff-right-neighbor-sim-Rational-Neighborhood-Relation x≍y d z =
    pr2 (x≍y d z)

module _
  {l1 l2 : Level} {A : UU l1} (N : Rational-Neighborhood-Relation l2 A)
  where

  iff-self-neighborhood-sim-Rational-Neighborhood-Relation :
    (d : ℚ⁺) (x y : A) →
    sim-Rational-Neighborhood-Relation N x y →
    neighborhood-Rational-Neighborhood-Relation N d x x ↔
    neighborhood-Rational-Neighborhood-Relation N d y y
  iff-self-neighborhood-sim-Rational-Neighborhood-Relation d x y x≍y =
    ( iff-right-neighbor-sim-Rational-Neighborhood-Relation N x≍y d y) ∘iff
    ( iff-left-neighbor-sim-Rational-Neighborhood-Relation N x≍y d x)

[fredrik-bakke]

Ah, okay, great

[malarbol]

BTW, I really feel like adding the saturated axiom on premetric spaces. This way, the limit map is short, the natural similarity relation is equivalent to ∀ δ → N δ x y, we have N ε x y ⇔ (∀ δ → ε < δ → N δ x y) as in the (fixed) third axiom of Richman premetric spaces, etc. And I don't really see any drawback.

Do you have any objection, @fredrik-bakke or @lowasser ?

[fredrik-bakke]

BTW, I really feel like adding the saturated axiom on premetric spaces. This way, the limit map is short, the natural similarity relation is equivalent to ∀ δ → N δ x y, we have N ε x y ⇔ (∀ δ → ε < δ → N δ x y) as in the (fixed) third axiom of Richman premetric spaces, etc. And I don't really see any drawback.

Do you have any objection, @fredrik-bakke or @lowasser ?

Is this what is currently called closed premtric spaces in the library? I don't have anything against this, and since Richman agrees it is a good condition to add it seems plausible that it is good. The questions one should ask oneself is

1. Is this condition important in establishing the basic theory of "(pre)metric spaces"?
2. Are there important examples that do not satisfy this axiom?

[malarbol]

BTW, I really feel like adding the saturated axiom on premetric spaces. This way, the limit map is short, the natural similarity relation is equivalent to ∀ δ → N δ x y, we have N ε x y ⇔ (∀ δ → ε < δ → N δ x y) as in the (fixed) third axiom of Richman premetric spaces, etc. And I don't really see any drawback.
Do you have any objection, @fredrik-bakke or @lowasser ?

Is this what is currently called closed premtric spaces in the library?

Yes, and then I use this to define saturated metric spaces, metric spaces where the premetric structure is closed (not he best names, I know...) and other variations.

I don't have anything against this, and since Richman agrees it is a good condition to add it seems plausible that it is good. The questions one should ask oneself is

1. Is this condition important in establishing the basic theory of "(pre)metric spaces"?

I do believe it helps tying everything up together. E.g., as I mentioned before, we'd really like to have "the complete metric space of Cauchy approximations in a complete metric space" instead of having to specify "the saturated complete metric space of Cauchy approximations in a saturated complete metric space".

2. Are there important examples that do not satisfy this axiom?

I don't think there is. At the moment, any metric spaces can be saturated and we should expect any meaningful properties to be preserved. The basic example would be metric-space-of-rational-numbers-with-open-neighborhoods but it's mainly here as an example of non-saturated metric space, although it's not even mentioned. I wouldn't consider it important.