What kind of category is generated by Cubical type theory?

Question

What kind of ‘category’ is Cubical type theory the internal language of?

Its known that Martin-Löf type theories are the internal language of Locally cartesian closed categories, adding higher inductive types you get the internal language of locally cartesian closed $(\infty , 1)$-categories, a.k.a HoTT without Univalence. And as far as I know, it is suspected that plain HoTT is the internal language of whatever an $(\infty , 1)$-topos is.

Cubical type theory doesn’t quite fit into this sequence of type theories but it is surprisingly good at modelling HoTT. It is a strange kind of type theory in that it uses De Morgan algebras to reason about cubes but non the less it begs the question: What kind of category does it generate?

I suspect the answer to this question isn’t known, however I would be more than happy to see peoples suspicions.

Answer 1

There are two kinds of answers as to what kind of category a "homotopy type theory" is the internal language of. On the one hand there is a kind of $(\infty,1)$-category that is the semantic object of real interest; but on the other hand there is a 1-categorical presentation of the latter that corresponds more closely to the syntax of the type theory. The latter kind of category (whose variants go by names like "contextual category", "category with families", "category with attributes", "type-theoretic fibration category", "tribe", etc.) is also closely related to the model categories and fibration categories used to present $(\infty,1)$-categories in classical abstract homotopy theory.

For instance, HoTT with $\mathrm{Id},\Sigma,\Pi$ and function extensionality, but no universes, corresponds (conjecturally) to locally cartesian closed $(\infty,1)$-categories — presented by means of "$\Pi$-tribes" (or whatever other name you prefer for the latter).

Cubical type theory is a syntactic variation which changes the corresponding 1-categorical presentations, but not the desired $(\infty,1)$-categorical semantics. That is, the analogous cubical type theory, with $\mathrm{Id},\Sigma,\Pi$ (and, in the cubical case, provable function extensionality), but no universes, also corresponds (conjecturally) to locally cartesian closed $(\infty,1)$-categories, but now presented in a different way by $\Pi$-tribes containing (or more precisely, fibered over the theory of) some kind of "interval object". There is a sketch of the latter kind of category (for a more general kind of "type theory with shapes") in appendix A of https://arxiv.org/abs/1705.07442.

Answer 2

I would say that the question is not even well defined.

Saying that Martin löf type theory with extensional identity types is the internal language of cartesian closed categories with natural number objects is a rather clear formal statement: you are saying that some $2$-category of contextual categories with additional structure corresponding to Martin löf type theory is equivalent to a $2$-category of cartesian closed categories with natural number objects.

Note that even at this level, one only have a $2$-equivalence of (strict) $2$-categories, this is not an equivalence of the $1$-categories.

When you move to $\infty$-categorical statement there is a new difficulty: you are comparing $\infty$-categories:

For example, when one says that Martin löf type theory with intentional identity type is the internal language of cartesian closed $(\infty,1)$-categories with natural number objects (not proved yet), it is a statement that compare a "homotopy category", (or a Dwyer-Kan localization) of contextual categories with the structure corresponding to Martin löf type theory, to some homotopy category (or $\infty$-category) of cartesian closed $(\infty,1)$-category.

In general those homotopy category (or $\infty$-category) are defined as ordinary $1$-category, localized at some class of weak equivalences.

(I recomend this paper of Lumsdain and Kapulkin for a very nice and precise formulation of this)

To come back to your question, if one start with cubical type theory, it is rather clear what is the underlying $1$-category (although probably a pain to state or to prove): it is some kind of contextual category with additional structures corresponding to the axioms of cubical type theory, but it is very unclear what should be the weak equivalences between them, and hence what should be the corresponding 'homotopy category' or $\infty$-category that we want to compare to some other homotopy/$\infty$-category of $\infty$-categories with certain structures/properties, or even if you want to see it as $2$-category and so one.

Depending on the choice of weak equivalences, one could get very different answer to that question (so you might get precise answer to your question after all, just probably not a unique one)

For example, one could imagine a notion of weak equivalences that completely ignore the cubical aspect, and which would provide an equivalence with some notion of $(\infty,1)$-topos.

Or one could take a more restricted notion of weak equivalences that see the cubical aspect and say that cubical type theory is the internal language of some kind of cubical fibrations category satisfying some additional axiom in the spirit of model toposes.