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.

  • $\begingroup$ The 1-categorical presentation of the categorical semantics of cubical type theory is described in section 8 of hal.inria.fr/hal-01378906/document $\endgroup$
    – user40276
    May 30 '18 at 1:17
  • 3
    $\begingroup$ @user40276 I don't think that answers the question: that paper constructs one specific model in the category of cubical sets, whereas the question is about what general class of categories admit models. $\endgroup$ May 30 '18 at 16:29
  • 1
    $\begingroup$ @MikeShulman You're right. But I was not trying to answer the question. It's just the model of cubical sets. Now that I reread my comment, it's indeed ambiguous or even plainly wrong the way it's written. I should have said "One 1-categorical presentation..." instead. $\endgroup$
    – user40276
    May 31 '18 at 3:52

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.


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.

  • $\begingroup$ I'm having trouble parsing the paragraph starting "Like, when one says". Are you saying that the internal language conjecture asserts an equivalence between the homotopy category of the category of contextual categories and the homotopy category of the category of lccc $(\infty,1)$-categories? If so, I suppose that's one way to state it, although I think most people would prefer an equivalence between the $(\infty,1)$-category of contextual categories and the $(\infty,1)$-category of lccc $(\infty,1)$-categories. $\endgroup$ May 29 '18 at 17:56
  • 1
    $\begingroup$ The latter, for instance, is what Kapulkin and Szumilo obtain in the merely left-exact case in arxiv.org/abs/1709.09519, presenting these $(\infty,1)$-categories by fibration categories. $\endgroup$ May 29 '18 at 17:57
  • $\begingroup$ Of course, I entierely agree with you that an equivalence of $(\infty,1)$-category is preferable if you can get it. but the equivalence of homotopy categories already give you most of what you want. Regarding what statement between the equivalence of $(\infty,1)$-category and the equivalence of homotopy category is the closest to the informal claim that "some kind of type theory is the internal language of some kind of categories" I guess that's more of a philosophical question on which I'm not making any claim. $\endgroup$ May 29 '18 at 20:56
  • $\begingroup$ Well, you wrote "when one says ... it is a statement that compare a 'homotopy category'..." which seems to be making a claim that the informal statement always does refer to the homotopy-category-level version. $\endgroup$ May 29 '18 at 21:42
  • $\begingroup$ Well... maybe by "I'm not making any claim", I mostly meant "I think it is a terminology question and I don't care that much about this terminology". but of course you are absolutely right (and I've edited). $\endgroup$ May 30 '18 at 13:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.