Mathematical Structures in Computer Science


Modular correspondence between dependent type theories and categories including pretopoi and topoi

a1 Dipartimento di Matematica Pura ed Applicata, Università di Padova, via G. Belzoni n. 7, I-35131 Padova, Italy Email:

Article author query
maietti me   [Google Scholar] 


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.

(Published Online December 8 2005)
(Received January 26 2004)
(Revised May 3 2005)