Are there any models of Martin-Löf's intensional type theory in which univalence or function extensionality fails?
In the HoTT book, axioms like $\mathsf{LEM}_{\infty}$ (in Section 3.4) are proved to be inconsistent with univalence. I suppose that there might be some models in which univalence fails and such axioms hold, which is interesting.
Thanks.
“HoTT” isn’t generally currently considered as referring to a single specific formal system — it’s a similar situation to, say, “constructive mathematics”, for which there are various different more or less well-studied formal systems.
The core of most systems currently used for HoTT is Martin-Löf’s intensional type theory, ITT, usually also with funext. This is agnostic on homotopical questions: it has both the simplicial set model, where univalence holds, and the good old-fashioned set model, where UIP holds (“uniqueness of identity proofs” — in HoTT terminology, the statement/scheme asserting that every type is a set), and (at least as long as you’re working with ZFC or similar as your background foundation) LEM∞ holds as well. So in this case, LEM∞ certainly can hold — but it’s not what one would usually call a model of HoTT.
On the other hand, you might mean a stronger system — ITT augmented with some homotopical axioms, like univalence. In this case, because of the results you mention, there can’t be any model where LEM∞ holds.
One reasonable in-between thing one might mean by “models of HoTT” would be: models of ITT in which UIP doesn’t hold, i.e. models which are “homotopically non-trivial”. For this sense, the answer to your question is no, LEM∞ can’t hold in such models, since Hedberg’s Theorem shows that LEM∞ implies UIP, so any model of ITT + LEM∞ is homotopically trivial.
