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 is, 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.

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.