The power of this seems similar to the power of constructive Cauchy sequences because you can use the (x < y) → A u B function to approximate the value to any positive precision error.
If you have (x<y)→A∪B, then I think that’s true, but if you just have (x<y)→||A∪B|| (where ||−|| is propositional truncation, basically quotienting by the relation that is always true, so collapsing the two sides to be indistinguishable), then the homotopy type book suggests that it might be wrong.
It’s a bit similar to how the naive types-as-propositions encoding of the axiom of choice makes it trivially provable constructively, but a more careful encoding makes it imply excluded middle.
I guess to clean it up even further:
A set L is a lower real number when it is inhabited, downwards-closed and upwards-rounded.
A set U is an upper real number when it is inhabited, upwards-closed and downwards-rounded.
A closed interval [sup L, inf U] is constructed with a lower real L and an upper real U such that L < U.
A closed interval [sup L, inf U] is a real number if every rational interval x < y either has x < sup L or inf U < y.
The power of this seems similar to the power of constructive Cauchy sequences because you can use the (x < y) → A u B function to approximate the value to any positive precision error.
If you have (x<y)→A∪B, then I think that’s true, but if you just have (x<y)→||A∪B|| (where ||−|| is propositional truncation, basically quotienting by the relation that is always true, so collapsing the two sides to be indistinguishable), then the homotopy type book suggests that it might be wrong.
It’s a bit similar to how the naive types-as-propositions encoding of the axiom of choice makes it trivially provable constructively, but a more careful encoding makes it imply excluded middle.