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. 
 A: 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.
A: 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.
