More generally, the issue with such interpretation is that substitution in type theory is interpreted by pullback in category theory, and substitution in ordinary type theory preserves all type-theoretic operations *strictly* and *functorially*, so we need some model for an $(\infty,1)$-category in which pullback has these properties. This is the purpose of the various flavors of categorical models of dependent types that type theorists have developed, so what one needs is a coherence/strictification theorem for $(\infty,1)$-categories making them into such a structure.

A natural approach (for lots of reasons) is to start with a locally presentable $(\infty,1)$-category and present it by a suitable model category, take the display maps to be the fibrations, and then strictify it somehow. It's not too hard to show that a right proper Cisinski model category will give rise to the appropriate structure on these display maps, up to isomorphism, to model type theory. Cisinski and Gepner-Kock have shown that any locally presentable, locally cartesian closed $(\infty,1)$-category can be presented by some right proper Cisinski model category. Finally, a recent coherence theorem of Lumsdaine-Warren (still unpublished) applies to strictify this structure as necessary.

Thus, putting it all together, type theory (without universe types) admits a model in any locally presentable locally cartesian closed $(\infty,1)$-category. And it should probably be possible to remove the local presentability condition by passing to presheaf categories and then restricting the model to the representables. As Urs said, what remains to be done is to handle univalent universes, and there we have partial results only. (Higher inductive types are also not covered by the above sketch, but they should be handled by a forthcoming paper of Lumsdaine and myself.)

I would personally stop short of claiming yet that it is proven that homotopy type theory is "exactly the internal language of" locally cartesian closed $(\infty,1)$-categories, because for that I would want to have a complete functorial semantics in place. In particular, I would want it to be the case that the syntactic model of type theory is initial among locally cartesian closed $(\infty,1)$-toposes, and I don't think we know anything of that sort yet.