No, "is not irrational" isn't the same as "is rational" without excluded middle; that's the whole point. (Equality of real numbers is not computable, so there is nonconstructive content to the implication "if not irrational, then rational".)
(I will retract a whole bunch of my worldview if you can inhabit the type "not-not-rational -> rational" in something like MLTT.)
You take a set S and partition it into two subsets, A and B, so that each element uniquely belongs to either of them. For each element of S it is true that "not-not-in-A -> in-A". Can this be shown to be true in MLTT? I don't know much about setoids to show it, but if it can't, that's the problem of MLTT, not mine. In the context of this proof, it is true.
(I will retract a whole bunch of my worldview if you can inhabit the type "not-not-rational -> rational" in something like MLTT.)