Universe Paradoxes and Hurkens's Construction

Instantiating $z:{\mathsf{El}}_1(V)$ at $A:U_1$ uses the outer ${\mathrm{\Pi }}_2$-application and yields a function expecting $r:{\mathsf{El}}_1((A{\to }_1{u}_0){\to }_{1}A{\to }_1{u}_0)$. The applications to $r$ and then $a:{\mathsf{El}}_1(A)$ use ${\mathrm{\Pi }}_1$-application. In the result, $z{\cdot }_{2}A{\cdot }_{1}r$ has type ${\mathsf{El}}_1(A{\to }_1{u}_0)$, so it is the argument expected by $r$. Only the first application, $z{\cdot }_{2}A$, uses ${\mathrm{\Pi }}_2$.

The four displayed conversions have ledgers The first line converts the result of the auxiliary argument in both $L_1$ and $L_2$. The second converts the premise in $L_1$; the third converts the induction premise in $\mathrm{\Omega }$ and $L_2$; and the fourth gives the codomain expected in $L_1$ and $L_2$. Expanding the second and third lines contracts the large-code abstraction in $\mathsf{sb}$, which is the recorded ${\beta }_2$ site. The final application $L_2{\cdot }_0\mathrm{\Omega }$ is typed by the supplied small application operation; it is not reduced. Thus no conversion invokes ${\beta }_0$ or ${\beta }_{01}$.

With $\delta =\mathsf{intro}\circ \mathsf{match}$, equation (RH) at $x,p$ expands to $$\mathsf{match}(\delta x)(p)\equiv T(\delta )(\mathsf{match}(x))(p)\equiv \mathsf{match}(x)(p\circ \delta ).$$ If $h:X_0(p)$, then $s_2(p,h)=\lambda x.h(\delta x)$ has type $X_0(p\circ \delta )$: its final negative premise is converted by the displayed equation. The four uses are distinct. It converts the negative conclusion in the typing of $s_1$, converts the negative conclusion in the typing of $s_2$, identifies $\mathsf{match}(x_0)(p)$ with $X_0(p\circ \delta )$ in $l_0$, and makes the same identification when $l_2(p,h)$ is assigned type $\mathrm{\neg }\mathsf{match}(x_0)(p)$. No other non-beta conversion occurs in the final application $l_0(p_0,l_2,l_1):\mathrm{\perp }$.

Let $\cdot ⊢A\mathsf{type}$. Apply theorem 76.4 to the assumed code $F$ whose decoding is empty, and convert the resulting term to $g:\mathbf{0}$. Empty elimination at the constant motive $A$ gives $$a:={\mathsf{ind}}_{\mathbf{0}}(x.A;g):A.$$ Equivalently, using the recursor of definition 28.3, $$a:={\mathsf{abort}}_A(g),{\mathsf{abort}}_A:\mathbf{0}\to A.$$ Thus every closed type is inhabited under that Hurkens interface. The construction is uniform in $A$; no property of the target type is used beyond its formation judgment.