How much homotopy type theory should be modeled by the unstable motivic category? 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 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? 
 A: 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.
