# Are simplicial sets the intended model of HoTT?

While thinking about Jason Rute's question, I wondered if there was an intended model for HoTT. The main candidate for the intended model are simplicial sets, where Vladimir Voevodsky first observed the univalence phenomenon. However, it is not clear that HoTT is intended to describe this model as opposed to groupoid models or a broader class of models.

A related question is whether there is a notion of standard model for HoTT. That is, a notion comparable in role to ω-models for second-order arithmetic and transitive/well-founded models for set-theory.

-
Is it clear that HoTT has an intended model? My vague impression is that HoTT can serve as an internal language for various kinds of higher categories and that it wasn't intended to describe just one such category. –  Qiaochu Yuan Jul 11 '13 at 1:49
No, that's the first question. If there is an intended model it's surely simplicial sets. –  François G. Dorais Jul 11 '13 at 1:52
I'll add my standard comment that things have been done in homotopy theory with cubical sets (with connections) and also with $n$-fold groupoids, which have not been achieved with simplicial sets, mainly because of the ease of considering multiple compositions. Could this have implications for HoTT? –  Ronnie Brown Jul 11 '13 at 10:39
@RonnieBrown: I think so. It is clear that there are variants of identity types which give slightly different higher-dimensional structure. The standard identity types naturally lead to globular structure, but one can imagine $n$-fold identity types that will make things look more like simplices. I think some people are experimenting, but it's hard to replace an entrenched theory. I think similar situation arises with "non-standard" homotopy. –  Andrej Bauer Jul 11 '13 at 11:25
@Andrej: In your last sentence, do you mean something specific by "non-standard" homotopy? –  François G. Dorais Jul 11 '13 at 14:54

My impression is as follows.

While I cannot speak for Voevodsky, he certainly gives the impression that simplicial sets is his favorite, if not the intended model. For example, he would suggest axioms on the basis of them being valid in simplicial sets (such as excluded middle for mere propositions).

If one takes HoTT as the internal language of something, then the something will be something like $(\infty, 1)$-toposes, but this has not been worked out yet in precise detail. This point of view will probably appeal to categorical logicians and others close to category theory. One certainly would not worry about the intended model under this view.

Classical first-order logic and model theory often use the concept of "standard model" or "intended model", despite the fact that many results explain that belief in such a model requires a certain amount of blind faith (for example, faith in ones own mathematical instinct). I find it intriguing that Martin-Löf also seems to have an intended model of his theory. He talks about it explicitly. So even though many participants of the HoTT project are of the categorical kind, others are of a more orthodox type-theoretic kind. My impression is that for them a more profound foundational shift is hapenning with HoTT. One consequence of this is the urgency to resolve the computational content of the Univalence axiom, without which the axiom is the forbidden fruit.

During the Univalent year at the Institute for Advanced Study there were several discussions where the two views arose in opposition to each other. This was a very fruitful situation, as it made everyone think harder. When we wrote the book, we decided at a very early stage not to speak about models or other "meta" topics, such as the meta properties of the underlying type system. After all, if HoTT aspires to be a foundation of mathematics, then it cannot place itself on top of any notion outside HoTT. It must build directly on top of reader's premathematical knolwedge. At the same time, it has to respect existing informal mathematical tradition as much as possible, or else it is just a logicians' hobby.

Thus, while the question of the intended or standard model is important, I think it is perhaps not the right question to ask about a proposed new foundation, because it immediately makes it harder to take the new system at face value, directly and not through the eyes of a logician. I understand of course the logician's urge to view the landscape from the meta-level, and it is good that there are such people (me being one of them). My point is that to understand the intent and the value of a new foundation one actually has to descend and truly live with it for a while, to see what sort of mathematical intuitions it begets. I think anthropologists could teach us a lesson.

-
An intended model for HoTT seems like a rather sad idea. It's like the Vikings discovering America but then rather intending to go back home after all. –  Urs Schreiber Jul 11 '13 at 12:25
Thanks, Andrej! This confirms some of my initial impressions. Regarding the categorical logic perspective, despite the fact that this hasn't been fully worked out, is there a clear feeling what the intended class of models is from that point of view? Are all $(\infty,1)$-toposes univalent? –  François G. Dorais Jul 11 '13 at 13:22
No, no, it seems that one has to work to get univalence. At present we lack techniques to fabricate univalent models of various kinds. But if we discount univalence, there is still the question on how type theory and higher toposes fit together. –  Andrej Bauer Jul 11 '13 at 16:38
This is a much fairer and more even-handed answer than I would have been able to give. (-: Personally, despite those long and thought-provoking discussions at IAS, I am still surprised that in the 21st century anyone uses the phrase "intended model" any more. Are the integers the "intended abelian group"? –  Mike Shulman Jul 11 '13 at 22:18
@FrançoisG.Dorais, I would say that yes, absolutely, all $(\infty,1)$-toposes are univalent. The problem is to find definitions of "$(\infty,1)$-topos" and "univalent" which make this true, but this is only a technical problem --- intuitively, we have a pretty good idea of what both mean. It's true that at present we don't know how to model the usual strict form of univalence in all Grothendieck $(\infty,1)$-toposes (which are the only ones that have a precise definition at the moment), but there are weaker forms of univalence that do hold. –  Mike Shulman Jul 11 '13 at 22:21

Of course questions of intent don't really have well-defined answers, but I think that there are two reasonable points of view. One is that HoTT should be the correct internal language for any higher topos in the sense of Lurie, or something like that. This should cover many different Quillen model categories, of which simplicial sets are only the simplest example. The other point of view is that HoTT aims to be an alternative foundation for homotopy theory and mathematics in general, in which case models are only important as relative consistency proofs rather than as the main point of the theory.

-
I agree in general, but disagree that models are only good for relative consistency proofs. They have many more uses than that. –  Andrej Bauer Jul 11 '13 at 8:34
When you say that HoTT should be the correct internal language for higher topos, do you include univalence or do you just mean the homotopy interpretation of identity types? –  François G. Dorais Jul 11 '13 at 14:22