Universes and Universe Levels

Boolean elimination cannot define $$D(\mathsf{tt})\equiv \mathbb{N},D(\mathsf{ff})\equiv \mathbf{1}$$ as a type family: its branches are terms, while $\mathbb{N}$ and $\mathbf{1}$ have so far appeared only in type judgments. A universe is a type whose terms name types: it makes types available as terms. Boolean recursion may then return $\mathbb{N}$ or $\mathbf{1}$ in a universe, and the result may again be used as a type. The price is a size discipline.

The Russell hierarchy

We extend the theory of chapter 27–chapter 28 by an externally indexed sequence $${\mathcal{U}}_0:{\mathcal{U}}_1:{\mathcal{U}}_2:\cdots .$$ In the Russell presentation, an element of ${\mathcal{U}}_i$ is used directly as a type. The index $i$ is a metatheoretic natural number, not a term of the object theory.

For later calculations, note the nullary instances explicitly: U-Void, U-Unit, U-Bool, and U-Nat place $\mathbf{0},\mathbf{1},\mathbf{2},\mathbb{N}$ in every ${\mathcal{U}}_i$. Together with U-Sum, these are the branch elements used by the large eliminations below.

The open-endedness is deliberate. Martin-Löf adopts a reflection principle for the universe of small types but notes that it does not justify the axiom that the universe is one of its own elements, which Girard had shown contradictory [ML75]. His adjacent-level rule is weaker than the all-lower-level instance U-Hier fixed here. The sequence supplies a place for each universe without closing the entire sequence inside one final universe.

Large elimination

A large elimination is an ordinary elimination whose motive is a universe, so its result may subsequently classify terms.

A primitive type-level Boolean conditional could reproduce this example, but would not provide recursion into a universe for $\mathbb{N}$ and hence would not define the recursive family below.

Type families as universe maps

Proof of Proposition 29.16 — Families are maps into

Proof. Application gives $F(x):{\mathcal{U}}_i$, and U-El makes it a type. Abstraction gives the reverse assignment. Their composites are $(\lambda x.B)(x)\equiv B$ and $\lambda x.F(x)\equiv F$ by the $\mathrm{\Pi }$ rules. ◻

For example, if $\mathrm{\Gamma }⊢A:{\mathcal{U}}_0$ and $\mathrm{\Gamma },x:A⊢B:{\mathcal{U}}_0$, rule U-W gives $\mathrm{\Gamma }⊢{\mathsf{W}}_{x:A}B:{\mathcal{U}}_0$. Thus the W-type former, not merely its ordinary formation rule, is available to universe-valued families.

Universe-polymorphic constraints

The calculations in this section use the optional cumulative membership extension

$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$i\le j$

$\mathrm{\Gamma }⊢A:{\mathcal{U}}_j$

Without U-Cumul, every premise of U-Pi must have exactly the rule’s single level, so level inference collapses to unification rather than the inequality problem below. This is an explicit local change of theory, not a silent property of definition 29.1.

An implementation replaces some external indices by level variables. For the fragment used here, level expressions are generated by $$\ell ::=0\mid u\mid \ell +1\mid max(\ell ,\ell ),$$ and formation emits inequalities between such expressions. Normalize a level expression as a finite maximum of atoms $u+n$ and a constant $n$. Then $\ell \le r$ means that every atom on the left is dominated by an atom with the same parameter on the right or by a known parameter constraint.

Proof of Proposition 74.10 — Completeness of the normalized solver

Proof. Fix an assignment of the external parameters satisfying $P$; those constraints restrict the inputs but add no unknown-bearing edge. Split every maximum into atomic inequalities and draw an edge $a\stackrel{n}{\to }x$ for $a+n\le x$. A positive cycle sums to $x+n\le x$ with , impossible in $\mathbb{N}$. If no such cycle exists, every edge inside a strongly connected component has weight zero; the variables in that component may be identified. The quotient graph is finite and acyclic. Process it in topological order, assigning each node the maximum of the expressions delivered by its incoming edges. This terminates. Every solution dominates every incoming expression, so induction over the topological order proves that it dominates the constructed assignment. The assignment itself satisfies every edge, hence is the least solution. ◻

Universe polymorphism is metatheoretic generalization over level variables followed by solving; it is not object-language quantification over levels. Kovács instead studies level structures and level-indexed families [Kov22]. That more expressive calculus is engineering evidence, not a theorem transferred to ours.

Lifting and cumulativity

The frozen Russell hierarchy is noncumulative. From $A:{\mathcal{U}}_i$ one cannot silently conclude $A:{\mathcal{U}}_{i+1}$. The cumulative rule used explicitly in section 74.4 is one repair; the other changes the syntax.

Cumulative membership changes typing, while explicit lifting changes syntax. We never assume both silently.

The fuss-free design replaces a proliferating family of lift naturality equations with a smallness calculus and proves its own equivalence and injectivity results [SS26]. Those results depend on that paper’s syntax and equations. Mugen implements displacement-algebra universe polymorphism and reports separate Agda and OCaml artifacts [FAM23]. We borrow neither metatheorem for the calculus fixed here.

A semantic boundary

Proof of Lemma 74.14 — Set interpretation of the universe rules

Proof. The ordinary final rules are sound by lemma 28.14; it remains to inspect the universe-specific final rules. For every environment $\rho$, U-Form is valid because $V_{{\kappa }_i}$ is a set. If , then which is the U-Hier case. If $[[A{]]}_{\rho }^{\mathrm{\Gamma }}\in V_{{\kappa }_i}$, then that denotation is a set; transitivity of $V_{{\kappa }_i}$ also keeps all its elements inside the stage. This proves U-El, while equality of two universe elements gives equality of the same two sets and proves U-El-Eq.

For the representative dependent-closure case, assume $$A_{\rho }:=[[A{]]}_{\rho }^{\mathrm{\Gamma }}\in V_{{\kappa }_i},B_{\rho ,a}:=[[B{]]}_{(\rho ,a)}^{\mathrm{\Gamma },x:A}\in V_{{\kappa }_i}(a\in A_{\rho }).$$ Strong inaccessibility makes $V_{{\kappa }_i}$ closed under the indexed product, so $$[[\prod _{x:A}B{]]}_{\rho }^{\mathrm{\Gamma }}=\prod _{a\in A_{\rho }}{B}_{\rho ,a}\in V_{{\kappa }_i}.$$ This is U-Pi. The $\mathrm{\Sigma }$-, W-, coproduct-, and nullary cases use the corresponding closure operation already defined in definition 73.39 (one line each).

A lift and its argument have literally the same set denotation. This proves Lift-El; closure at the next stage proves Lift-U, and applying the same set operation to equal denotations proves the congruence and commuting rules (one line for each constructor). Finally, the case $i=j$ of U-Cumul is immediate. If and $A\in V_{{\kappa }_i}$, then , hence $A\in V_{{\kappa }_j}$. Because the interpretation is defined on raw expressions, the denotation of $A$ is the same set whether a derivation uses it as a universe element or, by U-El, as a type. These cases extend the simultaneous induction of lemma 28.14. ◻

Proof of Theorem 74.15 — Relative consistency and separation

Proof. Soundness is lemma 74.14. A closed term of $\mathbf{0}$ would denote an element of the empty set, while the displayed Boolean equality would identify the distinct denotations $1$ and $0$. ◻

Proof of Theorem 29.14 — Disjointness of the booleans

Proof. Define $P(b):={\mathsf{If}}_0(\mathbf{1},\mathbf{0},b):{\mathcal{U}}_0$. Congruence sends an assumed equality of booleans to $P(\mathsf{tt})\equiv P(\mathsf{ff}):{\mathcal{U}}_0$. Computation and U-El-Eq give $\mathbf{1}\equiv \mathbf{0}$ as types, so conversion sends $\star :\mathbf{1}$ to a term of $\mathbf{0}$. The second assertion is the Boolean-separation clause of theorem 74.15. ◻

This is a relative model theorem under a strong set-theoretic hypothesis. It proves neither normalization nor decidability, and it does not assert that inaccessible cardinals are necessary for every finite fragment.

Bibliographic notes

The universe pages of Martin-Löf’s predicative paper give the historical closure and hierarchy boundary [ML75]. Generalized level structures are developed by Kovács [Kov22]. The implementation comparison above is deliberately bounded to the displayed interfaces of the fuss-free and Mugen artifacts [SS26, FAM23]; their normalization or elaboration theorems are not imported into this chapter.