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.

1. Are two models of ETCS necessarily equivalent categories?

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

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

4. 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.

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.

1. Are two models of ETCS necessarily equivalent categories?

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

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

4. 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.

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.

1. Are two models of ETCS necessarily equivalent categories?

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

3. Is there a functor between any two models of ETCS? A span?

4. 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.

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.

1. Are two models of ETCS necessarily equivalent categories?

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

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

4. 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.