Toposes and intuitionistic theories of types (Q1115435): Difference between revisions

It is by now well-known that intuitionistic (higher-order) type theories correspond to toposes, in the sense that every such theory is ``embodied'' in a topos, and every topos has a canonical theory of which it is (equivalent to) the embodiment. The aim of this paper is to introduce a notion of translation of theories which makes this correspondence into an equivalence of categories, when arbitrary left exact functors are taken as the morphisms between toposes. (Previous authors had considered a more ``rigid'' notion of translation corresponding to logical functors between toposes.) Indeed, the correspondence becomes an equivalence of 2-categories, since the authors also introduce ``comparisons'' of interpretations which correspond to natural transformations between left exact functors.