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.
Best Answer
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.