EDIT: What follows is true for extensional MLTT. If you add univalence to intensional MLTT, all of this goes out the window. It is conjectured that you can replace "locally cartesian closed category" with "locally cartesian closed infinity categeory" and similarly for toposes and everything will work out.
It can be proved that every topos is locally cartesian closed, and that models of MLTT are precisely the locally cartesian closed categories. The syntactical model of MLTT, i.e. the model built from well-formed types and terms, is the initial model of MLTT, and hence also the initial locally cartesian closed category. The unique functor induced by initiality assigns each valid term in MLTT a morphism in some given locally cartesian categor, which can be seen as recovering intuitionistic proofs from MLTT because toposes are locally cartesian closed.
It is not true that MLTT universes are always toposes though. They are not always cocomplete and need not have a subobject classifier. A consequence is that MLTT does not have proper existential quantifiers (despite what the article claims) because Σ_(x : A) B(x) carries proofs of B(x) along with elements x. It is thus not true that Σ_(x : A) B(x) is a subset of A, which one would expect from existential quantification.
MLTT corresponds to a weaker logic than the more usual intuitionistic one: Sequents in the former make sense in the latter, but not necessarily conversely.
Oh, and maybe there is a slight misconception in your last paragraph: Universes in MLTT are not the same thing as models of MLTT. Models of MLTT are something you talk about from externally of MLTT, from a metatheoretical viewpoint. The universes in the HoTT sense are internal to the logic.
It can be proved that every topos is locally cartesian closed, and that models of MLTT are precisely the locally cartesian closed categories. The syntactical model of MLTT, i.e. the model built from well-formed types and terms, is the initial model of MLTT, and hence also the initial locally cartesian closed category. The unique functor induced by initiality assigns each valid term in MLTT a morphism in some given locally cartesian categor, which can be seen as recovering intuitionistic proofs from MLTT because toposes are locally cartesian closed.
It is not true that MLTT universes are always toposes though. They are not always cocomplete and need not have a subobject classifier. A consequence is that MLTT does not have proper existential quantifiers (despite what the article claims) because Σ_(x : A) B(x) carries proofs of B(x) along with elements x. It is thus not true that Σ_(x : A) B(x) is a subset of A, which one would expect from existential quantification.
MLTT corresponds to a weaker logic than the more usual intuitionistic one: Sequents in the former make sense in the latter, but not necessarily conversely.
Oh, and maybe there is a slight misconception in your last paragraph: Universes in MLTT are not the same thing as models of MLTT. Models of MLTT are something you talk about from externally of MLTT, from a metatheoretical viewpoint. The universes in the HoTT sense are internal to the logic.