ch:pure-type-systems: ch:pure-type-systems

The outer product has domain $\ast :◻$ and codomain $\prod _{x:X}X:\ast$ under $X:\ast$. Its decisive premise is therefore $(◻,\ast ,\ast )\in \mathcal{R}$. After deleting that triple, generation rules out the outer product and hence the outer Lam. The inner derivation remains: $$\frac{\begin{array}{c}{\displaystyle \frac{X:\ast ⊢X:\ast }{X:\ast ,x:X⊢x:X}}\mathrm{Var}\\ {\displaystyle \frac{\begin{array}{c}X:\ast ⊢X:\ast \\ X:\ast ,x:X⊢X:\ast \\ (\ast ,\ast ,\ast )\in \mathcal{R}\end{array}}{X:\ast ⊢\prod _{x:X}X:\ast }}\mathrm{Prod}\end{array}}{X:\ast ⊢\lambda (x:X).x:\prod _{x:X}X}\mathrm{Lam}.$$ Thus monomorphic identity needs only $(\ast ,\ast ,\ast )$.

The first product needs $r_2=(◻,\ast ,\ast )$: its domain is $\ast :◻$ and its body $X\to X$ has sort $\ast$. Its least vertex is ${\lambda }_2$.

For the second product, forming the domain kind $\ast \to \ast$ uses $r_{\omega }=(◻,◻,◻)$. Under $F:\ast \to \ast$, the product over $X:\ast$ and the outer product over $F$ both use $r_2$. Hence its least vertex is ${\lambda }_{2\omega }$. Deleting $r_{\omega }$ leaves the annotation $\ast \to \ast$ illegal; deleting $r_2$ blocks the product over $X$.

For the third, the final product over $n:\mathsf{Nat}$ uses $r_{\to }$, but a legal declaration $\mathsf{Vec}:\prod _{n:\mathsf{Nat}}\ast$ uses $r_P=(\ast ,◻,◻)$. Accounting for that required declaration, the least vertex is ${\lambda }_P$. Deleting $r_P$ leaves the family declaration illegal, so $\mathsf{Vec}n$ cannot be formed. This distinction is why merely postulating an unverified constant type would conceal the decisive axis. In every case, lemma 60.6 transports the displayed derivation to any vertex with a larger product-triple set, proving all upward inclusions without rebuilding its rule tree.

Assume $F:\prod _{y:A}D\in \mathrm{\Gamma }$ and $\mathrm{\Gamma }⊢N:A$. The source application is $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}\mathrm{\Gamma }⊢F:\prod _{y:A}D\\ \mathrm{\Gamma }⊢A:s\end{array}}{\mathrm{\Gamma },x:A⊢F:\prod _{y:A}D}}\mathrm{Weak}\\ {\displaystyle \frac{\mathrm{\Gamma }⊢A:s}{\mathrm{\Gamma },x:A⊢x:A}}\mathrm{Var}\end{array}}{\mathrm{\Gamma },x:A⊢Fx:D[x/y]}\mathrm{App}.$$ Substitution with $\mathrm{\Gamma }⊢N:A$ gives $\mathrm{\Gamma }⊢(Fx)[N/x]:D[x/y][N/x]$. By lemma 60.11, $x\notin \mathrm{FV}(D)$: the product type of $F$ is well formed in $\mathrm{\Gamma }$, while $x\notin \mathrm{dom}(\mathrm{\Gamma })$. Together with $x\ne y$ and the chosen freshness of $y$, the substitution-composition lemma reduces the two sides to $FN$ and $D[N/y]$. Equivalently, the target derivation is one App from $\mathrm{\Gamma }⊢F:\prod _{y:A}D$ and $\mathrm{\Gamma }⊢N:A$.

Generation gives $\mathrm{\Gamma }⊢F:\prod _{x:A}B$ and $\mathrm{\Gamma }⊢N:A$. The induction hypothesis for $N{⟶}_{\beta }{N}^{\prime }$ gives $\mathrm{\Gamma }⊢N^{\prime }:A$, so $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢F:\prod _{x:A}B\\ \mathrm{\Gamma }⊢N^{\prime }:A\end{array}}{\mathrm{\Gamma }⊢F{N}^{\prime }:B[N^{\prime }/x]}\mathrm{App}.$$ Compatibility gives $B[N/x]{⟶}_{\beta }^{\ast }B[N^{\prime }/x]$, hence $B[N^{\prime }/x]{=}_{\beta }B[N/x]$. The original application derivation contains a typing of $F:\prod _{x:A}B$. Since that product is not a sort, correctness of types and generation give $\mathrm{\Gamma },x:A⊢B:s_B$; substitution with $\mathrm{\Gamma }⊢N:A$ gives $\mathrm{\Gamma }⊢B[N/x]:s_B$. With this explicit classifier, Conv derives $\mathrm{\Gamma }⊢F{N}^{\prime }:B[N/x]$.

Take constants $a,b$ and $$S=\{s_0,s_1,s_2,s_3\},\mathcal{A}=\{a:s_0,b:s_1\},\mathcal{R}=\{(s_0,s_1,s_2),(s_0,s_1,s_3)\}.$$ From $a:s_0$ and $b:s_1$, weakening gives $x:a⊢b:s_1$. The two Prod instances derive $$\cdot ⊢\prod _{x:a}b:s_2,\cdot ⊢\prod _{x:a}b:s_3.$$ No axiom has the form $s:s$. In the uniqueness proof, the product case tries to infer equality of result sorts from the fixed pair $(s_0,s_1)$. Functionality is exactly the premise that would force $s_2=s_3$; here it fails, and no beta-step converts the distinct constants.

Use these three products as axis witnesses: $$P_2=\prod _{X:\ast }X,P_{\omega }=\prod _{X:\ast }\ast ,P_P=\prod _{x:A}\ast (A:\ast ).$$ For $P_2$, Ax gives $\ast :◻$, Var gives $X:\ast ⊢X:\ast$, and Prod with $(◻,\ast ,\ast )$ gives $P_2:\ast$. For $P_{\omega }$, the two premises have sorts $◻$ and $◻$, so Prod with $(◻,◻,◻)$ gives $P_{\omega }:◻$. For $P_P$, the premises are $A:\ast$ and $x:A⊢\ast :◻$, so Prod with $(\ast ,◻,◻)$ gives $P_P:◻$. In each case, generation applied after deleting the named triple recovers premise sorts convertible to the displayed pair. Since every cube vertex is functional, lemma 60.26 forces those premise sorts to be the same pair. No remaining product triple has that pair, so the witness is no longer typable.

For the redex $(\lambda (x:A_0).M_0)N$, generation yields $$\mathrm{\Gamma },x:A_0⊢M_0:B,\mathrm{\Gamma }⊢\lambda (x:A_0).M_0:\prod _{x:C}D,\mathrm{\Gamma }⊢N:C,$$ and the generated abstraction product gives $\prod _{x:A_0}B{=}_{\beta }\prod _{x:C}D$. Product compatibility yields $A_0{=}_{\beta }C$ and $B{=}_{\beta }D$. Generation of $\mathrm{\Gamma }⊢\prod _{x:A_0}B:s$ gives $\mathrm{\Gamma }⊢A_0:s_0$, so conversion changes the argument derivation to $\mathrm{\Gamma }⊢N:A_0$; substitution gives $\mathrm{\Gamma }⊢M_0[N/x]:B[N/x]$; compatibility gives $B[N/x]{=}_{\beta }D[N/x]$. Correctness of types for the function premise, followed by generation and substitution with $\mathrm{\Gamma }⊢N:C$, gives $\mathrm{\Gamma }⊢D[N/x]:s_D$; a final conversion using that classifier restores the application’s generated result type.

If Conv omits its premise $\mathrm{\Gamma }⊢B:s$, it can replace a legal type by an arbitrary beta-equal raw expression without exhibiting a classifier for the target. The induction above then lacks the sort premise needed by its final conversion and by context extension. The failed presupposition is that every right-hand side of a typing judgment is itself classified.

Both systems contain the sort $\ast$ and the ordinary-product triple $(\ast ,\ast ,\ast )$. The one-sort system has the circular axiom $\ast :\ast$; ${\lambda }_C$ instead has two sorts, the axiom $\ast :◻$, and the four cube triples. Substitution is proved by rule induction for every PTS schema, so it applies to both. Strong normalization is the imported instance theorem for the eight cube systems and its reducibility interpretation uses the acyclic sort structure. Membership in the general PTS schema provides no such interpretation for $\ast :\ast$.