Are there any models of Martin-Löf's intensional type theory in which univalence or function extensionality fails?


In the [HoTT book](https://homotopytypetheory.org/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 without Funext, Univalence
“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](https://homotopytypetheory.org/2012/03/30/a-direct-proof-of-hedbergs-theorem/) shows that LEM∞ implies UIP, so any model of **ITT** + LEM∞ is homotopically trivial.


