This definition is somewhat vague by design. Rather than canonize a fixed set of principles, the nLab adopts a ‘pluralist’ point of view which recognizes different needs and foundational assumptions among mathematicians who use set theory. Thus, there are various axes to consider when formulating categorical properties one thinks SetSet should satisfy, including

first-order vs. higher-order logic
impredicative vs. predicative mathematics
‘variability’ vs. ‘constancy’ (Lawvere)
classical logic vs. intuitionistic logic
image factorizations and quotient sets, i.e. sets vs setoids.
initial and free structures, i.e. transfinite construction of free algebras/quotient inductive types
choice principles
replacement or collection principles
smallness structures

just to name a few. Quite a bit of axiomatic fine-tuning can enter when one considers the panoply of hypotheses that might appeal to one or another school of intuitionism or constructivism, or various combinatorial or cardinal hypotheses one might attach to ZFC, etc.

Properties

Characterization

The category SetSet has many marvelous properties, which make it a common choice for serving as a ‘foundation’ of mathematics. For instance:

It is a well-pointed topos,

So in particular it is locally cartesian closed.
It is locally small.
It is complete and cocomplete (in fact, locally finitely presentable?), and therefore ∞\infty-extensive (as is any cocomplete topos).

At least assuming classical logic, these properties suffice to characterize SetSet uniquely up to equivalence among all categories; see cocomplete well-pointed topos. Note, however, that the definitions of “locally small” and “(co)complete” presuppose a notion of small and therefore a knowledge of what a set (as opposed to a proper class) is.

As The a groupoid,SetSetcore groupoid is of characterized by the fact thatSetSet (whose morphisms are the bijections) is characterized by the fact that

Core(Set) Set Core(Set) is the discrete object classifier in the category Grpd of groupoids and functors, playing a similar role in classifying discrete groupoids in GrpdGrpd that the set of truth values Ω\Omega does in classifying subsets in SetSet. The morphism F:I→SetF:I \rightarrow Set is an indexed family of sets and II is an index groupoid.

As a topos, SetSet is also characterized by the fact that

SetSet is the terminal object in the category of Grothendieck toposes and geometric morphisms. The terminal morphism Γ:E→Set\Gamma\colon E \to Set from any other topos EE is the global sections functor.

It is usually assumed that SetSet satisfies the axiom of choice and has a natural numbers object. In Lawvere’s theory ETCS, which can serve as a foundation for much of mathematics, SetSet is asserted to be a well-pointed topos that satisfies the axiom of choice and has a natural numbers object. It follows that it is automatically “locally small” and “complete and cocomplete” relative to the notion of “smallness” defined in terms of itself (actually, this is true for any topos).

Conversely, Set\Set in constructive mathematics cannot satisfy the axiom of choice (since this implies excluded middle), although constructivists might accept COSHEP (that SetSet has enough projectives). In predicative mathematics, Set\Set is not even a topos, although most predicativists would still agree that it is a pretopos, and predicativists of the constructive school would even agree that it is a locally cartesian closed pretopos.

Size

Above we considered SetSet to be the category of all sets, so that in particular SetSet itself is a large category. Authors who assume a Grothendieck universe as part of their foundations often define SetSet to be the category of small sets (those contained in the universe). One often then writes SETSET for the category of large sets, which is the universe enlargement of SetSet.

Opposite category and Boolean algebras

See for instance van Oosten, theorem 2.4

Set in homotopy type theory
A variant of SetSet where functions are generalized to relations is Rel.

(n+1,r+1)(n+1,r+1)-categories of (n,r)-categories

Pos
Set
- Rel
Grpd, ∞Grpd
Cat
- Ho(Cat)
- AccCat
- PrCat
- LexCat
- MonCat
- VCat
- CatAdj
- Prof
- Operad
2Cat
ModCat, CombModCat
(∞,1)Cat
- Pr(∞,1)Cat
- (∞,1)Operad
(∞,n)Cat

References

Saunders MacLane, §IV.10 of: Categories for the Working Mathematician, Graduate Texts in Mathematics 5 Springer (1971, second ed. 1997) [[doi:10.1007/978-1-4757-4721-8](https://link.springer.com/book/10.1007/978-1-4757-4721-8)]
Jaap van Oosten, Basic category theory (pdf)

On Set in homotopy type theory:

Egbert Rijke, Bas Spitters, Sets in homotopy type theory, Mathematical Structures in Computer Science, Volume 25, Issue 5 (From type theory and homotopy theory to Univalent Foundations of Mathematics) (arXiv:1305.3835)

Last revised on January 3, 2024 at 15:20:43. See the history of this page for a list of all contributions to it.