We present a modular correspondence between various categorical structures and their internal languages in terms of extensional dependent type theories à la Martin-Löf. Starting from lex categories, through regular ones, we provide internal languages of pretopoi and topoi and some variations of them, such as, for example, Heyting pretopoi.With respect to the internal languages already known for some of these categories, such as topoi, the novelty of these calculi is that formulas corresponding to subobjects can be regained as particular types that are equipped with proof-terms according to the isomorphism ‘propositions as mono types’, which was invisible in previously described internal languages.

: We present and study the category of formal topologies and some of its variants. Two main results are proven. The first is that, for any inductively generated formal cover, there exists a formal topology whose cover extends in the minimal way the given one. This result is obtained by enhancing the method for the inductive generation of the cover relation by adding a coinductive generation of the positivity predicate. Categorically, this result can be rephrased by saying that inductively generated formal topologies are coreflective into inductively generated formal covers.The second result is that unary formal covers are exponentiable in the category of inductively generated formal covers and hence, thanks to the coreflection, unary formal topologies are exponentiable in the category of inductively generated formal topologies.From a localic point of view the exponentiability of unary formal topologies means that algebraic dcpos are exponentiable in the category of open locales. But, the coreflection theorem states that open locales are coreflective in locales and hence, as a consequence of well-known impredicative results on exponentiable locales, it allows to prove that locally compact open locales are exponentiable in the category of open locales.