[Chattered]

There might be some confusion. The typical proof of the irrationality of root 2 is phrased as a proof-by-contradiction, and I've come across folk who mistakenly think that this technique is exclusive to classical mathematics.

In fact, the standard proof-by-contradiction that sqrt(2) is irrational is also intuitionistically valid. The important point for this case is that we're proving a negative property (irrationality), so this sort of proof by contradiction is fine.

The standard example of a classical proof I use is the one showing that there exist irrationals x and y such that x^y is rational. The dead easy proof asks whether x^y is rational for x=y=sqrt(2). If it is, we're done. Otherwise, we just take x=sqrt(2)^sqrt(2) and y=sqrt(2).

But note that we don't actually know for sure which x and y work, so this is definitely classical. An intuitionistic proof here would have to tell us directly what x and what y work.

[auggierose]

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]

Yes. You can translate the classical proof, assuming excluded middle for propositions.