Is cubical type theory still consistent with univalent excluded middle and univalent choice?
I decided to rewrite my answer, because I thought I could explain the details
better. I'd still defer to someone more knowledgeable should they happen to come
along.

I think it is relatively safe to say that cubical type theory as an approach on
the whole is compatible with the classical axioms you want. The reasons for
this are:


The differences people usually point out, like the $\mathsf{Glue}$ type,
are just a way of making univalence hold for all types, independent of
their belonging to a universe. This is (in my view) merely fixing a
limitation of the HoTT approach of minimally extending Martin-löf type
theory, where it's impossible to state the univalence axiom except by
reference to a universe. However, if you have enough universes with
univalence axioms, every type is in a universe, and so univalence holds for
all types. In fact, this is how Agda actually works directly; the universes
are primary, and all types are declared as part of a universe, similar to a
pure type system.
There is (I've heard) a cubical set model (discovered by Emily Riehl) that is
completely compatible with the standard simplicial set model, and I believe
it has been shown to be adequate for doing cubical type theory. I think what
this means is that if you add EM (and maybe choice), you get the same
homotopy theory as the classical simplicial set model. I've also heard that
there are constructive analogues of the simplicial set model, so it is not
inherently classical.


Now, what you have to worry about are other details. For instance, cubical Agda
uses the sort of cubes with inversions and connections. So, if i and j are
dimension variables, then ~ i is a dimension, and so is i ∨ j. There are
also Cartesian cubes that don't have ∨ but have other similar constructions.
These affect the details of how you are able to construct paths. Having more of
them is convenient for easily constructing compositions of paths and whatnot,
but my understanding is that the model that matches the classical simplicial
model lacks most of these things.

Now, more specifically, I've also heard that most of these other cubical set
models are anti-classical (I'd forgotten that earlier). I've not been able to
work out the details of how you demonstrate this inside implemented cubical
type theories, but my understanding is that, using ~ as an example, you try to
construct some contradictory scenario using a point i on the interval such
that i = ~i. There's no way given in the type theory to construct such a
point, and somehow it's inconsistent to presume that you can tell whether any
abstract point is or is not like that.

So, I guess the answer to your specific question is that there is probably a
way to refute excluded middle in cubical Agda (although I don't know how), and
every other computer implemented cubical type theory. But it's also likely that
a cubical type theory could be implemented that is consistent with classical
axioms (and homotopy theory) and supports all the reasoning desired (although
maybe it's more difficult to construct certain things). Unfortunately, you'll probably have to wait until the details are fleshed out more and some implementation decides to pick up the compatible version of the theory.

Another option, I suppose, is to not worry about the anti-classical part too much. If you use the cubical primitives to implement something similar to reasoning in the HoTT book, and avoid working directly with the cubical operations, you can probably be reasonably confident (I think) that you haven't relied on any paradoxes. I think there are efforts to provide a HoTT interface on top of cubical type theory in some of the libraries available. You could also dabble in learning the direct cubical parts, even though you don't use them directly, although I don't know exactly which parts are still part of the 'proper' model.

Edit: by the way, here is a presentation about cubical set models of homotopy type theory that mentions the anti-classical properties of many cubical set models. It describes, vaguely, what you have to do to refute excluded middle, but it's all in terms of looking at the models from the outside, hence some of the difficulty of translating that to a refutation within cubical type theory (for me).

Edit 2: here's a potential more positive answer. It's been pointed out to me that the constructions in the above video may not be possible to carry out inside cubical type theory. They are constructions that can be carried out in the 'intended' cubical set models, but just like Martin-löf type theory has other models than the intended one (which is how you get to HoTT), the cubical set models aren't necessarily the only model of the corresponding cubical type theory. So it's possible that cubical type theories are compatible with excluded middle and choice, even though their most obvious models are not.