4 ms·
Good point. So then the question becomes: can you prove in HoTT that there exist irrational x, y such that x^y is rational?
by auggierose 13y ago
Good point. So then the question becomes: can you prove in HoTT that there exist irrational x, y such that x^y is rational?
- fmap 13y agoYes. You can translate the classical proof, assuming excluded middle for propositions.