On Tarski-style universes in type theory
I'm looking at this note about universes in type theory.
For Tarski-style universes (page 2), as far as I understand, the "$a$" in $a:U_i$ are formal names of types, whereas the "$T_i(a)$" in $T_i(a) \ type$ are actual types. What I don't understand is the purpose of "$u_i:U_{i+1}$" and "$T_{i+1}(u_i)=U_i$". Is there any intuitive explanation on why we have these two "axioms" (or whatever)?
Further, it is said in the remark on page 3 that Tarski-style universes can be formulated in LF:
$U_i: \textbf{Type}; \ T_i: (U_i)\textbf{Type};\ u_i:U_{i+1};\ T_{i+1}(u_i)=U_i : \textbf{Type}$
But how is this related to $El(A)$ from the LF mentioned in my previous question? Is there any relationship between $El(-)$ and $T_j(-)$?
1 answer
The following users marked this post as Works for me:
| User | Comment | Date |
|---|---|---|
| user205 | (no comment) | Mar 30, 2023 at 22:02 |
I'm a bit confused about what you're confused about for the first part. In a Russell-style universe system, we'd have a hierarchy of universes with $\mathcal U_i : \mathcal U_{i+1}$, i.e. the $i$th universe is a type in the $(i+1)$th universe. As you state, for a Tarski-style universe system, $\mathcal U_i$ is a type of "codes" for types in the $i$th universe and $T_i(a)$ for $a : \mathcal U_i$ is the "actual" type, i.e. a thing that can be to the right of a "$:$". Thus, there should be a code $u_i$ in $\mathcal U_{i+1}$ that represents the fact that $\mathcal U_i$ is a type in the $(i+1)$th universe. That is, $u_i : \mathcal U_{i+1}$ and $T_{i+1}(u_i) = \mathcal U_i$. This is just directly how you say the Russell-style $\mathcal U_i : \mathcal U_{i+1}$ in a Tarski-style universe.
As for how $El$ relates to $T_i$, $El$ and $T_0$ are the same thing where LF has only one universe, namely $\mathsf{Type}$. So $\mathcal U_0$ correspond to $\mathsf{Type}$, $T_0$ corresponds to $El$, and $type$ corresponds to $kind$. To be clear, this is treating LF and this logic with Tarski-style universes on the same footing. If we wanted to formalize this logic in LF, then the $El$ of LF as the meta-language and the $T_0$ of the object language would be different kinds of things.
1 comment thread
0 comment threads