$\infty$-categorical interpretation of type theory

Question

One can read at several places that Martin-löf type theory should be the internal language of a locally Cartesian closed infinity category, and that the univalence axiom should distinguished infinity topos among locally Cartesian closed infinity categories. This is generally presented as a commonly accepted fact but not proven yet, for example, in the introduction of the HoTT book, one can read "in particular questions of coherence and strictness remains to be addressed"

Roughly,I would like to understand what are the difficulties for proving this (it seems to be an extremely natural result), or more precisely what does mean the sentence I quoted from the book ?

Thank you !

Answer 1

Mike Shulman has a good discussion of what exactly needs to be shown in his

• Michael Shulman, "The univalence axiom for inverse diagrams" (arXiv:1203.3253)

The issue is that in the type theory the classification of objects is by strict pullbacks. So roughly the problem is that one has to show the object classifier of a random $\infty$-topos is, when the latter is presented by a type-theoretic model category, presented by an object which classifies other objects by strict pullbacks with strict respect for composition. Establishing this in generality is (or would be) a kind of semi-strictification result for $\infty$-toposes.

See also the other references in the nLab entry.

Answer 2

More generally, the issue with such interpretation is that substitution in type theory is interpreted by pullback in category theory, and substitution in ordinary type theory preserves all type-theoretic operations strictly and functorially, so we need some model for an $(\infty,1)$-category in which pullback has these properties. This is the purpose of the various flavors of categorical models of dependent types that type theorists have developed, so what one needs is a coherence/strictification theorem for $(\infty,1)$-categories making them into such a structure.

A natural approach (for lots of reasons) is to start with a locally presentable $(\infty,1)$-category and present it by a suitable model category, take the display maps to be the fibrations, and then strictify it somehow. It's not too hard to show that a right proper Cisinski model category will give rise to the appropriate structure on these display maps, up to isomorphism, to model type theory. Cisinski and Gepner-Kock have shown that any locally presentable, locally cartesian closed $(\infty,1)$-category can be presented by some right proper Cisinski model category. Finally, a recent coherence theorem of Lumsdaine-Warren (still unpublished) applies to strictify this structure as necessary.

Thus, putting it all together, type theory (without universe types) admits a model in any locally presentable locally cartesian closed $(\infty,1)$-category. And it should probably be possible to remove the local presentability condition by passing to presheaf categories and then restricting the model to the representables. As Urs said, what remains to be done is to handle univalent universes, and there we have partial results only. (Higher inductive types are also not covered by the above sketch, but they should be handled by a forthcoming paper of Lumsdaine and myself.)

I would personally stop short of claiming yet that it is proven that homotopy type theory is "exactly the internal language of" locally cartesian closed $(\infty,1)$-categories, because for that I would want to have a complete functorial semantics in place. In particular, I would want it to be the case that the syntactic model of type theory is initial among locally cartesian closed $(\infty,1)$-toposes, and I don't think we know anything of that sort yet.