context ${\mathfrak U}_\mathrm{Sets}$ … set universe
definiendum ${\bf Set}$
postulate $\mathrm{Ob}_{\bf Set}:={\mathfrak U}_\mathrm{Sets}$
inclusion ${\bf Set}$ … locally ${\mathfrak U}_\mathrm{Sets}$-small category
postulate $f\in{\bf Set}[X,Y]\ \ \Leftrightarrow\ \ f:X\to Y$


Here '$f:X\to Y$' on the right denoty a function in the type theory sense, where domain and codomain are sets. Note that ${\bf Set}$ is a nice category: it's closed in particular, so that each hom-class is an object and hence a set in $\mathrm{Ob}_{\bf{Set}}$ and so all function are sets too. The expression '$f:X\to Y$' can be viewed as the predicate on $f$ as defined in the entry Function. Note that this predicates requires a codomain declaration.

There are also characterizations of the category of sets which don't require an a conventional set theory (e.g. see (Trimble on ETCS I and links therein), but a kind of axiom of infinity to “fill up” the category. (Note that the first order topos approach actually goes without the need for objects of a category, in the sense we do. It goes with arrows and composition only, and then objects are essentially the image of the domain “maps” to arrows.)

Status of the category Set within category theory

In category theory, if you're interested in some mathematical structure, you set it up by considering a category $\bf C$ with some objects and the arrows of interest (e.g. groups and group homomorphisms). In axiomatic set theory, you only need one initial collection of axioms and then look for models of your structure within the logical domain of discourse. One consequence of this is that a set theory generally grants the existence of much more than you want to work with construction but will be part of your set theory. For example, the sets $\mathbb Q\setminus 9001$ and $\mathbb Z_5 \cup \langle 7,\mathbb R\rangle$ are (silly) objects and $\mathrm{Hom}(\mathbb Q\setminus 9001,\mathbb Z_5 \cup \langle 7,\mathbb R\rangle)$ is the (even sillier) set of all function between them. The category $\bf Set$ is the category theoretical realization of this messy conglomerate of things.

But because set theory is so encompassing, $\bf Set$ is very special: The functors $F:{\bf C}\to{\bf Set}$ can be viewed as all set theoretical realizations of your structure. It has exponential objects (it's a topos, even), i.e. any ${\bf Set}[X,Y]$ is also internally represented by an object, which is denoted $Y^X$. For this reason, every presheaf category turns out to be a topos. Just define things like product and exponents pointwise in the argument!

Please check out the discussion of the Yoneda lemma in presheaf category.


Wikipedia: Category of sets

nLab: Trimble on ETCS I, and links therein.



Elements of


Link to graph
Log In
Improvements of the human condition