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