It's often said that homotopy type theory should be interpretable in any $\infty$-topos. But really it should be interpretable in any "predicative $\infty$-topos". I'm not quite sure what this means, but the prime example to me of an $\infty$-category which is "almost, but not quite, an $\infty$-topos" is the unstable motivic category $H(S)$ over a base scheme $S$.


The category $H(S)$ is locally cartesian closed, and locally presentable so that it presumably has any kind of higher inductive type one could want. I think it doees not have a subobject classifier, but probably that just means that it won't admit propositional resizing.


The failure of $H(S)$ to be an $\infty$-topos [can be seen](https://mathoverflow.net/a/294031/2362) in the fact that $\Omega B$ is not the identity on grouplike $A\_\infty$ objects, where $B$ is the bar construction; in particular, colimits indexed by $\Delta^{op}$ are not van Kampen. I'm not sure what to make of this type-theoretically, since it's not clear how to even define what a simplicial object is, let along an $A\_\infty$ object. Should one expect that, given a definition of $A\_\infty$ object in HoTT, it will be the case that every grouplike $A\_\infty$ space is a loopspace, as is the case in any $\infty$-topos? Or would that be a statement analogous to Whitehead's theorem, not expected to hold in all models?


If we assume arbitrarily large Grothendieck universes, then I would have to think that $H(S)$ will admit type-theoretic universes. But perhaps they won't be univalent? 



How much homotopy type theory should be modeled by the unstable motivic category?
When you say "really it should be interpretable in any predicative $\infty$-topos", well it depends on what you mean by "homotopy type theory". Homotopy type theory is not a fixed system, but a subject that studies many different type theories. Some of those are conjectured to correspond to $(\infty,1)$-toposes, others to predicative variants, and so on.


One of the most precise statements we know is that any locally cartesian closed locally presentable $(\infty,1)$-category can be presented by a "$\Pi$-tribe" that has various kinds of higher inductive types. The latter is the conjectural semantics of Martin-Lof type theory with function extensionality and HITs, but no universes at all.


I don't know the details of in what cases a non-univalent universe can be constructed. There are various problems with making a universe (of any kind) sufficiently strict to correspond to a type-theoretic universe, but if we ignore those, then it seems possible that a non-univalent universe could be constructed in many models. I don't know anything about the motivic category, but it could well be such a model.


A subobject classifier is, in addition to propositional resizing, a univalent universe of $(-1)$-types. So this is part of the same problem. Predicativity is basically about propositional resizing or not, but in the absence of univalence the problems are more basic; even a "predicative $(\infty,1)$-topos" should satisfy univalence.


Univalence of the universe corresponds fairly closely to having colimits satisfying descent, or which are "van Kampen". It's not necessary to mess around with simplicial objects and $A\_\infty$ stuff; as Christian Sattler recently reminded me, by Remark 6.1.3.11 of *Higher Topos Theory*, a locally cartesian closed locally presentable $(\infty,1)$-category is an $(\infty,1)$-topos as soon as *pushouts* are van Kampen. This property is certainly visible in the finitary syntax of type theory, even in the absence of a universe; it means that HIT pushouts (and other HITs as well) satisfy a "univalence-inspired large elimination rule". Of course if there is a univalent universe, then such a rule is derivable, but in the absence of a universe it can be postulated separately, and I believe that if there is a (not known to be univalent) universe then this elimination rule turns out to be equivalent to univalence of that universe.


So I think the answer to your question is that such a category models a version of homotopy type theory with $\Sigma, \Pi, \mathrm{Id}$ types, with function extensionality, and higher inductive types *without* large elimination rules, and (possibly) non-univalent universes.


