# Motivations for introducing a "super-universe"

I'm trying to understand universes in type theory, and I'm looking at this note. Let's consider a toy example, where we have just two universes, $$U_0$$ and $$U_1$$. Then we have this set of rules (ignoring the rules on type constructors):

$$\frac{}{U_0 \ \text{type}} \quad \frac{a:U_0}{T_0(a) \ \text{type}}$$

$$\frac{}{U_1 \ \text{type}} \quad \frac{a:U_1}{T_1(a) \ \text{type}} \quad \frac{}{u_0:U_1} \quad \frac{}{T_1(u_0)=U_0}$$

$$\frac{a:U_0}{t_1(a) : U_1} \quad \frac{a:U_0}{T_1((t_1(a)) = T_0(a) }$$

I'm thinking about $$U_0$$ as "sets", and $$U_1$$ as "classes". So if $$S$$ is a set, we can say $$S:U_0$$, and for every set $$S$$, $$T_0(S)$$ is the collection of all elements that $$S$$ contains. But if $$S$$ is the set of all sets (which is not a set itself), for example, then we cannot say $$S:U_0$$. This motivates the introduction of $$U_1$$, which "includes" everything that $$U_0$$ includes (indicated by the rule $$t_1(a):U_1$$), plus it includes the set of all sets $$U_0$$. For every class $$a:U_1$$, $$T_1(a)$$ is the collection of all elements it contains, and there is a special class $$u_0$$ whose elements are exactly all sets, i.e., all elements of $$U_0$$. Lastly, the rule $$T_1((t_1(a)) = T_0(a)$$ says that if $$a$$ is a set, then the collection of its elements is the same as the collection of its elements when this set is a considered as a class, which seems to be a natural requirement.

Is this the right way to think about this two-universe setup in the context of sets/classes? Also, how to think about it in more type-theoretic way? I.e., what I presented seems to be a set-theoretic motivation of introducing a super-universe $$U_1$$ that "contains" $$U_0$$. What would be type-theoretic motivation for introducing $$U_1$$? I suppose it's related to quantification and/or context extension, but I'm not sure about the details.

• I think your informal reasoning is correct. I have no idea what superuniverses are: Does it mean a universe that is closed under universe operator $t\mapsto U(t)$ "containing" $t$? Nov 17, 2023 at 0:24
• Maybe I shouldn't have used the term 'superuniverse'. What I meant by a 'superuniverse' is just the universe $U_1$ in the context of my question. Nov 17, 2023 at 0:27
• Oh, I see. I once heard that the introduction of larger universes is related to Girard's paradox, which can be understood as type-theoretic version of Russell's paradox. Nov 17, 2023 at 18:21