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, 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, 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 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).
Let be a locally small, well-pointed topos (such as a locally small model of ETCS); the following are equivalent.
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 is monadic over (via the contravariant powerset functor). Thus, it remains to prove that 2 implies 1. So suppose that admits coproducts indexed by its homsets. In particular, for any we can form the coproduct , which of course comes with a canonical map to . This map is a bijection on global elements, so since is well-pointed, it is an isomorphism.
Consider the “global sections” functor . Well-pointedness implies that this functor is faithful and conservative. However, since by the above we have , it follows that is full as well, so that is equivalent to a full subcategory of . From now on we identify it with its essential image.
Let and suppose that is a subset of . By assumption on , it admits the coproduct where is if and otherwise. But this coproduct maps to via a bijection on global elements as before, so it is an isomorphism, and thus as well. Hence is closed in under subsets. It follows that the full inclusion 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 -set of -sets is again an -set.
If is essentially small, then these properties imply that it must be a Grothendieck universe. If is large, then it contains sets of arbitrarily large cardinality, hence (by closure under subsets) it contains sets of all cardinalities—thus it is all of .
(We have proven the axioms of a universe in a “structural” form. We can alternately directly construct an inaccessible cardinal such that is the category of sets in . We argue as before that is a full subcategory of , and let be the smallest cardinal number not the cardinality of a set in ; it follows that consists precisely of the sets of cardinality . Since is a topos with a NNO, must be an uncountable strong limit?. Finally, if and for each , then , showing that is regular, and hence inaccessible.)
is, up to equivalence, the unique locally small and cocomplete well-pointed topos (hence the unique locally small and cocomplete model of ETCS), and the unique locally small and complete well-pointed topos (hence the unique locally small and complete model of ETCS).
Since the category of sets in some Grothendieck universe does not admit all small coproducts (for instance, not those of the size of the universe itself), if any of the equivalent statements the theorem hold for some cocomplete topos, that topos must be all of Set.
A more direct proof of the corollary is possible.
We show as in the theorem that is a full inclusion. Cocompleteness of then shows that it has a left adjoint given by , so it suffices to show that the unit of this adjunction is a bijection.
For injectivity, we need to show that if , then . If , then since coproducts in a topos are disjoint, the pullback of and is the initial object . But since , their pullback is also . By well-pointedness, is not isomorphic to , so by contradiction, .
For surjectivity, we need to show that any map is equal to for some . Now for each , the pullback of and is a subobject of 1, call it . Since a well-pointed topos is two-valued, every must be unless some is . Since coproducts in a topos are stable under pullback, . But then if for every , we would have , contradicting well-pointedness. Thus there must be an with , which implies that .
In constructive mathematics, is not a model of , but it is a model of the intuitionistic version? thereof – that is, it is a (constructively) well-pointed topos with a NNO. It is also locally small, complete and cocomplete.
However, the above theorem and corollary both fail intuitionistically, at least as stated above. The proof of the theorem goes through up to the point where we identify with a full subcategory of . The next paragraph, however, proves only that is closed under indexed unions and detachable subsets (more precisely, under subsets whose characteristic function lands in the set of truth values belonging to — whereas for arbitrary , the only truth values we can be sure belong to are “true” and “false”).
Depending on how we choose to define “Grothendieck universe” intuitionistically, this may imply that if is essentially small then it is a Grothendieck universe. However, it definitely does not follow intuitionistically that if is large, it must be all of ; the argument for this in the classical case implicitly uses the axiom of choice in the guise of the well-ordering (or at least total ordering) of cardinal numbers.
In particular, the corollary fails to hold intuitionistically. A concrete weak counterexample (which can be made into a strong counterexample by working internally to some topos) is given by the following.
Let be a truth value (identified with the subset ) such that is valid and is indecomposable and projective, and let be the topos . Then 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 .
Note that in this example, the “global sections” functor is not the forgetful functor (which doesn’t even preserve the terminal object), but the exponential functor . This is the direct image functor in the geometric morphism , whereas the obvious forgetful functor is the left adjoint to the inverse image functor that exhibits as a locally connected topos.