What is a universe?

Question

What is a universe?

More specifically,

1. Is a type system without a term-type distinction, are universes just ordinary types?
2. If (1) is true, can we the system-builders freely choose which types are "labeled" as universes or is there a specific property that the collection of universes must satisfy?
3. (An elaboration of (2)). If we label every type as a universe is it wrong or just misleading?
4. What are universes in systems that possess a term-type distinction?
5. Given a type, is it inherently associated with exactly one universe? (The same way that a term is associated with exactly one type.)
6. Do universes "exist globally" or are they like a "local fiction" (like universe levels in NFU ... that exist purely for the purpose of stratifying formulas and don't exist otherwise).

NOTE: I'll reserve the word sort for use in a non-formal/meta-level sense; in this question a sort is not the type of a kind.

---

What follows is my attempt to make sense of the material.

---

At time of writing, the universe tag wiki refers to the Wikipedia page and nLab.

Wikipedia says the following about universes in the context of type theory specifically.

In some type theories, especially in systems with dependent types, types themselves can be regarded as terms. There is a type called the universe (often denoted ${\mathcal {U}}$) which has types as its elements.

Here's how I interpret this.

• In type systems that have a weak or nonexistent term-type distinction, a universe $\mathcal{U}$ is just a type.
• In type systems that have a term-type distinction, $\mathcal{U}$ is a new sort of type that has types as elements. These systems now have a term-type-universe distinction.

The Wikipedia article gets most of its content from this article on homotopy type theory.

In this setting, it appears that a universe is a type for which we have an inference rule kind of like the following.

$\varphi$ is a fixed well-formed formula (that might be empty or might be an interpretation function) and $U$ is a universe.

$$ \frac{A : U}{\varphi(A) \;\; \text{type}} $$

Section 4 of that article covers some concrete choices made by different proof assistants.

That and the section before about typical ambiguity are, to me at least, strongly reminiscent of the set theory NFU ... which can informally be obtained by taking the Russellian theory of simple types and just identifying stuff at every level of the hierarchy by neglecting type indices on defining formulas.

However, in the NFU case, the different universes in the universe hierarchy do not exist globally. They spring into existence when we need to stratify a formula and then disappear.

Answer 1

There's a simple criterion for a term $U$ to be a universe... If there exists $\Gamma, t, T$ such that $\Gamma \vdash t : T$ and $\Gamma \vdash T : U$. So, (1) is unproblematic, but (2) is false, (3) is wrong but can be made sort of true as explained below, (4) your inference rule below nailed it, (5) depends on your choice, and note that a term does not have to be associated with exactly one type either, it's all just design choices, (6a) universes are essential to express certain constructs. Primary examples include proving that $0\ne 1$, and (in HoTT) proving that the fundamental group of $S_1$ is $\mathbb Z$. More concretely, we can define $$F(n)=\begin{cases} \top & n=0\\ \bot & \text{otherwise} \end{cases}$$ which is a function $F : \mathbb N \to \mathscr U$, into a universe! Now suppose for contradiction that $0 = 1$, then $F(0)=F(1)$, and so $\top = \bot$, therefore $\top \to \bot$ which is contradiction.

(6b) if you meant "universe hierarchy" in your (6) instead of just "universe", then it depends on your choice.

I promised to explain (3). In Haskell, certain combinations of language extensions makes every datatype (such as $\mathbb N$ defined inductively with constructor $\mathrm Z : \mathbb N$ and $\mathrm S : \mathbb N \to \mathbb N$) generate a copy in a higher level. So you will have $`\mathbb N$ be a universe with type $`\mathrm Z : `\mathbb N$ and type constructor $`\mathrm S : `\mathbb N \to `\mathbb N$. However, these types don't have "values" in the usual sense. It is there simply because we are reluctant to introduce full dependent types in Haskell, and we need a compile time natural number. And in Haskell, all compile time information is contained in the types (essentially).

(5) is also worth mentioning. In fact, the term $\lambda x. x$ already has multiple typing! It can be typed either as $\mathbb N \to \mathbb N$, or as $\mathrm{Bool} \to \mathrm {Bool}$. You may have two arguments against this:

1. There is a principal type $\alpha \to \alpha$.
2. In type theories such as CIC or MLTT, $\lambda x. x$ is not a term, $\lambda (x:\alpha). x$ is. This annotation gives us the correct type.

For the first point, there will be no principal types once you introduce things like dependent functions. The second point is valid. And in MLTT and CIC (ignoring universes, which we will discuss later), there is a valued property called uniqueness of typing. Such a property is not present in Nuprl or Cedille, for example.

You can enforce uniqueness of typing even with universes. But we would also want something called cumulativity, where each universe is included in higher universes. This would mean that if $A : U_1$, we also have $A : U_2$, which is sometimes convenient. This would then break uniqueness of typing. But if we are careful enough, we can maintain a "uniqueness of typing up to universes" property.

Your last point about typical ambiguity is true in some systems where each declaration is checked so that all the universe levels form a dag (i.e. no cycles). But different from NFU, where after a set comprehension $F_{x, y} = \{z: x \in z \in y \}$ you are free to identify some of the parameters, creating a seemingly ill-stratified definition $F_{x, x}$, in usual type theories you are forbidden to do so, unless you justify this with explicit lifts or otherwise indicate a correct interpretation.

Of course, you can do without typical ambiguity. In Agda for example, everything works smoothly because we have a thing called universe polymorphism. For example, we can define the product type over any universe level:

open import Agda.Primitive  -- Some primitive built-ins
-- In agda, (Set a) plays the role of the a-th universe.
data _*_ {a b : Level} (A : Set a) (B : Set b) : Set ??? where
  _,_ : A -> B -> A * B

Now, what should be filled in the question marks? Since Agda is a predicative system, we need the type to be higher than both a and b. Agda provides a "max" operation to express this: fill in a ⊔ b and Agda will be happy.

This of course raises a further question: What is the type of (a : Level) -> Set a? It must be higher than every a, right? Originally, this doesn't has a type (which is perfectly fine, not every type has a type, just like how not every collection of sets is a set). But currently, this has the type Setω, which is not equal to Set a for any a. This suggests an ordinal hierarchy. And indeed, Agda now has ω * 2 universes.

Answer 2

Note: I'm approaching this from a purely syntactic perspective. I'm sure that a deeper answer could be given from the semantic perspective.

In all type theories I'm aware of, a universe is a type that classifies types. You mention the idea of a type-term distinction. I'm interpreting this as the presence or absence of a judgment of the form $A \ type$, separate from $x : A$. This naturally leads to two styles of adding a universe to a type theory: universes ala Russel (Russel universes) and universes ala Tarski (Tarski universes).

A Russel universe is some type $U$, whose elements are other types. If we have some type $ℕ$, then we can derive a the judgment $ℕ : U$. The presence of a Russel universe allows us, if we wish, to completely eliminate any separate $A \ type$ judgment, replacing it with $A : U$ (assuming we have some type for $U$ itself). This solution is conceptually straightforward and is used in languages like Coq and Agda.

A Tarski universe is also some type $U$, but instead of its elements being types, they are terms, which we call type codes. Basically, instead of being able to derive $ℕ : U$, we have some new term, which I will call $`ℕ$, for which we can derive the judgment $`ℕ : U$. We do this for each type former. Notably, $`ℕ$ is not a type. We cannot derive $`ℕ \ type$ or $zero : `ℕ$. Instead, we introduce a special syntax which allows us to transform a type code into a type. This syntax is usually called $El$ (short for element), and allows us to derive that $El(a) \ type$ given that $a : U$. In order to make $El$ useful, we introduce the "obvious" judgmental equalities: for instance that $El(`ℕ) = ℕ \ type$. If instead we made these judgmental equalities into mere equivalences, where an explicit coercion is required to transform a code into a type, we would have what are called weak Tarski universes. For a language that actually implements weak Tarski universes (though they are essentially hidden by elaboration), check out cooltt: https://github.com/RedPRL/cooltt.

So to answer your questions with all this in mind:

1. Yes
2. A type is a universe when its elements classify other types in some meaningful way
3. I would say that this is wrong, but I do not have enough knowledge of semantics to back up why it must be
4. Tarski universes
5. Not necessarily, if we have a cumulative hierarchy of universes, we could have a rule classifying a type in any universe level
6. Universes exist globally in all type theories with them that I know of