Define the completion of an arbitrary metric space

[lowasser]

It is not actually obvious to me right this minute that this is possible, and I don't think equivalence classes of Cauchy approximations will cut it.

When defining the limit of a Cauchy approximation of equivalence classes Cauchy approximations -- that is, showing that the metric space of equivalence classes of Cauchy approximations is complete -- essentially what you want is to construct a new Cauchy approximation, mapping each epsilon to the value of an inhabitant of the equivalence class at that epsilon. It requires countable choice to pick out the inhabitant (because the domain Q+ is countable).

HoTT, now that I actually look at it for how it defines Cauchy reals, uses a higher inductive-inductive type family to simultaneously construct the reals and the neighborhood relation between them. Every place I've seen this sort of higher inductive-inductive construction done before uses Cubical Agda or some other system that does fancy shenanigans with defining equality in terms of paths.

I haven't yet figured out if you can do it with just truncation the way agda-unimath seems to.

[VojtechStep]

I haven't yet figured out if you can do it with just truncation the way agda-unimath seems to.

I'm not an expert, but while I'd expect just truncations to not be enough, I believe you should be able to construct the type with just point constructors, then define the relation on that, then take the coequaliser to add the paths, and then set truncate. It sounds like a real PITA to work with, though related formalization will probably just use the universal property and not the concrete construction

[lowasser]

Some things worth noting from my research:

nLab:

On the other hand, even the (modulated) Cauchy real numbers are not necessarily Cauchy complete, i.e. a Cauchy sequence (even a modulated one) of Cauchy real numbers need not converge to another Cauchy real number (though it always does converge to a Dedekind real number, since the Dedekind real numbers are always Cauchy complete). The problem is that without enough countable choice, we cannot lift a (modulated) Cauchy sequence of (modulated Cauchy) real numbers to a Cauchy sequence of Cauchy sequences in order to “diagonalize” it; a countermodel is constructed by Lubarsky.

(This uses a direct definition of the Cauchy reals as equivalence classes of Cauchy approximations, not the higher inductive-inductive definition used in HoTT definition 13.3.2.)

I also see that even Cubical Agda didn't support higher inductive types, at least recently.

The point constructors get tricksy to a point I'm not sure I can get past, unfortunately, as a result of shenanigans with coinductive records, which appear to be the only way to support the coinductive types being used, on the one hand -- but on the other hand, some of these want multiple constructors, and how coinductive data types, as opposed to records, are antirecommended.

For points in the completion of a metric space, a simple coproduct type in the record field is adequate, but I don't think that suffices for the neighborhood relation, because the constructor arguments have different shapes -- e.g. some constructors are only valid for mapped points from the original metric space, some are only valid for limits of Cauchy approximations.

[malarbol]

essentially what you want is to construct a new Cauchy approximation, mapping each epsilon to the value of an inhabitant of the equivalence class at that epsilon.

If I understood correctly, we need to construct a map ℚ⁺ → A from a map ℚ⁺ → (A / ~) and it's only possible with countable choice?

It seems to me that a map into the quotient of ℚ⁺ → A under f ~ g = (d : ℚ⁺) → (f d) ~ (g d), i.e. a map

(ℚ⁺ → (A / ~)) → (ℚ⁺ → A) / ~

would be enough. Is there a way to construct this using some universal property of quotient spaces or does it also require some choice principal?

For example, proving that any map ℚ⁺ → (A / ~) is equal to class ∘ f for some f : ℚ⁺ → A, would be enough but I guess this is where you need the choice axiom. Is there any way to construct an object in (ℚ⁺ → A) / ~ without actually having to define any map ℚ⁺ → A?

PS: sorry it these are dumb questions or known results on quotients or choices. As you know, I haven't worked with set quotients a lot and I lack some insight on the different choice principles.

[lowasser]

Yes, you've found where we need choice; no, it doesn't look like you can do it without choice -- the comment I quoted above from nLab cites an explicit counterexample, it seems.

I am hopeful the higher inductive strategy from HoTT is viable, but haven't yet found a way to do it that satisfies Agda's positivity checking as described here. I have some hopes of figuring out a way to do it, maybe using some explicit counter for how many levels deep we are in the induction.

[malarbol]

Ok. That's a shame. Even though, I still think the "Cauchy pseudometric space of Cauchy approximations in a metric space" could be an interesting concept to add. I.e. the pseudometric space of Cauchy approximations in a metric space with neighborhoods given by N-cauchy d f g = (ε δ : ℚ⁺) → N (ε + δ + d) (f ε) (g δ). And the same goes for "metric quotient of a pseudometric space": i.e. the quotient of a pseudometric space by the metric identification, with a quotient metric structure (TBD).

At least we could prove some fun results like "any Cauchy approximation in the Cauchy pseudometric space of Cauchy approximations has a limit" (some kind of pseudocomplete pseudometric space) and mention how it does not extend to the metric quotient so it's not enough to mimic the classic construction of metric completion.

[lowasser]

Even though, I still think the "Cauchy pseudometric space of Cauchy approximations in a metric space" could be an interesting concept to add. I.e. the pseudometric space of Cauchy approximations in a metric space with neighborhoods given by N-cauchy d f g = (ε δ : ℚ⁺) → N (ε + δ + d) (f ε) (g δ). And the same goes for "metric quotient of a pseudometric space": i.e. the quotient of a pseudometric space by the metric identification, with a quotient metric structure (TBD).

I have successfully implemented those atop #1450 ; I figured I'd wait for that to be merged before submitting the PRs.

Also, FWIW, I eventually realized coinduction isn't actually what we are looking for. Additionally, it might be worth having the definition available even if it does require countable choice, potentially using the style demonstrated in #1380 .

I think my most recent idea for how to emulate the HoTT approach is doomed to failure, unfortunately. I had imagined an inductive step of "how many limit operations deep are we," but that doesn't adequately handle the case where we have a Cauchy approximation where the number of limit operations grows without bound for e.g. sufficiently small epsilon, and the types don't actually allow you to ignore that case.

We could simply turn off positivity checking for this file, but as described in Agda's docs, that allows you to prove contradictions.

I may just go ahead and implement completions of metric spaces with countable choice, though there are at least some steps to make that happen: notably, we have to show countable choice implies choice for the rational numbers, which is unexpectedly tricky for the definitions of countability we have today.

[malarbol]

Even though, I still think the "Cauchy pseudometric space of Cauchy approximations in a metric space" could be an interesting concept to add. I.e. the pseudometric space of Cauchy approximations in a metric space with neighborhoods given by N-cauchy d f g = (ε δ : ℚ⁺) → N (ε + δ + d) (f ε) (g δ). And the same goes for "metric quotient of a pseudometric space": i.e. the quotient of a pseudometric space by the metric identification, with a quotient metric structure (TBD).

I have successfully implemented those atop #1450 ; I figured I'd wait for that to be merged before submitting the PRs.

Ow! That's cool! How was your experience working atop #1450? Was the new name scheme pleasant to work with? And I'd really love to see it, specifically the metric identification work. It's been in my mind for quite some time now so it would actually be a relief to see it formalized.

I may just go ahead and implement completions of metric spaces with countable choice, though there are at least some steps to make that happen: notably, we have to show countable choice implies choice for the rational numbers, which is unexpectedly tricky for the definitions of countability we have today.

I'd love to help, if a can.

[malarbol]

Yes, you've found where we need choice; no, it doesn't look like you can do it without choice -- the comment I quoted above from nLab cites an explicit counterexample, it seems.

So ,to be clear, there's a map ((ℚ⁺ → A) / ~) → (ℚ⁺ → (A / ~)) but there's absolutely no hope to construct an inverse map (ℚ⁺ → (A / ~)) → ((ℚ⁺ → A) / ~) without some countable choice axiom?

[lowasser]

I am perfectly satisfied with #1450 and had no objections.

As far as the countable choice....uh, the issue is getting from ℚ⁺ → ((ℚ⁺ → A) / ~) to (ℚ⁺ → A) / ~, I think? Getting from a Cauchy approximation (in the quotient metric space) of equivalence classes of Cauchy approximations (in the original metric space A), to a new equivalence class of Cauchy approximations. The double layering is important. The key point is that as soon as you have a map from ℚ⁺ to equivalence classes, you need countable choice to get representatives of the equivalence classes that you could actually do anything with.

[lowasser]

As for seeing the examples of what I did with #1450:

https://github.com/lowasser/agda-unimath/blob/redo-cauchy-approximation-metrics/src/metric-spaces/pseudometric-space-of-cauchy-approximations-metric-spaces.lagda.md

https://github.com/lowasser/agda-unimath/blob/induced-metric-space-pseudometric/src/metric-spaces/induced-metric-space-of-pseudometric-spaces.lagda.md

[malarbol]

As for seeing the examples of what I did with #1450:

https://github.com/lowasser/agda-unimath/blob/redo-cauchy-approximation-metrics/src/metric-spaces/pseudometric-space-of-cauchy-approximations-metric-spaces.lagda.md

https://github.com/lowasser/agda-unimath/blob/induced-metric-space-pseudometric/src/metric-spaces/induced-metric-space-of-pseudometric-spaces.lagda.md

That's really cool! I hope we can get #1450 merged soon and work with that!

[malarbol]

As far as the countable choice....uh, the issue is getting from ℚ⁺ → ((ℚ⁺ → A) / ~) to (ℚ⁺ → A) / ~, I think? Getting from a Cauchy approximation (in the quotient metric space) of equivalence classes of Cauchy approximations (in the original metric space A), to a new equivalence class of Cauchy approximations. The double layering is important. The key point is that as soon as you have a map from ℚ⁺ to equivalence classes, you need countable choice to get representatives of the equivalence classes that you could actually do anything with.

To be clear, in what I wrote, A was the pseudometric space of Cauchy approximations (with the Cauchy pseudometric) and ~ the similarity relation w.r.t. this pseudometric (so the double layering with hidden inside A). The plan was to show that "any Cauchy approximation in the pseudometric space of Cauchy approximations has a pseudometric limit" and then take the quotients. But I'm still missing a way to relate "Cauchy approximations in the pseudometric space" and "Cauchy approximations in the quotient metric space".

The pointwise quotient gives a map from "Cauchy approximations in the pseudometric space" to "Cauchy approximations in the quotient metric space" and I understand countable choice would be needed to construct some inverse map but I actually need slightly less: the space of "Cauchy approximations in the pseudometric space" has a product equivalence relation induced by the similarity relation in the pseudometric space and the pointwise quotient factors into a map ((ℚ⁺ → A) / ~) → (ℚ⁺ → (A / ~)) (quotient of Cauchy approximations into Cauchy approximations in the quotient). If this map could be inverted somehow, I think that would finish the proof. I really hoped some universal property of the quotient would help, but it seems not.

Anyways, parts of this plans might still be useful so maybe I'll try to work some details. And I really need to understand quotient spaces better. E.g. what are Cauchy approximations in the quotient metric space, and how can I prove things on them.

[malarbol]

Hello again. I finally convinced myself that the existence of a map (ℚ⁺ → (A / ~)) → ((ℚ⁺ → A) / ~) for all type A and equivalence relation ~ on A does require ACC. However, I still have a little speck of hope that, maybe we could do without it. The equivalence relation we are considering here is deeply connected with the underlying pseudometric structure and the property we are trying to prove (convergence of Cauchy approximation) so maybe there's a workaround to using ACC.

In your construction of the metric quotient of a pseudometric space (metric identification), is there any way to relate Cauchy approximations in the quotient to Cauchy approximations in the non-quotiented pseudometric space? E.g. any Cauchy approximation in the quotient can be approximated by a Cauchy approximation of the form quotient-map ∘ f for some Cauchy approximation f in the pseudometric space?

[fredrik-bakke]

I'm not an expert, but while I'd expect just truncations to not be enough, I believe you should be able to construct the type with just point constructors, then define the relation on that, then take the coequaliser to add the paths, and then set truncate. It sounds like a real PITA to work with, though related formalization will probably just use the universal property and not the concrete construction

Sorry for interjecting, but I think what you are looking for is a set quotient.

[malarbol]

As for seeing the examples of what I did with #1450:

https://github.com/lowasser/agda-unimath/blob/redo-cauchy-approximation-metrics/src/metric-spaces/pseudometric-space-of-cauchy-approximations-metric-spaces.lagda.md

How do you feel about calling this pseudometric-completion-metric-spaces? After all, it seems that, for any metric space M, we construct a pseudometric space N such that:

• there's an isometry of pseudometric spaces M → N;
• any Cauchy approximation in N has a limit;
• for any complete metric space C, any short map M → C uniquely factors through a short map N → C.

[lowasser]

I feel awkward about calling it a completion when it's not complete, I will admit.

[malarbol]

I feel awkward about calling it a completion when it's not complete, I will admit.

I was under the impression that this pseudometric space was complete (i.e., all Cauchy approximations have a limit).

I understand the term "complete pseudometric space" could be problematic: non-unicity of limits in pseudometric spaces make this concept a structure rather than a property but this seems relevant somehow.

[lowasser]

Oh, right, without the truncation to a metric space we don't have to use choice. Yeah, then that's okay.

[malarbol]

Oh, right, without the truncation to a metric space we don't have to use choice. Yeah, then that's okay.

I'm still bugged that we can't prove that the metric quotient of a complete pseudometric space is complete, but I guess this is still an interesting step.

[malarbol]

I've been given another look at https://github.com/lowasser/agda-unimath/blob/induced-metric-space-pseudometric/src/metric-spaces/induced-metric-space-of-pseudometric-spaces.lagda.md and I wonder if it would be better to use set-quotient instead of equivalence-class in type-induced-metric-space-Pseudometric-Space.

This still doesn't solve some completion problem or anything like this, but I think it's nicer to keep the levels at Metric-Space (l1 ⊔ l2) (l1 ⊔ l2)

[lowasser]

For sure. I mostly just hadn't figured out how to use set quotients yet. I can have another go at it if we like.

[malarbol]

For sure. I mostly just hadn't figured out how to use set quotients yet. I can have another go at it if we like.

I think I'll try it myself too. I'm learning about set quotients, with a few interesting results in #1482, and this seems like a nice result to follow up with.

You already seem quite busy with a lot of other PRs so I was thinking about taking https://github.com/lowasser/agda-unimath/blob/induced-metric-space-pseudometric/src/metric-spaces/induced-metric-space-of-pseudometric-spaces.lagda.md as a base module, crediting you, and then making the changes to use set-quotient instead of equivalence-class.

[malarbol]

For sure. I mostly just hadn't figured out how to use set quotients yet. I can have another go at it if we like.

I've reworked https://github.com/lowasser/agda-unimath/blob/induced-metric-space-pseudometric/src/metric-spaces/induced-metric-space-of-pseudometric-spaces.lagda.md for quotient sets in #1484 (src/metric-spaces/induced-metric-space-of-pseudometric-spaces.lagda.md) if you want to have a look.

Incidentally, for a metric space M : Metric-Space l1 l2, both this construction and Σ-components-at-bounded-distance-Metric-Space (see src/metric-spaces/decomposition-metric-spaces-elements-at-bounded-distance-metric-spaces.lagda.md) define a metric space in Metric-Space (l1 ⊔ l2) (l1 ⊔ l2) isometrically equivalent to M, so they're actually equal. I'm not sure what to make of that, but I guess we'll have to mention it at some point.

[lowasser]

Sounds great, go for it.

[malarbol]

Sounds great, go for it.

I already did, half an hour ago.

Since you're always ok I figured I would go for it without bothering you asking. I've obviously co-credited you in the PR and I'd be happy to have your feedback. (It's built atop #1450 so the diff is a bit messy.)

[malarbol]

So, one the one hand, we have (#1486)

pseudometric-completion-Pseudometric-Space : 
  Pseudometric-Space l1 l2 → Pseudometric-Space (l1 ⊔ l2) l2

such that

has-limit-cauchy-approximation-pseudometric-completion-Pseudometric-Space :
  ( U :
    cauchy-approximation-Pseudometric-Space
      ( pseudometric-completion-Pseudometric-Space M)) →
  Σ ( cauchy-approximation-Pseudometric-Space M)
     ( is-limit-cauchy-approximation-Pseudometric-Space
       ( pseudometric-completion-Pseudometric-Space M)
       ( U))

and on the other hand we have (#1484)

metric-quotient-Pseudometric-Space : 
  Pseudometric-Space l1 l2 → Metric-Space (l1 ⊔ l2) (l1 ⊔ l2) 

If I understood correctly, the plan was to consider the construction

pseudocompletion-Metric-Space : 
  Metric-Space l1 l2 → Metric-Space (l1 ⊔ l2) (l1 ⊔ l2) 
pseudocompletion-Metric-Space M =
  metric-quotient-Pseudometric-Space
    ( pseudometric-completion-Pseudometric-Space
      ( pseudometric-Metric-Space M))

as a candidate for Cauchy completion of M.

We don't know how to prove that cauchy-pseudocompletion-Metric-Space M is complete without the axiom of countable choice. For some reason, I still have faith we can prove this without ACC but I'd prefer to know if it's hopeless.

Have you seen / thought of / etc. any proof that

∀ (M : Metric-Space l1 l2) → is-complete-Metric-Space (pseudocompletion-Metric-Space M)

actually implies the axiom of countable choice?

[malarbol]

Just a few follow-up thoughts on this. Please correct me if you see anything wrong

0. we're trying to prove that a certain metric quotient space P / ~ (where P is a pseudometric space) is complete.
1. this involves working with some maps ℚ⁺ → (P / ~). Using results on generic equivalence relations eventually leads us to ACC. That's because anything that work for "all equivalence relations" should also work for the trivial equivalence relation, where the quotient space is essentially the propositional truncation. E.g. lifting maps from ℚ⁺ → (P / ~) to (ℚ⁺ → P) / ~) is ACC. So, put another way, if we hope to prove (0.), we'll have to use some specific properties of our equivalent relation (similarity in the pseudometric-completion space).
2. when you said

essentially what you want is to construct a new Cauchy approximation, mapping each epsilon to the value of an inhabitant of the equivalence class at that epsilon.

you mean that given a Cauchy approximation u in P / ~, we need to construct a Cauchy approximation v in P such that quotient-map ∘ v ＝ u (as Cauchy approximations in P / ~). It seems to me that we can slightly relax this condition by asking quotient-map ∘ v and u to be similar in the Cauchy-pseudometric space of Cauchy approximations in P / ~. If ~ were the trivial equivalence relation, this would again be equivalent to ACC, but in our case it's not, so maybe there's hope. Moreover, asking quotient-map ∘ v ＝ u is the same as similarity in the "product pseudometric structure" on Cauchy approximations in P / ~. Working with the Cauchy-pseudometric structure instead might help us?

3. We're not only working with generic maps u : ℚ⁺ → (P / ~) but Cauchy approximations so the additional properties on u ε and u δ might also help us somehow. For example, when working with "bounded distance decompositions" in #1482, not all maps ℚ⁺ → A take value in s single bounded-distance component, but Cauchy approximations do and this enables to prove a few properties. Maybe we can hope something similar happens here.

[malarbol]

It seems to me that we can slightly relax this condition by asking quotient-map ∘ v and u to be similar in the Cauchy-pseudometric space of Cauchy approximations in P / ~.

I formalized this last thought a bit better and it is actually a characterization of convergent Cauchy approximations in the "metric pseudocompletion": defining

module _
  {l1 l2 : Level} (P : Pseudometric-Space l1 l2)
  where

  metric-pseudocompletion-Pseudometric-Space :
    Metric-Space (l1 ⊔ l2) (l1 ⊔ l2)
  metric-pseudocompletion-Pseudometric-Space =
    metric-quotient-Pseudometric-Space
      ( pseudometric-completion-Pseudometric-Space P)

  pseudometric-metric-pseudocompletion-Pseudometric-Space :
    Pseudometric-Space (l1 ⊔ l2) (l1 ⊔ l2)
  pseudometric-metric-pseudocompletion-Pseudometric-Space =
    pseudometric-Metric-Space
      metric-pseudocompletion-Pseudometric-Space

you get a characterization of convergent Cauchy approximations in metric-pseudocompletion-Pseudometric-Space P as

  lemma-is-convergent-cauchy-approximation-metric-pseudocompletion-Pseudometric-Space :
    ( u :
      cauchy-approximation-Metric-Space
        ( metric-pseudocompletion-Pseudometric-Space P)) →
    is-convergent-cauchy-approximation-Metric-Space
      ( metric-pseudocompletion-Pseudometric-Space P)
      ( u) ↔
    exists
      ( cauchy-approximation-Pseudometric-Space
        ( pseudometric-completion-Pseudometric-Space P))
      ( λ v →
        sim-prop-Pseudometric-Space
          ( pseudometric-completion-Pseudometric-Space
            ( pseudometric-metric-pseudocompletion-Pseudometric-Space P))
          ( u)
          ( map-metric-quotient-cauchy-approximation-Pseudometric-Space
            ( pseudometric-completion-Pseudometric-Space P)
            ( v)))
  [...]

so proving that it is complete is exactly like proving that all Cauchy approximations can be lifted up to similarity. I still don't know how to prove this but it seems less restrictive that full-fledged lifts so I don't believe they are really necessary.

[malarbol]

[Sorry for the long posts. I'm using this space as a notebook while researching metric completions.]

Following up with

 lemma-is-convergent-cauchy-approximation-metric-pseudocompletion-Pseudometric-Space :
    ( u :
      cauchy-approximation-Metric-Space
        ( metric-pseudocompletion-Pseudometric-Space P)) →
    is-convergent-cauchy-approximation-Metric-Space
      ( metric-pseudocompletion-Pseudometric-Space P)
      ( u) ↔
    exists
      ( cauchy-approximation-Pseudometric-Space
        ( pseudometric-completion-Pseudometric-Space P))
      ( λ v →
        sim-prop-Pseudometric-Space
          ( pseudometric-completion-Pseudometric-Space
            ( pseudometric-metric-pseudocompletion-Pseudometric-Space P))
          ( u)
          ( map-metric-quotient-cauchy-approximation-Pseudometric-Space
            ( pseudometric-completion-Pseudometric-Space P)
            ( v)))
  [...]

this last condition is equivalent to the existence of v : cauchy-approximation-Pseudometric-Space (pseudometric-completion-Pseudometric-Space P) such that the class quotient of u in the metric pseudocompletion of the metric pseudocompletion of P is the class quotient of

map-metric-quotient-cauchy-approximation-Pseudometric-Space
  ( pseudometric-completion-Pseudometric-Space P)
  ( v))

This only depends on the class of v in the metric pseudocompletion of the pseudometric completion of P so we need to relate quotient-map u (in the metric pseudocompletion of the metric pseudocompletion of P) to some element quotient-map v (in the metric pseudocompletion of the pseudometric completion of P) via map-metric-quotient-cauchy-approximation-Pseudometric-Space.

This suggests that the metric pseudocompletion of the pseudometric completion of P could play a prominent role in the proof, somehow.

I managed to prove that this equal to the metric pseudocompletion of P, which is quite promising. The metric pseudocompletion absorbs pseudometric completion on the right.

The map map-metric-quotient-cauchy-approximation-Pseudometric-Space extends to a map from the metric pseudocompletion of the pseudometric completion of P to the metric pseudocompletion of its metric pseudocompletion; we need to prove that this map is an equivalence.

[malarbol]

In other words, if we denote by

C : Pseudometric-Space → Pseudometric-Space 
C = pseudometric-completion-Pseudometric-Space

Q : Pseudometric-Space → Metric-Space 
Q = metric-quotient-Pseudometric-Space

p : Metric-Space → Pseudometric-Space
p = pseudometric-Metric-Space

we want to prove that for any P : Pseudometric-Space l1 l2, Q (C P) is complete, i.e., construct a map

C (p (Q (C P))) → Q (C P)

To do this, I think we need to understand the relation

Q ( C (p (Q (C P)))) ↔ Q ( C (C P)) ↔ Q (C P)

for the right hand, quotients of limits give a proof that Q ( C (C P)) ＝ Q (C P) ; for the left hand, there's a natural map Q (C (C P)) → Q ( C (p (Q (C P)))); we need to prove that this is an isometric equivalence.