ch:first-class-universe-levels: ch:first-class-universe-levels

Associativity and commutativity collect the four generators. Inflation gives $\alpha \bigsqcup {\alpha }^{+}\equiv {\alpha }^{+}$ and $\beta \bigsqcup {\beta }^{+}\equiv {\beta }^{+}$, so $$({\alpha }^{+}\bigsqcup \beta )\bigsqcup (\alpha \bigsqcup {\beta }^{+})\equiv {\alpha }^{+}\bigsqcup {\beta }^{+}.$$ Writing the normal form as $u$, idempotence gives $u\bigsqcup ({\alpha }^{+}\bigsqcup {\beta }^{+})\equiv u$. This is the defining witness of $\mathsf{Below}(u,{\alpha }^{+}\bigsqcup {\beta }^{+})$.

One suitable term is $$\lambda h.(h0\mathbb{N}0,h{0}^{+}{\mathcal{U}}_0\mathbb{N},h{0}^{+}({\mathsf{Lift}}_{0^{+}}\mathbb{N})(\mathsf{lift}0)),$$ with type $$(\mathrm{\Pi }t:\mathsf{Level}.\mathrm{\Pi }A:{\mathcal{U}}_t.A\to A)\to \mathbb{N}\times {\mathcal{U}}_0\times {\mathsf{Lift}}_{0^{+}}\mathbb{N}.$$ The three applications use respectively $\mathbb{N}:{\mathcal{U}}_0$, ${\mathcal{U}}_0:{\mathcal{U}}_{0^{+}}$, and ${\mathsf{Lift}}_{0^{+}}\mathbb{N}:{\mathcal{U}}_{0\bigsqcup 0^{+}}\equiv {\mathcal{U}}_{0^{+}}$. The higher-rank product $\mathrm{\Pi }t:\mathsf{Level}.\mathrm{\Pi }A:{\mathcal{U}}_t.A\to A$ is well formed but inhabits no single universe, because its codomain level depends on the bound term $t$.

For $z:{\mathsf{Lift}}_u({\mathsf{Lift}}_{v}A)$, define $$F(z)={\mathsf{lift}}_{u\bigsqcup v}({\mathsf{lower}}_v({\mathsf{lower}}_{u}z)).$$ For $w:{\mathsf{Lift}}_{u\bigsqcup v}A$, define $$G(w)={\mathsf{lift}}_u({\mathsf{lift}}_v({\mathsf{lower}}_{u\bigsqcup v}w)).$$ Two uses of Lift-F place the source of $F$ in ${\mathcal{U}}_{t\bigsqcup v\bigsqcup u}$; one use places its target in ${\mathcal{U}}_{t\bigsqcup (u\bigsqcup v)}$, and associativity converts the levels. The same calculation types $G$. Repeated Lift-$\beta$ lowers both composites to the corresponding input after lowering. Applying Lift-$\eta$ outward once on the single lift and twice on the nested lift gives $F(G(w))\equiv w$ and $G(F(z))\equiv z$. With syntactic level identity, the universe conversion between $(t\bigsqcup v)\bigsqcup u$ and $t\bigsqcup (u\bigsqcup v)$ would fail; the decision procedure of corollary 117.10 supplies that equality.

The principal calculus has level terms $t::=0\mid t^{+}\mid t\bigsqcup t$, the typing judgment $\mathrm{\Gamma }⊢t:\mathsf{Level}$, and universes ${\mathcal{U}}_t$. At that signature, Corollary 4.3 of Danielsson, Favier, and Kubánek gives decidable judgmental equality, as recorded in theorem 117.11.

The bounded calculus has level expressions generated by zero, successor, and join, but a level is typed by a bound-sensitive judgment . At that signature Chan and Weirich prove subject reduction, type safety, consistency, and canonicity; normalization of open terms and decidable checking are not among the proved claims.

The displacement system takes external level expressions in a hierarchy $H(\mathrm{\Delta })$. Its core judgments include $\mathrm{\Gamma }{⊢}_{H(\mathrm{\Delta })}A{\mathsf{type}}_{\ell }$ and $\mathrm{\Gamma }{⊢}_{H(\mathrm{\Delta })}e:A$; closed declarations may be acted on by a displacement. Theorem 3.10 of Hou, Angiuli, and Mullanix sends every hierarchy theory, under its stated smallness hypotheses, faithfully into a displacement algebra.

None of these results transfers by shared notation. Decidable equality for the principal calculus does not decide the bound-sensitive relation of the bounded calculus or the external order of an arbitrary displacement algebra. Subject reduction for bounded levels does not prove normalization of the principal or displacement systems. The displacement representation theorem does not type the higher-rank $\mathsf{twiceLevel}$ term and proves neither bounded-level canonicity nor the principal calculus’s erasure theorem. Each transfer would require a typed translation and preservation of the relevant conversion or reduction judgment.

The source ledger is

The first column is exactly the theorem package of theorem 117.11; the second is the bounded-system package recorded in its comparison card. Blank or open cells cannot be filled by transporting a result across the different level, lift, and bound rules.