### A Dual for Set?

#### Posted by David Corfield

Our $n$Lab entry for ETCS has

The axioms of ETCS can be summed up in one sentence as:

$\bullet$ The category of sets is a well-pointed topos with a natural numbers object satisfying the axiom of choice.

Do we take then models of ETCS as forming the 2-category of well-pointed toposes with a natural numbers object satisfying the axiom of choice? And is $Set$ initial in this 2-category? If so, is it then an initial (2)-algebra of sorts? And if all that, is there an analogue terminal (2)-coalgebra?

I know about the idea of well-founded and non-well-founded sets as minimal and maximal fixed points for the powerset functor on the category of classes, as in algebraic set theory. I was wondering if there is something similar going on in a structural set theory such as ETCS.

Posted at October 14, 2009 3:10 PM UTC
## Re: A Dual for Set?

That’s certainly reasonable. Although you have to specify what the morphisms and 2-cells are. There are two obvious choices for morphisms between toposes: geometric morphisms and logical functors. Probably logical functors is what you want in this context. And I think there are various reasons why noninvertible transformations between logical functors aren’t well-behaved, so probably this is really only a (2,1)-category, but that’s okay.

I’m almost positive the answer is “no.” Presumably in order to ask this question, you have some ambient set+class theory in which you can define the 2-category of all (possibly large) models of ETCS in such a way that it contains the category $Set$ of (small) sets. Now usually the initial object in a (2-)category of toposes is a “free topos” or “term model,” so if this 2-category has an initial object I would expect it to be of that sort. (I’m actually doubtful that it even has an initial object, since well-pointedness and choice aren’t obviously expressible in the type-theoretic form used for constructing a free topos.)

Moreover, there are also plenty of

smallmodels of ETCS, and it seems pretty unreasonable to expect a logical functor from $Set$ to a small topos. Note that free toposes are countable, since they’re built out of logical terms, but also for instance the category of sets of cardinality $\lt \beth_\omega$ is a small model of ETCS (as long as your ambient theory is strong enough to define $\beth_\omega$).It is true that $Set$ is initial in the 2-category of

cocompletemodels of ETCS—but that’s because (up to equivalence) it’s theonlyobject of that 2-category!