Interpreting a proof of $2^\mathbb{N}$ being uncountable
There is no assumption in your proof that the functions involved are computable, so it would be quite stingy to interpret the proof that way merely because Agda allows you to compute with its terms.
Rather, yes how it should be interpreted depends on the model, and constructive (in the sense of just removing axioms) proofs like the one you've given enable an even wider range of models. So it applies to classical functions, because we can (I believe) interpret all the operations you used as operations on classical functions. It's just that when those operations are used to combine classical functions, they don't produce computable functions, even though the operations are in a sense computable.
When you do interpret the proof in a computable setting, what you get is actually a stronger result. The classical reading is, &quot;the reals (or, Cantor space really for your example) are uncountable.&quot; The computable reading is, &quot;the computable reals are computably uncountable.&quot; The latter means that we can actually compute a real that is left out of any alleged computable enumeration.
A good write up of this is here, although it applies equally well to types that aren't inductive, even though the title doesn't emphasize it. The first part of the author's thesis also gives a pretty good description of modest sets, which are a way of thinking about the 'computable operations on non-computable data' angle.
So, don't make the mistake of thinking that Agda and the like are only for reasoning about their own terms. It's an easy mistake to make coming from a computer programming background, but I think it's a mistake even there.
The reason why is your oracle example. One could imagine a model where there is an extra $^ℕ$ sequence added as a sort of brute fact (also all sequences computable from it, of course). When you ask about its bits, the computer accesses some sort of physical sensor and determines the answer based on that (and memoizes it). This bit sequence is not 'computable' in the sense of being described by some term, but as long as you haven't added axioms that depend on bit sequences being describable by terms, your proofs should hold for it. So this sort of 'open world' assumption seems to match aspects of actual computers.