How do we compare models of ETCS? The elementary theory of the category of sets (nLab) gives axioms on a category such that it is a category of sets. In answering this MO question I realised that we might have trouble comparing different models of ETCS. So here are some questions starting with easy ones (which I should know the answer to!) to the more difficult.


*

*Are two models of ETCS necessarily equivalent categories?

*Are two models of ETCS equivalent as well-pointed topoi with NNO and Choice?

*Is there a functor (Edit: a logical functor, as Todd pointed out) between any two models of ETCS? A span?

*Do models of ETCS necessarily even belong to the same category?
I wonder, because the sets that one model of ETCS has as hom-objects may be completely different to the sets that the other model has as hom-objects, and there is a priori no way to map between them.
 A: (Caveat: I come from set theory rather than category theory and know only a little about ETCS.)
The answer to your question is no. The basic reason is that even the models
of set theory themselves can differ vastly. If $M$ is a
model of ZFC, then the category $Set^M$, which is Set as
interpreted in $M$, will be a model of ETCS. But if ZFC is
consistent, then the models of set theory $M$ are diverse.
For example, some have CH and others have $\neg CH$, and
furthermore, by the incompleteness theorem, they can
satisfy different arithmetic statements. Such statements
show up in the category $Set^M$, since every
arithmetic statement (first order statement about natural
numbers) has a translation into the formal language of
ETCS. So in general these categories are not elementary equivalent in the language of ETCS. In particular, the natural numbers objects of such categories will not in general be isomorphic, and so there can be no nice functors between the categories. For example, by the Lowenheim-Skolem theorem, some models of set theory will be countable and others will have an uncountable set of natural numbers, with a different theory, and these aspects will prevent their corresponding Set categories from being equivalent as categories or from having nice functors. In
general, it will not be possible to map the natural number
object from one to the other in any nice way.
