nLab
cocomplete well-pointed topos

The category of sets is, among other things, a well-pointed topos with a natural numbers object satisfying the axiom of choice—i.e. a model of ETCS. However, $\mathrm{Set}$ cannot be characterized uniquely by this or any other elementary property, i.e. by a property that doesn’t refer, explicitly or implicitly, to the notion of set. This is a version of Gödel’s incompleteness theorem?.

However, $\mathrm{Set}$ can be characterized uniquely by the addition of non-elementary categorial properties, the most notable and obvious of which are completeness and cocompleteness. On the other hand, it is also true that any topos is complete and cocomplete relative to itself, in the sense that its self-indexing? is complete and cocomplete as an indexed category?. Thus, in order to characterize $\mathrm{Set}$ in this way we have to mean “external” completeness and cocompleteness (which is the intuitive notion of completeness, in the context of some notion of set).

Theorem

Let $S$ be a locally small model of ETCS; the following are equivalent.

1. $S$ is equivalent either to $\mathrm{Set}$ or to the category of sets in some Grothendieck universe.
2. $S$ admits all coproducts indexed by its own homsets.
3. $S$ admits all products indexed by its own homsets.

Proof

The implications from 1 to 2 and 1 to 3 are easy exercises, following from the “second-order replacement axiom” of a Grothendieck universe. And the implication from 3 to 2 follows because any topos which has some type of limit automatically also has the same sort of colimit, because $S^{\mathrm{op}}$ is monadic over $S$ (via the contravariant powerset functor). Thus, it remains to prove that 2 implies 1. So suppose that $S$ admits coproducts indexed by its homsets. In particular, for any $X\in S$ we can form the coproduct ${\coprod }_{x:1\to X}1$, which of course comes with a canonical map to $X$. This map is a bijection on global elements, so since $S$ is well-pointed, it is an isomorphism.

Consider the “global sections” functor $\Gamma =S(1,-):S\to \mathrm{Set}$. Well-pointedness implies that this functor is faithful and conservative. However, since by the above we have $X\cong {\coprod }_{\Gamma (X)}1$, it follows that $\Gamma$ is full as well, so that $S$ is equivalent to a full subcategory of $\mathrm{Set}$. From now on we identify it with its essential image.

Let $X\in S$ and suppose that $Y\subset X$ is a subset of $X$. By assumption on $S$, it admits the coproduct ${\coprod }_{x:1\to X}{Z}_x$ where $Z_x$ is $1$ if $x\in Y$ and $\varnothing$ otherwise. But this coproduct maps to $Y$ via a bijection on global elements as before, so it is an isomorphism, and thus $Y\in S$ as well. Hence $S$ is closed in $\mathrm{Set}$ under subsets. It follows that the full inclusion $S\hookrightarrow \mathrm{Set}$ is a bijection on subobject lattices, and thus a logical functor (preserves power objects). Finally, the hypothesis on coproducts implies that the union of an $S$-set of $S$-sets is again an $S$-set.

(We have proven the axioms of a universe in a “structural” form. We can alternately directly construct an inaccessible cardinal such that $S$ is the category of sets in $V_{\kappa }$. Let $\kappa$ denote the smallest cardinal number not in $S$, it follows that $S$ consists precisely of the sets of cardinality $<\kappa$. Since $S$ is a topos with a NNO, $\kappa$ must be an uncountable strong limit. Finally, if $X\in S$ and $Y_x\in S$ for each $x\in X$, then ${\coprod }_{x:1\to x}{Y}_x\in S$, showing that $\kappa$ is regular, and hence inaccessible.)

Corollary

$\mathrm{Set}$ is, up to equivalence, the unique locally small and cocomplete model of ETCS, and the unique locally small and complete model of ETCS.

A more direct proof of the corollary is possible.

Proof

We show as in the theorem that $\Gamma$ is a full inclusion. Cocompleteness of $S$ then shows that it has a left adjoint given by $X\mapsto {\coprod }_{X}1$, so it suffices to show that the unit $X\to S(1,{\coprod }_{X}1)$ of this adjunction is a bijection.

For injectivity, we need to show that if $j_x=j_y$, then $x=y$. If $x\ne y$, then since coproducts in a topos are disjoint, the pullback of $j_x$ and $j_y$ is the initial object $0$. But since $j_x=j_y$, their pullback is also $1$. By well-pointedness, $0$ is not isomorphic to $1$, so by contradiction, $x=y$.

For surjectivity, we need to show that any map $k:1\to {\coprod }_{X}1$ is equal to $j_x$ for some $x$. Now for each $x$, the pullback of $k$ and $j_x$ is a subobject of 1, call it $U_x$. Since a well-pointed topos is two-valued, every $U_x$ must be $0$ unless some $U_x$ is $1$. Since coproducts in a topos are stable under pullback, $1={\coprod }_X{U}_x$. But then if $U_x=0$ for every $x$, we would have $1={\coprod }_{X}0=0$, contradicting well-pointedness. Thus there must be an $x$ with $U_x=1$, which implies that $k=j_x$.

Intuitionistic Failure

This theorem, and even the corollary, fail intuitionistically, as may be suspected from the use of excluded middle in their proofs. A concrete counterexample is given by the following.

Let $𝒰$ be a truth value (identified with the subset $\{\star \mid 𝒰\}\subseteq \{\star \}=1$) such that $\neg \neg 𝒰$ is valid and $𝒰$ is indecomposable and projective, and let $S$ be the topos $\mathrm{Set}/𝒰$. Then $S$ is a Grothendieck topos, hence cocomplete and locally small, and the assumptions on $𝒰$ ensure that it is well-pointed, but in an intuitionistic theory they don’t imply that $𝒰=\top$.