Formulation of Tarski-style universes in LF

Question

Lately I've been asking questions on type theory on MSE, and I've been getting great answers, but I decided to give a try to this site and see if it will be helpful as well.

I'm looking at this note about universes in type theory.

1. 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)? In another source, Luo says that every predicative universe $U_i$ has name $u_i$ in $U_{i+1}$, but why do we need to have a name for $U_i$ in $U_{i+1}$?

2. Further, it is said in the remark on page 3 that Tarski-style universes can be formulated in LF (I think he has his LF used in UTT in mind):

$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 Luo's LF mentioned in this question? What is the relationship between $El(-)$ and $T_j(-)$? I believe there must be some relationship, as suggested by the answers by András Kovács in the two cited questions (the second cited question appears below).

3. If I want to declare several unrelated predicative universes (as well as the impredicative $Prop$ universe), do I just make a series of declarations of distinct $U_i$ as in quote above? (So I will have several unrelated nested universes.) Or are there any technical difficulties with that? I asked a similar question before, and got an answer, but that question doesn't involve LF and now I'm wondering how to implement this if I use the LF mentioned above.

Answer 1

Papers on universes are usually concerned with universes that are large, i.e., most authors are intersted only in universes closed under dependent products. But nothing prevents us from having a baby universe, which I think is easier to understand.

Suppose we wanted to have a baby universe $U$ which contained all the types that can be formed starting with types $\mathtt{nat}$ and $\mathtt{bool}$ using binary cartesian product. So the elements of $U$ would be types such as $$\mathtt{bool}, \quad \mathtt{nat}, \quad \mathtt{bool} \times \mathtt{nat}, \quad (\mathtt{nat} \times \mathtt{nat}) \times \mathtt{bool}, \quad \ldots $$ and so on. Due to formalistic reasons, we want to keep elements and types separate (allowing types to be elements of other types would lead to Russell-style universes), so our $U$ cannot actually contain the above types. Instead its elements will be codes of types, and we will also need a decoding function. How could we code the above types? With an inductive type, like this (using Agda notation):

data U : Type where
  n : U
  b : U
  p : U → U → U

For example, p(p(n,n),b) encodes the type $(\mathtt{nat} \times \mathtt{nat}) \times \mathtt{bool}$. The decoding function $T$ takes elements of $U$ to types, in other words, $T$ is a type family parameterized by $U$:

T : U → Type
T n = nat
T b = bool
T (p (a, b)) = T a × T b

This was Agda. In formal type theory, as found in books and papers, we would instead postulate formation rules \begin{gather*} \frac{ }{\vdash U \ \mathsf{type}} \qquad \frac{ }{\vdash n : U} \qquad \frac{ }{\vdash b : U} \qquad \frac{\vdash a : U \qquad \vdash b : U}{\vdash p(a,b) : U} \qquad \frac{\vdash a : U}{\vdash T(a)\ \mathsf{type}} \end{gather*} and judgemental equalities \begin{align*} T(n) &\equiv \mathtt{nat} \\ T(b) &\equiv \mathtt{bool} \\ T(p(a,b)) &\equiv T(a) \times T(b) \end{align*}

Note that the above definition of $U$ is not the only possible way of coding the types. If we lived in 1950 we would encode everything with natural numbers (Gödel was very much alive then):

U = nat

and, for a suitable bijection unpair : nat → nat × nat define

T : U → Type
T 0 = nat
T (suc 0) = bool
T (suc (suc k)) = T a × T b where (a, b) = unpair k

Sometimes we use the symbol $\mathrm{El}$ instead of $T$, depending on the author and the weather. Read $e : \mathrm{El}(a)$ as "$e$ is an element of $a$".

I hope the basic ideas are now a bit clearer. Nothing much changes when we pass to "real" universes that are closed under products, except that everything gets slightly more complicated because $U$ and $T$ become mutually recursive.

We may also have several universes. For example, if we wanted two universes $U$ and $V$ such that $U$ "is an element" of $V$, then we would introduce a code $u : V$ and decode it as $T_V(u) = U$. (Of course, we need two decoding function $T_U$ and $T_V$.)

You can do whatever you like. For example, you could have universes indexed by the integers $$\ldots, U_{-2}, U_{-1}, U_0, U_1, U_2, \ldots$$ such that $U_k$ contains (a code of) $U_{- 3 k + 7}$ for all $k \in \mathbb{Z}$, or whatever. Once again, each universe $U_k$ gets its own $T_k$. Whether the end result is interesting, insane, either or both, is a separate question.