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 questionprevious question.
