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?

isan infinity topos: Raptis & Strunk, " Model topoi and motivic homotopy theory". I guess it's an open question as to whether their variant is a good replacement for the usual motivic category. $\endgroup$ – Charles Rezk Jun 25 '18 at 17:21