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.