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.