Can we define geometric morphisms (between ETCS categories) elementarily?

The ETCS axioms give conditions on a category for it to be a category of sets. These axioms can be written out in first order language, resulting in a finite axiomatisation of the category of sets. Given a model of ZFC one can form the associated category of sets and this will satisfy the axioms. On the other hand, the axioms do not require a priori defined sets. (The existence of a model of the ETCS axioms then is probably on par with the assuption there exists a model of the ZFC axioms) The appropriate definition of map between ETCS categories is a geometric morphism.

Is it possible to define geometric morphisms elementarily? In first order language?

Then one can define the category of ETCS categories and consider the relations between models. This is related to my previous question.

• Absolutely! But tbh, it's probably overkill. To do basic model theory of any first-order logical system, assuming you want the usual completeness theorem and things, your minimal metatheory is probably something like ZC (I don't believe you need replacement, though I wouldn't swear to this); a reverse-mathematician could surely sharpen this up a bit. If you want to prove existence of models, then replacement is enough: sets of cardinality bounded by any strong limit cardinal (eg $2^{2^{\ddots ^ \omega}}$) give a model of bounded Zermelo set theory, and hence of ETCS. (cont’d) – Peter LeFanu Lumsdaine Oct 20 '10 at 2:41