Unnested universes in type theory

Question

All sources I looked at only talk about a nested family of universes $U_0 : U_1:U_2: \dots$ (for example, the HoTT book, or Notes on Universes in Type Theory, or this answer). If one has two (or more) universes that are not nested, how can one formally introduce them? For example, in this paper (and elsewhere), the author talks about the universe Prop of logical propositions "as found in impredicative type theories such as CC and UTT" and the universe CN of common nouns. Intuitively, these two universes should be "disjoint", in the sense that it would be counterintuitive to say that $Prop:CN$ or $CN:Prop$. It is clear how the impredicative $Prop$ fits in the "framework" with nested universes (again, see this answer), but it is not clear how the universe $CN$ fits in here. Do we just postulate several "chains" of universes, like $$Prop=U_0 : U_1:U_2 \dots\\ CN=U_0' : U_1':U_2':\dots$$ or are there problems with this approach?

Answer 1

We can specify disjoint universes which are not necessarily organized into any hierarchy. Most commonly we use Tarski-style universes for this purpose.

• Types and terms are distinct objects, types themselves have no types.
• A Tarski universe is a type $\mathsf{U}$ together with an operation $\mathsf{El}$ such that for $A : \mathsf{U}$ we have that $\mathsf{El}\,A$ is a type. $\mathsf{El}$ is short for "element of", so $\mathsf{El}\,A$ is the type of the elements of $A$.
• $\mathsf{U}$ is closed under certain assumed type formers. For example, $\mathsf{U}$ has $\mathsf{Bool}$ if $\mathsf{Bool} : \mathsf{U}$ and the type $\mathsf{El}\,\mathsf{Bool}$ supports the introduction and elimination rules of the usual $\mathsf{Bool}$ type former.

This setup allows us to specify any number of unrelated universes, but we can also reproduce hierarchies by assuming a universe for each (external) universe level. Here, a universe doesn't have to be contained in any universe. Universes are just types, and a universe is contained in some universe precisely if it is of the form $\mathsf{El}\,x$, where $\mathsf{El}$ is the "element" operation of some other universe. Tarski universes are the simplest to formally specify, so they're often used in the metatheory of type theories. In the popular implementations of type theories though, level-indexed hierarchies are more common, for reasons of practical convenience and flexibility.

We can specify disjoint hierarchies in Tarski-style, but alternatively we can also do it in Russell-style (where terms and types are identified; like in the HoTT book and in many other places). In Russell style, every universe must be in a universe, but that's the case if we assume two (or more) disjoint hierarchies.

Answer 2

The philosophy of type theory with universes can be summed up by two maxims. Every term has a type, and every type is a term.

Since types are themselves terms, they must have a type. Such types are called universes.

Because a universe is a type, it must reside in a universe. So we clearly should have some universes $U_0 : U_1 : U_2 : \ldots$. This does not preclude that there may be additional universes outside this chain, but we do not assume their existence.

You may think it might be convenient to have just one universe $U : U$, but this actually leads to paradox. So we really do need infinitely many distinct universes.

The question of nested universes is not about whether we have this chain of universes, but about whether these universes overlap. We generally don’t want to have ambiguity over what type a given term has. On the other hand, we need some way of relating types in one universe to types in another. If we have types $T_1 : U_i$ and $T_2 : U_j$, we want to know what universes contains types like $T_1 \times T_2$, $T_1 \to T_2$, etc. Your postulated two chains of universes don’t help us with this problem. The HoTT book chooses to do this by having each universe be a “subset” of the next universe. So if $T : U_0$, then $T : U_1$ as well.

With this approach, we begin to see how we might approach two “incompatible” universes. We could choose to label universes by something other than a natural number. We could take a partial order $(P, <)$ such that (1) there exists some $x \in P$, (2) for all $a, b \in P$, there exists some $c \in P$ such that $a, b < c$. We could then have, for each $p, q \in P$, a universe $U_p$, where if $p < q$, then $U_p : U_q$, and if $p \leq q$ and $T : U_p$, then $T : U_q$.

Finally, I’m not totally certain that the type of common nouns should be a “universe”, since I see no reason why its elements should be types.