Are type universes related to proper classes from set theory?

Question

I'm currently learning Lean 4, and in the book they mention that the type hierarchy was introduced to avoid a version of Russell's paradox. From reading a bit about set theory a while ago, I remember they dealt with Russell's paradox by introducing Classes, or collections that are not members of any other entity. These seem to be similar concepts, but different because Type 1 is a member of Type 2 and such. Are they related at all?

Answer 1

They have a close relationship. Type universes, like Grothendiek universes in set theory, are a way to formally represent very large objects which in traditional set theory are too big to be sets, and would instead be called classes.

Classes in set theory

As for Russell's paradox, modern ZFC avoids doing naive comprehension, so you can't talk about the set of all sets, nor an arbitrary subset thereof, like the set of all sets that don't contain themselves. Instead, in ZFC, one must do comprehension over existing sets. Classes are a way to talk about collections of sets that are too big to be sets, like the class of all sets, the class of ordinals, the class of groups, etc. It also is used to represent functions that are too large, like the cardinality function. In ZFC, classes are an informal concept. There is no logical notion of a class in ZFC, but instead one thinks of a class as an unbounded comprehension $\{x : \phi(x)\}$ where $\phi$ is a formula of ZFC with one free variable. In NGB set theory, the notion of class is a formal part of the axioms of the logic.

Grothendieck universes in set theory

In some areas of mathematics, it is important to be able to talk directly about class-size objects, like in category theory where one wants to talk about the category of sets, or in metamathematics where one needs to talk about models of ZFC. For this, one can assume the existence of strongly inaccessible cardinals $\kappa$, and the set $V_{\kappa}$ of all sets smaller than $\kappa$ form a model of ZFC, what the categorical mathematicians call a Grothendieck universe. The subsets of $V_{\kappa}$ behave like proper classes, so you can for example talk about the set of all small sets (or small groups or small categories) where "small" means it is in the Grothendieck universe $V_{\kappa}$.

Universes in type theory

Types were first introduced by Russell to fix his paradox, but I don't know the details, and I don't know if his ramified type theory contains what we would now call universes.

But many flavors of modern dependent type theory contains the notion of a universe Type, the type of (small) types. But just like set theory, it is a contradiction to have Type in Type. So usually there is a hierarchy of types, Type 0 : Type 1, Type 1 : Type 2, etc.

Relationship between type universes and Grothendieck universes

Dependent type theory with no special axioms is more general than a theory of sets. It describes something more like a higher topos. But if you add the axiom of choice (as much of Lean does), then types behave like sets in ZFC, and universes Type u behave like Grothendiek universes. In Lean, I think each Type u is roughly at the level of a new model of ZFC. While Lean and ZFC are different kinds of "set theories" (in type theory it doesn't make sense to say $A \in B$ for types $A$ and $B$), you can construct a model of ZFC in Lean using any type Type u. (Formally the type ZFSet.{u} of ZFC sets lives in Type (u+1) for any u.) Conversely, Mario Carniero's thesis showed ZFC plus infinitely many strongly inaccessible cardinals $\kappa_n$ can be used to create a model of Lean's type theory, where types are just modeled as sets, and where each Type n corresponds to the Grothendieck universe $V_{\kappa_n}$.

Using type universes to construct class-size objects

Finally, getting back to proper classes as in ZFC, for any Type u, and any predict P expressible in Lean, you can construct the subtype {X : Type u // P x}, for example here is the type of all types in Type 1 with at least two elements: {X : Type 1 // ∃ x y : X, x ≠ y}. However, unlike classes in ZFC, these are formal objects we can talk and reason about directly inside Lean. The only trade-off is that when we invoke Type u, we must go up a level in the universe hierarchy to Type (u+1).

Moreover, subtypes are just a special case of more general structures in type theory which let us construct the types of groups, topological spaces, ordinals, and the like, (including their respective categories) all of which would be proper classes in ZFC. Similarly, you can construct functions like the cardinality of a type. All of these types are parameterized over a type variable u, so that, say, Ordinal.{u} is the type of ordinals small enough to live in Type u. (Therefore, Ordinal.{u} lives in the next higher type Type (u+1).)

This universe polymorphism (with a hierarchy of type universes) gives a sort of breathing room, where one doesn't have to worry about hitting a ceiling of types that are too large to be types (again having to resort to something like proper classes in set theory).