Logicians and philosophers of science have proposed various formal criteria for theoretical equivalence. In this paper, we examine two such proposals: definitional equivalence and categorical equivalence. In order to show precisely how these two well-known criteria are related to one another, we investigate an intermediate criterion called Morita equivalence.

By a classifying topos for a first-order theory , we mean a topos such that, for any topos models of in correspond exactly to open geometric morphisms → . We show that not every first-order theory has a classifying topos in this sense, but we characterize those which do by an appropriate ‘smallness condition’, and we show that every Grothendieck topos arises as the classifying topos of such a theory. We also show that every first-order theory has a conservative extension (...) to one which possesses a classifying topos, and we obtain a Heyting-valued completeness theorem for infinitary first-order logic. (shrink)

We introduce a predicative version of topos based on the notion of small maps in algebraic set theory, developed by Joyal and one of the authors. Examples of stratified pseudotoposes can be constructed in Martin-Löf type theory, which is a predicative theory. A stratified pseudotopos admits construction of the internal category of sheaves, which is again a stratified pseudotopos. We also show how to build models of Aczel-Myhill constructive set theory using this categorical structure.