Is cubical type theory still consistent with univalent excluded middle and univalent choice?

Question

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?

Answer 1

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:

1. 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.

2. 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.