An important aspect of the Univalent Foundations is that it is compatible with classical mathematics. In fact, Voevodsky's simplicial set model of Martin-Lof type theory with the univalence axiom models the law of excluded middle too. So if you insist on doing things classically in Homotopy Type Theory, you may do so to your hearts content. You will only loose a bit of generality, i.e. your constructions will not work in every model of the type theory but only in the classical ones. But the computer assisted theorem proving won't be lost by just assuming LEM. However, when you have a computer proof that involves the axiom of choice of the law of excluded middle and you try to execute your proof (as if it were a program) the computer will get stuck on the instances where you have applied AC or LEM.
As for the various notions of real numbers or compactness, consider it a richness or a deficiency. It depends on your purposes, which you haven't explained.