1
$\begingroup$

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).

  1. 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.
$\endgroup$

1 Answer 1

6
$\begingroup$

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.

$\endgroup$
6
  • $\begingroup$ Thank you! I think I don't fully understand the case when we have two universes $U$ and $V$ with $U$ being "an element" of $V$. If $u:V$, then we can't consider $T(u)$ since the "domain" of $T$ is $U$. Are there two $T$s, $T_V$ and $T_U$? If so, then we should have a few more inference rules - what would they be? (Also, if we have to have two different $T$s, that would be consistent with what Luo writes in his note, since his $T$s have indices.) [continued below] $\endgroup$
    – user175254
    Mar 27, 2023 at 21:46
  • $\begingroup$ [continuation of above] But on the other hand, I'm confused by the following discrepancy: if we set $U_i=V, U_{i+1}=U$ to match Luo's notation (where $U$ and $V$ are the two universes from your answer), then what you consider is $u:U_i$ and $T(u)=U_{i+1}$ whereas Luo seems to be doing the opposite - he considers $u_i:U_{i+1}$ and $T_{i+1}(u_i)=U_i$. $\endgroup$
    – user175254
    Mar 27, 2023 at 21:46
  • $\begingroup$ I ammended the answer to point out that each universe has its own decoding. So $T_V(u) = U$. $\endgroup$ Mar 28, 2023 at 6:05
  • $\begingroup$ These baby examples are very helpful. So if we use Tarski-style universes, we don't have to have infinite "chains" of universes, whereas if we use Russel-style universes, we must have an infinite chain to avoid things like $U:U$? Also, the note I linked mentions "lifting operators" but I guess we don't have to have those lifting operators? (Maybe I should create a separate question about lifting operators as I don't have intuition on what they are for; in the note they're used in conjunction with inductive types; I'm not sure if these operators are only useful if we have inductive types, etc.) $\endgroup$
    – user175254
    Mar 28, 2023 at 23:57
  • $\begingroup$ We can do exactly the same thing with Russell universes as with Tarski universes. The only difference is that Russell universes do not need the decoding $T$ because types literally are elements of a universe. $\endgroup$ Mar 29, 2023 at 12:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.