# nLab Set

The category of sets

category theory

foundations

## Removing axioms

#### Categories of categories

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

# The category of sets

## Definition

$Set$ is the (or a) category with sets as objects and functions between sets as morphisms.

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 $Set$ should satisfy, including

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 $Set$ has many marvelous properties, which make it a common choice for serving as a ‘foundation’ of mathematics. For instance:

At least assuming classical logic, these properties suffice to characterize $Set$ 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 a groupoid, $Set$ is characterized by the fact that

• $Set$ is the discrete object classifier in the category Grpd of groupoids and functors, playing a similar role in classifying discrete groupoids in $Grpd$ that the set of truth values $\Omega$ does in classifying subsets in $Set$. The morphism $F:I \rightarrow Set$ is an indexed family of sets and $I$ is an index groupoid.

As a topos, $Set$ is also characterized by the fact that

It is usually assumed that $Set$ 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, $Set$ 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$ in constructive mathematics cannot satisfy the axiom of choice (since this implies excluded middle), although constructivists might accept COSHEP (that $Set$ has enough projectives). In predicative mathematics, $\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 $Set$ to be the category of all sets, so that in particular $Set$ itself is a large category. Authors who assume a Grothendieck universe as part of their foundations often define $Set$ to be the category of small sets (those contained in the universe). One often then writes $SET$ for the category of large sets, which is the universe enlargement of $Set$.

### Opposite category and Boolean algebras

###### Proposition

The power set-functor

$\mathcal{P} \;\colon\; Set \to Bool^{op}$

is a faithful functor which in its (eso+full, faithful) factorization induces an equivalence of categories between $Set$ and the opposite category of that of complete atomic Boolean algebras.

See for instance van Oosten, theorem 2.4

###### Remark

Restricted to FinSet this equivalence restricts to an equivalence with finite Boolean algebras. See at Stone duality for more on this.

###### Remark

In constructive mathematics, $\mathcal{P}$ defines an equivalence of $\Set$ with the opposite category of that of complete atomic Heyting algebras. In fact, for any elementary topos $\mathcal{E}$, the power object functor defines an equivalence of $\mathcal{E}$ with the opposite category of that of internal complete atomic Heyting algebras. (This phrase can be interpreted using the internal language of $\mathcal{E}$.)

In higher category theory the role of $Set$ is played for instance by

## References

• 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)
category: category

Last revised on June 11, 2022 at 07:59:35. See the history of this page for a list of all contributions to it.