First-Class Universe Levels and Level Polymorphism

Proof. For $a:A$, Lift-$\beta$ gives $\mathsf{lower}(\mathsf{lift}a)\equiv a$, which is one inverse law.

For the other, fix $b:{\mathsf{Lift}}_{u}A$ and apply Lift-$\eta$ to the pair $\mathsf{lift}(\mathsf{lower}b)$ and $b$. Both are terms of ${\mathsf{Lift}}_{u}A$ by Lift-I and Lift-E, and its third premise is discharged by Lift-$\beta$ at $a:=\mathsf{lower}b$, which gives $\mathsf{lower}(\mathsf{lift}(\mathsf{lower}b))\equiv \mathsf{lower}b$. The conclusion is $\mathsf{lift}(\mathsf{lower}b)\equiv b$, the second inverse law. ◻

Proof. Rule induction on the derivation of $J$. Variable and binder cases are the ordinary substitution cases. For L-Suc and L-Join, apply the induction hypotheses to their level premises and rebuild the rule. For L-Univ, substitution changes ${\mathcal{U}}_t$ to ${\mathcal{U}}_u$ and its type to ${\mathcal{U}}_{u^{+}}$. For Lift-F, substitution commutes with $t\bigsqcup v$ by the syntactic definition of substitution. Every level equality axiom is an equation schema and remains an instance after replacing $t$ by $u$. The remaining type-former, conversion, and computation cases are the corresponding ordinary substitution rules. ◻

Proof. For a finite map $M$, let $R(M)$ be the ordered join of its indicated iterates, with $R(\varnothing )=0$. We first prove $v\equiv R(N(v))$ by structural induction on $v$. The zero and variable cases use the definition of $R$. The join case uses the two induction hypotheses; associativity, commutativity, and idempotence then implement pointwise maximum. In the successor case, the distribution equation moves successor through the ordered join. The empty join becomes the constant iterate $(\star ,1)$, as required.

It remains to justify entries deleted during join. Inflation removes an iterate below a larger iterate of the same variable. Moreover, $0\bigsqcup x\equiv x$; applying successor $m$ times and distributing it shows that a variable iterate with exponent at least $m$ absorbs the constant iterate $(\star ,m)$. Hence every deletion preserves equality to $R(N(v))$. If $N(t)=N(u)=M$, the two induction results give $t\equiv R(M)$ and $u\equiv R(M)$. Symmetry and transitivity yield $t\equiv u$. ◻

Proof. Interpret levels in the natural numbers. A valuation $\sigma$ assigns a natural number to each level variable; extend it by $[[0{]]}_{\sigma }:=0$, $[[t^{+}{]]}_{\sigma }:=[[t{]]}_{\sigma }+1$, and $[[t\bigsqcup u{]]}_{\sigma }:=max([[t{]]}_{\sigma },[[u{]]}_{\sigma })$. Each of the six equations of definition 117.2 is valid in $(\mathbb{N},max,0,+1)$: left identity because $0$ is least, associativity, commutativity and idempotence because $max$ is a semilattice operation, distribution because $max(m,n)+1=max(m+1,n+1)$, and inflation because $max(m,m+1)=m+1$. Hence $t\equiv u$ implies $[[t{]]}_{\sigma }=[[u{]]}_{\sigma }$ for every $\sigma$.

The proof of lemma 117.8 gives $v\equiv R(N(v))$, so it also gives $[[v{]]}_{\sigma }=[[R(N(v)){]]}_{\sigma }$, and the latter is the maximum of $m$ over any constant entry $(\star ,m)$ together with $\sigma (x)+k$ over the variable entries $(x,k)$. It therefore suffices to separate two distinct maps produced by definition 117.7. Let $M\ne M^{\prime }$ be two such maps.

Suppose first that their variable entries differ at some $x$. Take $\sigma (x):=n$ and $\sigma (y):=0$ for every other variable. Every term of the maximum other than the one contributed by $x$ is bounded by a constant independent of $n$, while $x$ contributes $n+k$ when $(x,k)\in M$ and contributes nothing when $x$ is absent. For $n$ larger than every exponent occurring in $M$ or $M^{\prime }$, the two maxima are $n+k$ and $n+k^{\prime }$ with $k\ne k^{\prime }$, or one is $n+k$ and the other is bounded independently of $n$; in both cases they differ.

Otherwise the variable entries agree and the constant entries differ. Take $\sigma (y):=0$ for every variable. A map produced by definition 117.7 retains $(\star ,m)$ only when every variable entry has exponent strictly below $m$, so its maximum at this valuation is $m$ when a constant entry is present and is the largest variable exponent otherwise. If both maps carry constant entries $m\ne m^{\prime }$, the maxima differ. If exactly one does, its maximum is $m$ and the other’s is the largest shared variable exponent, which is strictly below $m$. If neither does, the maps agree, contradicting $M\ne M^{\prime }$.

So distinct maps have distinct interpretations at some valuation, and equal levels have equal maps. ◻

Proof. The maps are finite and computed by structural recursion, so equality of maps is decidable. lemma 117.8 gives one implication and lemma 117.9 the other. ◻

Proof. We construct the logical relation and derive each consequence. Use external indices $\ell \in \mathbb{N}\cup \{\omega \}$. Define reducibility ${\mathsf{Red}}_{\ell }(\mathrm{\Gamma };J)$ by well-founded induction on $\ell$, with type reducibility inductive and reducible type and term equality recursive in a type-reducibility witness. The relation is parameterized by generic type, term, and atomic-neutral equality relations that are partial equivalence relations, stable under weakening, conversion, and weak-head expansion, and contained in judgmental equality.

The first-class level clause is independent of $\ell$. A reducible level weak-head reduces to $0$, a successor of a reducible level, or a neutral built from an atomic neutral and joins. Define its external realizer by $$\uparrow 0=0,\uparrow (t^{+})=1+\uparrow t,\uparrow (t\bigsqcup u)=max(\uparrow t,\uparrow u),$$ and assign realizer $0$ to an atomic neutral. Mutual induction on reducible levels and their equality proves $$t\equiv u⟹\uparrow t=\uparrow u,t\bigsqcup u\equiv u⟹\uparrow t\le \uparrow u.$$ The zero, successor, and atomic-neutral cases are immediate. In the join case use the induction hypotheses and the corresponding equality of maxima. Associativity, commutativity, idempotence, and absorption are the same laws for maximum; the rule relating a neutral join to a successor uses the second displayed implication. This covers every level-equality generator.

A universe ${\mathcal{U}}_t$ is reducible at external level $\ell$ when $t$ is a reducible level and ; an element of that universe is a type reducible at external level $\uparrow t$. Neutral types, Level, $\mathrm{\Pi }$, $\mathrm{\Sigma }$, natural numbers, unit, empty, identity, and lifted types have their standard Kripke clauses. In the lift clause, $\mathsf{lift}$ and $\mathsf{lower}$ transport the underlying reducible term, and Lift-$\beta$ and Lift-$\eta$ make those transports inverse. The strict inequality in the universe clause makes recursive calls well founded.

Prove the fundamental lemma simultaneously for context formation, typing, type equality, and term equality. Variables use the reducible substitution. The structural, $\mathrm{\Pi }$, $\mathrm{\Sigma }$, natural-number, unit, empty, and identity cases are the ordinary Kripke cases. L-Zero, L-Suc, and L-Join use the level construction above; every semilattice equality uses the corresponding realizer equality. L-Univ uses . Lift-F, Lift-I, and Lift-E use the lift clause, and the two lift equalities use its inverse laws. Substitution uses weakening of the relation and its Kripke quantification. Conversion uses irrelevance of reducibility witnesses. These cases exhaust the system card, so every well-typed object is reducible.

Instantiate the generic equality by judgmental equality. A closed reducible natural weak-head reduces to zero or a successor chain, because the neutral case is impossible in the empty context; this proves canonicity. A closed term of the empty type would have to reduce to a neutral, also impossible, so the theory is consistent. Every reducible object has a weak-head normal form. Comparing the outer clauses of two reducibly equal types gives injectivity and nonconfusion.

For algorithmic equality, normalize levels to finite views consisting of a natural offset together with atomic neutral summands. Join is computed by maximum on offsets and union-with-domination on summands. Structural induction proves that view computation is deterministic and validates all semilattice equations; equality of finite views is decidable. Extend the usual mutually defined weak-head, type, term, and neutral comparisons by this level comparison and by congruence for universes and lifts. The resulting relations satisfy the generic-equality interface: weakening and conversion are inductions on comparison, weak-head expansion follows from determinism, and the level equations follow from the view calculation. Applying the fundamental lemma again proves completeness. Soundness is an induction on the comparison derivation. On well-formed inputs, decide judgmental equality by running the finite comparison; recursively reading its witnesses produces eta-long normal forms.

Typing is decided by mutual recursion only for the stated syntactic classes. In a context of checkable types, check a checkable term against a checkable type using decidable conversion. For an inferable term, recurse on syntax. A product first infers a universe for its domain and then checks its codomain in the extended context; a lift without its level annotation is not inferable. Every recursive call is on a proper subterm, proving termination and item 3. No rule handles arbitrary raw terms.

For item 4, define erasure structurally. All level expressions, universes, and type formers erase; $\mathsf{lift}$ and $\mathsf{lower}$ erase to their arguments. Relevant lambdas and applications erase homomorphically. In the non-strict translation an erased application drops its argument and an erased lambda substitutes a fixed looping term for its binder; in the strict translation the erased argument becomes a value placeholder. Prove by induction on the source reduction that erasure simulates each step in the appropriate target closure. The new level steps erase on both sides. Lift beta erases to reflexivity, and lift eta changes no runtime term. The ordinary beta, constructor, pair, and eliminator cases use the substitution–erasure lemma, proved by structural induction.

The graded fundamental lemma, by induction on the typing and usage derivations, says that a well-resourced source natural is related to its erasure. At natural numbers the relation exposes a numeral $n$; its source component gives reduction of $t$ to $\underset{―}{n}$, and its target component gives reduction of either erasure to $\underset{―}{n}$. The empty and weak-$\mathrm{\Sigma }$/unit match cases are exactly where the first two hypotheses of item 4 discharge otherwise stuck erased eliminations. The typing and usage hypotheses supply the remaining two premises. Therefore the claimed $n$ exists for both strictnesses.

The construction is noncumulative, uses homogeneous products, and restricts typing to the stated classes. The proof therefore yields none of the three excluded extensions. ◻