I want to formalize some undergraduate maths in cubical agda, and learning cubical type theory in the proccess. The problem is that I will need univalent excluded middle and univalent choice (and maybe propositional resizing). I know these are consistent with homotopy type theory (although computation is lost when axiom are used), but cubical that type theory is stronger (in the sense that univalence is a theorem). Are this axiom still consistent in the cubical setting? Is there a better way of doing classical theorems in cubical type theory?