“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 (if you’re working over ZFC or similar) 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.

“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.