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.

  • $\begingroup$ 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$? $\endgroup$
    – Hanul Jeon
    Nov 17, 2023 at 0:24
  • $\begingroup$ 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. $\endgroup$
    – user837242
    Nov 17, 2023 at 0:27
  • $\begingroup$ 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. $\endgroup$
    – Hanul Jeon
    Nov 17, 2023 at 18:21


You must log in to answer this question.

Browse other questions tagged .