ch:universes: ch:universes

The exercise states the claim for universe-element derivations in an arbitrary well-formed context; this supplies the induction hypothesis beneath binders. For a base universe element $\mathbf{0},\mathbf{1},\mathbf{2},\mathbb{N}$, replay the same rule at level $i+1$ and take $A^{\prime }=A$. The U-Hier case is the same, since implies .

For illustration, suppose the last rule is U-Pi. Applying the induction hypotheses to its premises, with context conversion where needed, gives In the last judgment, $B$ denotes the original body transported from $\mathrm{\Gamma },x:A$ to $\mathrm{\Gamma },x:A^{\prime }$ along the symmetric domain equality. Rule U-Pi at level $i+1$ constructs $\prod _{x:A^{\prime }}{B}^{\prime }:{\mathcal{U}}_{i+1}$, and dependent-product congruence gives $$\mathrm{\Gamma }⊢\prod _{x:A^{\prime }}{B}^{\prime }\equiv \prod _{x:A}B\mathsf{type}.$$ For $\mathrm{\Sigma }$ and $\mathsf{W}$, instantiate the same argument with U-Sig/Lift-Sig and U-W/Lift-W, respectively; the dependent context conversion is unchanged (four lines each). For a coproduct, use the two component induction hypotheses followed by U-Sum and Lift-Sum (two lines). These are all constructors allowed by the exercise, so the induction is complete.

Define externally $${\mathsf{Lift}}^{i\to i}A:=A,{\mathsf{Lift}}^{i\to (j+1)}A:={\mathsf{Lift}}_j({\mathsf{Lift}}^{i\to j}A).$$ Induction on $j-i$ first gives ${\mathsf{Lift}}^{i\to j}A:{\mathcal{U}}_j$. Using Lift-El at each successor step and transitivity then gives ${\mathsf{Lift}}^{i\to j}A\equiv A$ as types. The same induction proves the universe equality for products. Whenever ${\mathsf{Lift}}^{i\to j}B$ occurs in the lifted binder context, it denotes the universe element first formed in $\mathrm{\Gamma },x:A$ and then transported to $\mathrm{\Gamma },x:{\mathsf{Lift}}^{i\to j}A$ along the accumulated type equality. With that convention, the successor step is where the first line uses the induction hypothesis under Lift-Cong and the second uses Lift-Pi. Both sides of this successor step inhabit ${\mathcal{U}}_{j+1}$. Renaming the successor target $j+1$ to the exercise’s target level proves the displayed judgment; the base target $i$ is reflexivity.

For $\sum _{x:\prod _{a:A_i}{B}_j(a)}\prod _{c:C_k(x)}{D}_l(x,c)$ the cumulative rule U-Cumul raises every smaller premise to the chosen classifier. The two products therefore live at $max(i,j)$ and $max(k,l)$, and the outer sum at $m=max(i,j,k,l)$. Thus the least solution is obtained by assigning each fresh result variable the indicated maximum; a strict lift from level $r$ adds the constraint $r+1\le s$. Adding ${\mathcal{U}}_i:{\mathcal{U}}_i$ adds the strict formation edge $i+1\le i$. Summing edge weights around this one-edge cycle gives $1\le 0$, so no level assignment exists.

The final rule is U-Pi at level $1$. Its domain and codomain are both the lower universe viewed as an element of ${\mathcal{U}}_1$: For completeness, the context in the second premise is formed by $$\frac{\begin{array}{c}\cdot \mathsf{ctx}\\ {\displaystyle \frac{\cdot \mathsf{ctx}}{\cdot ⊢{\mathcal{U}}_0\mathsf{type}}}\mathrm{U}-{\mathrm{Form}}_0\end{array}}{X:{\mathcal{U}}_0\mathsf{ctx}}\mathrm{Ctx}-\mathrm{Ext}.$$ Equivalently, U-El applied to the first U-Hier premise also recovers $\cdot ⊢{\mathcal{U}}_0\mathsf{type}$. Thus the universe-specific rules are U-Form at level $0$, U-Hier from level $0$ to level $1$ twice, and U-Pi at level $1$.

Take $$\mathrm{comp}:=\lambda X.\lambda Y.\lambda Z.\lambda g.\lambda f.\lambda x.g(f(x)).$$ After introducing $X,Y,Z:{\mathcal{U}}_0$, rule U-El turns each of those universe elements into a type. In the further context $$g:Y\to Z,f:X\to Y,x:X,$$ two uses of $\mathrm{\Pi }$-elim give $f(x):Y$ and then $g(f(x)):Z$. Three inner uses of $\mathrm{\Pi }$-intro abstract $x,f,g$; three outer uses abstract $Z,Y,X$. The formation premises for ordinary arrows use $\mathrm{\Pi }$-form; the domains $X,Y,Z$ are available as types by U-El, and ${\mathcal{U}}_0$ itself is a type by U-Form. Consequently $$\cdot ⊢\mathrm{comp}:\prod _{X:{\mathcal{U}}_0}\prod _{Y:{\mathcal{U}}_0}\prod _{Z:{\mathcal{U}}_0}(Y\to Z)\to (X\to Y)\to (X\to Z).$$ No universe eliminator is used; universes have none. Only U-El is needed to let the quantified universe elements serve as ordinary types.

Assume the first premise of U-Pi, $\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$. Its own presuppositions include $\mathrm{\Gamma }\mathsf{ctx}$ and $\mathrm{\Gamma }⊢{\mathcal{U}}_i\mathsf{type}$; the latter is also an instance of U-Form. Applying U-El gives the missing domain formation judgment: $$\frac{\mathrm{\Gamma }⊢A:{\mathcal{U}}_i}{\mathrm{\Gamma }⊢A\mathsf{type}}\mathrm{U}-\mathrm{El}.$$ Context extension then gives $$\frac{\begin{array}{c}\mathrm{\Gamma }\mathsf{ctx}\\ \mathrm{\Gamma }⊢A\mathsf{type}\end{array}}{\mathrm{\Gamma },x:A\mathsf{ctx}}\mathrm{Ctx}-\mathrm{Ext}.$$ This is exactly the context required to state the second premise $\mathrm{\Gamma },x:A⊢B:{\mathcal{U}}_i$. From that premise, U-El also supplies $\mathrm{\Gamma },x:A⊢B\mathsf{type}$, so the raw product in the conclusion is well-formed by ordinary $\mathrm{\Pi }$-formation. Nothing beyond the two displayed universe-element premises and their standard presuppositions is needed.

Assume $$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i,\mathrm{\Gamma },x:A⊢B:{\mathcal{U}}_i.$$ For the left side, U-Pi at level $i$ gives $\prod _{x:A}B:{\mathcal{U}}_i$, and Lift-U then gives $${\mathsf{Lift}}_i(\prod _{x:A}B):{\mathcal{U}}_{i+1}.$$ For the right side, Lift-U first gives $${\mathsf{Lift}}_{i}A:{\mathcal{U}}_{i+1}\text{in }\mathrm{\Gamma },{\mathsf{Lift}}_{i}B:{\mathcal{U}}_{i+1}\text{in }\mathrm{\Gamma },x:A.$$ Rule Lift-El yields ${\mathsf{Lift}}_{i}A\equiv A\mathsf{type}$. Symmetry followed by context conversion transports the second judgment to $$\mathrm{\Gamma },x:{\mathsf{Lift}}_{i}A⊢{\mathsf{Lift}}_{i}B:{\mathcal{U}}_{i+1}.$$ Now U-Pi at level $i+1$ gives $$\prod _{x:{\mathsf{Lift}}_{i}A}{\mathsf{Lift}}_{i}B:{\mathcal{U}}_{i+1}.$$ Thus both terms compared by Lift-Pi inhabit the stated classifier in the same context. The context conversion justified by Lift-El is the only nonliteral bookkeeping step.

In context $X:{\mathcal{U}}_0$, the variable judgment $X:{\mathcal{U}}_0$, used twice with U-Pi at level $0$, gives $$\prod _{x:X}X:{\mathcal{U}}_0.$$ Rule Lift-U therefore gives $$X:{\mathcal{U}}_0⊢{\mathsf{Lift}}_0(\prod _{x:X}X):{\mathcal{U}}_1.$$ The outer domain satisfies ${\mathcal{U}}_0:{\mathcal{U}}_1$ by U-Hier, so U-Pi at level $1$ yields $$\cdot ⊢\prod _{X:{\mathcal{U}}_0}{\mathsf{Lift}}_0(\prod _{x:X}X):{\mathcal{U}}_1.$$ In context $X:{\mathcal{U}}_0$, Lift-El gives $${\mathsf{Lift}}_0(\prod _{x:X}X)\equiv \prod _{x:X}X\mathsf{type}.$$ Dependent-product congruence with the reflexive equality on the outer domain therefore gives $$\cdot ⊢\prod _{X:{\mathcal{U}}_0}{\mathsf{Lift}}_0(\prod _{x:X}X)\equiv \prod _{X:{\mathcal{U}}_0}\prod _{x:X}X\mathsf{type}.$$ The left-hand type is an element of ${\mathcal{U}}_1$ and is judgmentally equal as a type to the polymorphic-identity type. By convention 29.3, the latter is therefore ${\mathcal{U}}_1$-small.

To avoid capture, call the predecessor $k$ and the recursively computed universe element $R$. Define $${\mathsf{Cases}}_i(A_z,x.A_s,n):={\mathsf{rec}}_{\mathbb{N}}(A_z,\lambda k.\lambda R.A_s[k/x],n):{\mathcal{U}}_i.$$ In the step context $k:\mathbb{N},R:{\mathcal{U}}_i$, the term $A_s[k/x]:{\mathcal{U}}_i$ is obtained by substitution from the supplied successor branch and then weakened by $R$. The recursive result is deliberately discarded. Natural-number computation gives equalities at type ${\mathcal{U}}_i$: Applying U-El-Eq to these two term equalities gives exactly This is case analysis rather than recursive large elimination because the step branch does not use $R$.

Define a universe-valued discriminator $$P:=[\lambda x:A.\mathbf{1},\lambda y:B.\mathbf{0}]:A+B\to {\mathcal{U}}_0,$$ using U-Unit and U-Void for the two branch terms. Its constructor computations are $$P(\mathsf{inl}(a))\equiv \mathbf{1},P(\mathsf{inr}(b))\equiv \mathbf{0}:{\mathcal{U}}_0.$$ Suppose $h:\mathsf{inl}(a)\equiv \mathsf{inr}(b):A+B$ is a derivable judgmental equality. Application congruence gives $$P(\mathsf{inl}(a))\equiv P(\mathsf{inr}(b)):{\mathcal{U}}_0.$$ Composing with the two constructor computations yields $\mathbf{1}\equiv \mathbf{0}:{\mathcal{U}}_0$. Rule U-El-Eq turns this into $\mathbf{1}\equiv \mathbf{0}\mathsf{type}$. Since $\star :\mathbf{1}$, conversion gives the closed term $$\cdot ⊢\star :\mathbf{0}.$$ Thus a judgmental equality between opposite coproduct injections entails syntactic inconsistency, exactly as Boolean disjointness does.

Use recursion into ${\mathcal{U}}_0$, with the recursive result itself serving as the tail universe element: $$\mathsf{Vec}:=\lambda A.\lambda n.{\mathsf{rec}}_{\mathbb{N}}(\mathbf{1},\lambda k.\lambda R.A\times R,n):{\mathcal{U}}_0\to \mathbb{N}\to {\mathcal{U}}_0.$$ In the step context $A:{\mathcal{U}}_0,k:\mathbb{N},R:{\mathcal{U}}_0$, the nondependent product $A\times R$ is an element of ${\mathcal{U}}_0$ by U-Sig at level $0$. The two natural-number computation rules and Pi-beta give By U-El-Eq, the same equations hold as equalities of types.

Use the dependent motive $$C(n):=\mathsf{EqN}(n,n).$$ At zero, the characteristic equation $C(\mathsf{0})\equiv \mathbf{1}$ allows $\star :\mathbf{1}$ to be converted to a term $c_0:C(\mathsf{0})$. For the step, in context $k:\mathbb{N},e:C(k)$, the equation $$C(\mathsf{suc}(k))=\mathsf{EqN}(\mathsf{suc}(k),\mathsf{suc}(k))\equiv \mathsf{EqN}(k,k)=C(k)$$ allows the unchanged raw term $e$ to be converted to type $C(\mathsf{suc}(k))$. Let ${\overline{e}}_k$ denote that converted occurrence and set $$r:=\lambda n.{\mathsf{ind}}_{\mathbb{N}}(k.C(k);c_0,\lambda k.\lambda e.{\overline{e}}_k;n):\prod _{n:\mathbb{N}}\mathsf{EqN}(n,n).$$ At zero, Pi-beta and natural-number computation give $$r(\mathsf{0})\equiv c_0\equiv \star :C(\mathsf{0}).$$ Converting the classifier along $C(\mathsf{0})\equiv \mathbf{1}$ yields the requested judgment $$\cdot ⊢r(\mathsf{0})\equiv \star :\mathbf{1}.$$ At successors the same construction also gives $r(\mathsf{suc}(k))\equiv r(k)$, with the right-hand term silently converted from $C(k)$ to $C(\mathsf{suc}(k))$.

Assume $$h:\mathsf{suc}(m)\equiv \mathsf{suc}(n):\mathbb{N}.$$ By the preceding exercise, $r(m):\mathsf{EqN}(m,m)$. The successor computation for $\mathsf{EqN}$, used symmetrically, gives $$\mathsf{EqN}(m,m)\equiv \mathsf{EqN}(\mathsf{suc}(m),\mathsf{suc}(m))\mathsf{type}.$$ Apply congruence to the type-valued function $\lambda z.\mathsf{EqN}(\mathsf{suc}(m),z)$ and the equality $h$. This gives $$\mathsf{EqN}(\mathsf{suc}(m),\mathsf{suc}(m))\equiv \mathsf{EqN}(\mathsf{suc}(m),\mathsf{suc}(n))\mathsf{type}.$$ A final characteristic computation gives $$\mathsf{EqN}(\mathsf{suc}(m),\mathsf{suc}(n))\equiv \mathsf{EqN}(m,n)\mathsf{type}.$$ By transitivity, $\mathsf{EqN}(m,m)\equiv \mathsf{EqN}(m,n)$ as types. Converting the closed term $r(m)$ along this equality produces $$e:=r(m):\mathsf{EqN}(m,n),$$ where the displayed definition keeps the raw term and changes only its typing derivation.

Define $$G:=\lambda n.{\mathsf{rec}}_{\mathbb{N}}(\mathbb{N},\lambda k.\lambda R.R\to \mathbb{N},n):\mathbb{N}\to {\mathcal{U}}_0.$$ The step is well-typed because $R:{\mathcal{U}}_0$ and $\mathbb{N}:{\mathcal{U}}_0$, so U-Pi at level $0$ gives $R\to \mathbb{N}:{\mathcal{U}}_0$. Computation gives Now $\mathbb{N}:{\mathcal{U}}_0$, and in context $n:\mathbb{N}$ application gives $G(n):{\mathcal{U}}_0$. Hence U-Sig at level $0$ yields $$\cdot ⊢\sum _{n:\mathbb{N}}G(n):{\mathcal{U}}_0.$$ Thus the dependent sum is not merely equal to a small type; it is itself a element of ${\mathcal{U}}_0$, and so is ${\mathcal{U}}_0$-small by reflexivity.

The constraint $v\le u+1$ belongs to $P$: it restricts the external parameters but does not add a lower bound on the unknown $m$. Splitting the other maximum gives $v+2\le m$ and $u\le m$; the latter is dominated by $u+1\le m$. Hence the least symbolic choice is $$m=max(u+1,v+2).$$ For every parameter assignment satisfying $P$, any solution must dominate both surviving lower bounds, so this solution is principal. The hypothesis of proposition 74.10 used here is precisely the separation between parameter-only constraints in $P$ and constraints with the unknown on their right-hand side.