nLab cocomplete well-pointed topos

The (co)complete, locally small, well-pointed topos

The (co)complete, locally small, 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, SetSet 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, SetSet 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 SetSet 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 SS be a locally small, well-pointed topos (such as a locally small model of ETCS); the following are equivalent.

  1. SS is equivalent either to SetSet or to the category of sets in some Grothendieck universe.
  2. SS admits all coproducts indexed by its own homsets.
  3. SS admits all products indexed by its own homsets.

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 opS^{op} is monadic over SS (via the contravariant powerset functor). Thus, it remains to prove that 2 implies 1. So suppose that SS admits coproducts indexed by its homsets. In particular, for any XSX\in S we can form the coproduct x:1X1\coprod_{x\colon 1\to X} 1, which of course comes with a canonical map to XX. This map is a bijection on global elements, so since SS is well-pointed, it is an isomorphism.

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

Let XSX\in S and suppose that YXY\subset X is a subset of XX. By assumption on SS, it admits the coproduct x:1XZ x\coprod_{x\colon 1\to X} Z_x where Z xZ_x is 11 if xYx\in Y and \emptyset otherwise. But this coproduct maps to YY via a bijection on global elements as before, so it is an isomorphism, and thus YSY\in S as well. Hence SS is closed in SetSet under subsets. It follows that the full inclusion SSetS\hookrightarrow 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 SS-set of SS-sets is again an SS-set.

If SS is essentially small, then these properties imply that it must be a Grothendieck universe. If SS 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 SetSet.

(We have proven the axioms of a universe in a “structural” form. We can alternately directly construct an inaccessible cardinal such that SS is the category of sets in V κV_\kappa. We argue as before that SS is a full subcategory of SetSet, and let κ\kappa be the smallest cardinal number not the cardinality of a set in SS; it follows that SS consists precisely of the sets of cardinality <κ\lt\kappa. Since SS is a topos with a NNO, κ\kappa must be an uncountable strong limit. Finally, if XSX\in S and Y xSY_x \in S for each xXx\in X, then x:1XY xS\coprod_{x\colon 1\to X} Y_x\in S, showing that κ\kappa is regular, and hence inaccessible.)


SetSet 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 Γ\Gamma is a full inclusion. Cocompleteness of SS then shows that it has a left adjoint given by X X1X\mapsto \coprod_X 1, so it suffices to show that the unit XS(1, X1)X\to S(1,\coprod_X 1) of this adjunction is a bijection.

For injectivity, we need to show that if j x=j yj_x=j_y, then x=yx=y. If xyx\neq y, then since coproducts in a topos are disjoint, the pullback of j xj_x and j yj_y is the initial object 00. But since j x=j yj_x=j_y, their pullback is also 11. By well-pointedness, 00 is not isomorphic to 11, so by contradiction, x=yx=y.

For surjectivity, we need to show that any map k:1 X1k\colon 1\to \coprod_X 1 is equal to j xj_x for some xx. Now for each xx, the pullback of kk and j xj_x is a subobject of 1, call it U xU_x. Since a well-pointed topos is two-valued, every U xU_x must be 00 unless some U xU_x is 11. Since coproducts in a topos are stable under pullback, 1= XU x1 = \coprod_X U_x. But then if U x=0U_x=0 for every xx, we would have 1= X0=01 = \coprod_X 0 = 0, contradicting well-pointedness. Thus there must be an xx with U x=1U_x=1, which implies that k=j xk=j_x.

In Constructive/Intuitionistic Mathematics

In constructive mathematics, SetSet is not a model of ETCSETCS, 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 SS with a full subcategory of SetSet. The next paragraph, however, proves only that SS is closed under indexed unions and detachable subsets (more precisely, under subsets whose characteristic function lands in the set of truth values belonging to SS — whereas for arbitrary SS, the only truth values we can be sure belong to SS are “true” and “false”).

Depending on how we choose to define “Grothendieck universe” intuitionistically, this may imply that if SS is essentially small then it is a Grothendieck universe. However, it definitely does not follow intuitionistically that if SS is large, it must be all of SetSet; 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 𝒰\mathcal{U} be a truth value (identified with the subset {|𝒰}{}=1\{\star \;|\; \mathcal{U}\} \subseteq \{\star\} = 1) such that ¬¬𝒰\not\not\mathcal{U} is valid and 𝒰\mathcal{U} is indecomposable and projective, and let SS be the topos Set/𝒰Set/\mathcal{U}. Then SS is a Grothendieck topos, hence cocomplete and locally small, and the assumptions on 𝒰\mathcal{U} ensure that it is well-pointed, but in an intuitionistic theory they don’t imply that 𝒰=\mathcal{U} = \top.

Note that in this example, the “global sections” functor SSetS\to Set is not the forgetful functor Set/𝒰SetSet/\mathcal{U} \to Set (which doesn’t even preserve the terminal object), but the exponential functor Π U=Hom(U,)\Pi_U = Hom(U,-). This is the direct image functor in the geometric morphism Set/𝒰SetSet/\mathcal{U} \to Set, whereas the obvious forgetful functor is the left adjoint to the inverse image functor that exhibits SS as a locally connected topos.

Last revised on August 26, 2011 at 09:32:35. See the history of this page for a list of all contributions to it.