Reference. Introduction to Category Theory and Categorical Logic [streicher-intro-category-logic-2003]

January 1, 2003
Streicher, Thomas
Technische Universitat Darmstadt

Backlinks

Definition. Grothendieck universe [002q]

November 27, 2025

Motivation

November 27, 2025

In set theory (along with other theories which consider collections of stuff) there is an issue which you try to talk about the collection of collections, as it gives rise to certain paradoxes by the recursive nature of it. One way out is to consider a hierarchy of notions of collections, where a "collection of collections" is not in fact considered a "collection" itself but rather some notion of a higher increment of collection.

This is the idea behind universes, where the universe is a collection of all set's which intuitively can be thought of as a "set of all sets" but is not itself a set but one increment above it in the hierarchy.

Definition

November 27, 2025

A Grothendieck universe is a set (in ZFC) \(\mathcal U\) with the following properties (1):

(transitivity) If \(x \in \mathcal U\) and \(y \in x\), then \(y \in \mathcal U\).
(power set) If \(x \in \mathcal U\), then \(\mathcal P(x) \in \mathcal U\) where \(\mathcal P(x)\) is the powerset (set of all subsets) of \(x\).
(unions) If \(I \in \mathcal U\) and \(x_i \in \mathcal U\) for each \(i \in I\), then the union \[ \bigcup _{i \in I} x_i \in \mathcal U \]
(natural numbers) The set of natural numbers \(\mathbb {N} \in \mathcal U\).

Additional properties of \(\mathcal U\) can be enumerated as follows:

If \(x, y \in \mathcal U\) then \(\{x, y\} \in \mathcal U\).
If \(x \in \mathcal U\) and \(y \subset x\), then \(y \in \mathcal U\).
If \(I \in \mathcal U\) and \(x_i \in \mathcal U\) for each \(i \in I\), we have the cartesian product: \[ \prod _{i \in I} x_i \in \mathcal U \]
If \(I \in \mathcal U\) and \(x_i \in \mathcal U\) for each \(i \in I\), we have the disjoint union: \[\coprod _{i \in I} x_i \in \mathcal U \]
If \(x, y \in \mathcal U\), then the function set from \(x\) to \(y\) is also in \(\mathcal U\): \[ y^x = \{ f : x \to y \} \in \mathcal U \]

An aside on classes and sets

November 27, 2025

In a very general sense a class is any collection of sets defined by a property that all its members share. So we can express it it as a predicate on some universe \(\mathcal U\):

\[ A : \mathcal U \to \texttt {Prop} \]

As an example in the case of an unsorted set theory (such as ZFC) in which all objects are sets, we define a class \(C\) as a proposition or truth value in the context of some free variable \(A\), the notation used in (5) is:

\[ \Gamma , A \mid \phi \vdash C : \texttt {Prop} \]

This expresses that in the context of assumptions \(\Gamma \) extended with the variable \(A\) the proposition \(\phi \) defines a class \(C\). A more classical, albiet probably less formal, way to read this might be:

\[ C = \{ x \in \mathcal U \mid \phi (x)\} \]

Furthermore we say that a class \(X\) is a set if and only if there exists a class \(Y \in \mathcal U\) such that \(X \in Y\). A proper class is a class which is not a set (6).

Axiom of Universes

November 27, 2025

The common theme amongst these properties is that the aim to express closure of the set \(\mathcal U\) under various standard set-theoretic operations. This allows us to treat \(\mathcal U\) as a universe of sets in which we can carry out normal set-theoretic constructions without leaving the universe.

The Axiom of Universes is the general convention which is adopted in category theory and other fields which states that for every set \(x\) there exists a Grothendieck universe \(\mathcal U\) such that \(x \in \mathcal U\).

An element of \(\mathcal U\) is by convention called a \(\mathcal U\)-small set or simply a small set when the universe is clear from context or apparently also just a set (1).

A subset of \(\mathcal U\) is called \(\mathcal U\)-moderate or simply moderate when the universe is clear from context.

The general line of reasoning, at least in ZFC is that for every set \(x\) we assume there exists a Grothendieck universe \(\mathcal U\) such that \(x \in \mathcal U\). Accordinly for every universe \(\mathcal U\) there exists a larger universe \(\mathcal U'\) such that \(\mathcal U \in \mathcal U'\), and therefore also \(U \subseteq U'\). Thus under this assumption with have the guarantee of a hierarchy of universes (4):

\[ \mathcal U_0 \in \mathcal U_1 \in \mathcal U_2 \in \cdots \]

Which are also cumulative in the sense that

\[ \mathcal U_0 \subseteq \mathcal U_1 \subseteq \mathcal U_2 \subseteq \cdots \]

Remarks

November 27, 2025

An additional point made in (2) is that \(\mathcal U\) denotes a pure set, that is, all elements of \(\mathcal U\) are sets and there are no urelements (elements which are not sets). Formally we say that a set \(x\) is pure if for every finite sequence or chain (3):
\[ x_0 = x \in x_1 \in x_2 \in \cdots \in x_n \]
each \(x_i\) is a set. Another way this is intuitively thought of is that every object reachable from \(x\) by finitely many membership steps is also a set.

Since we are typically working in the context of ZFC set theory which only allows for sets as elements, all sets are pure by default hence the distinction is sometimes omitted. Theories such as ZFA (Zermelo-Fraenkel set theory with atoms) allow for urelements which do not qualify as sets but can be members of sets.
The countable set property is sometimes (7) also replaces with
\[ \emptyset \in \mathcal U \quad \text { or } \quad \omega \in \mathcal U \]
Where \(\omega \) is the set of all finite (von Neumann) ordinals.
Subset's of \(\mathcal U\) seem to have a somewhat confusing naming convention. So nlab says they are called moderate though this is sometimes also overloaded with the ambiguous term large. They mention that under the assumption that set is equivalent to small set then moderate clearly aligns with proper classes (as those are definitionally distinct from sets). I assume the convention taken in at least (1) is that they use they essentially use the term class to mean proper class and by implication moderate set relative to some universe.

My assumption is that people use class and proper class interchangeably mainly because a proper class actually refers to an object distinct from a set, whereas a class can make it ambiguous whether you mean a set (which is a class) or a proper class (which is not a set).