On Tarski-style universes in type theory

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.

posted about 2 years ago

CC BY-SA 4.0

Derek Elkins‭

1604 reputation 2 48 165 25