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.

"non-standard" homotopy? – François G. Dorais♦ Jul 11 '13 at 14:54