  We prove the conjecture that any Grothendieck $(\infty,1)$-topos can be
presented by a Quillen model category that interprets homotopy type theory with
strict univalent universes. Thus, homotopy type theory can be used as a formal
language for reasoning internally to $(\infty,1)$-toposes, just as higher-order
logic is used for 1-toposes. As part of the proof, we give a new, more
explicit, characterization of the fibrations in injective model structures on
presheaf categories. In particular, we show that they generalize the coflexible
algebras of 2-monad theory.
