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.
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.