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.