Computational type theory, elaboration, and clause compilation

The frozen Nuprl-style computational fragment

Evaluation is the deterministic lazy relation of convention 91.1. Integers, abstractions, pairs, and type formers are canonical at the root. The selected noncanonical root computations are $$(\lambda x.b)a\stackrel{C-\beta }{{⇝}_0}b[a/x],\mathsf{spread}((a,b);x,y.c)\stackrel{C-spread}{{⇝}_0}c[a/x,b/y],$$ together with the displayed integer operations after their principal arguments evaluate. Pair components and abstraction bodies are not evaluated to make the enclosing term canonical. The compatible closure of these roots is ${⟶}_{\mathcal{L}}$; ${\equiv }_{\mathcal{L}}$ is its reflexive, symmetric, transitive closure. Theorem 91.12 states that closure assignment and every assigned member relation are invariant under this conversion.

The candidate system ${\mathcal{C}}_i(A,B,R)$ is the least evaluation-saturated closure containing the integer triple and these generators:

1. from an equal domain and a functional family of equal fibers, generate equal dependent function types with (91.2) and equal dependent pair types with (91.3);

2. from an equal ambient type and pairwise equal endpoints, generate equal equality types with (91.4);

3. from an equal ambient type and a functional family of equal predicate types, generate equal set types with (91.5);

4. after constructing ${\mathcal{C}}_i$, generate ${\mathcal{C}}_{i+1}({\mathcal{U}}_i,{\mathcal{U}}_i,R_{{\mathcal{U}}_i})$, where $$R_{{\mathcal{U}}_i}(A,B)⟺\mathrm{\exists }R.{\mathcal{C}}_i(A,B,R).$$

Constructor tags are disjoint and injective, and each functional fiber family is invariant under equal domain representatives. These are premises of the closure; global uniqueness of assigned PERs is the conclusion of theorem 91.8, and member-relation computation stability is theorem 91.12.

At universe level $i$, closed type equality, membership, and member equality are For a functional telescope, the open judgment is the two-substitution clause of definition 91.21. The global artifact theorem theorem 91.23 equates its two full close(univ) sequent encodings; the fixed-level list correspondence is the separate local result proposition 91.25. The open judgment’s inhabited conclusion means that for every pair of equal substitutions the assigned cross-fiber PER has some element in its domain. In every derived rule below, each conclusion type and dependent family is assumed well formed and functional under equal substitutions. The complete derived rules used in the chapter are

$\mathrm{\Gamma },n:\mathbb{N}{⊢}_{i}n=n\in \mathbb{N}$

$\mathrm{\Gamma }{⊢}_{i}a=b\in \mathbb{N}$

$\mathrm{\Gamma }{⊢}_{i}a+1=b+1\in \mathbb{N}$

$\mathrm{\Gamma },x:A{⊢}_{i}b=b^{\prime }\in B$

$\mathrm{\Gamma }{⊢}_i\lambda x.b=\lambda x.b^{\prime }\in \prod _{x:A}B$

$\mathrm{\Gamma }{⊢}_{i}f=g\in \prod _{x:A}B$$\mathrm{\Gamma }{⊢}_{i}a=a^{\prime }\in A$

$\mathrm{\Gamma }{⊢}_{i}fa=g{a}^{\prime }\in B[a/x]$

$\mathrm{\Gamma }{⊢}_{i}a=a^{\prime }\in A$$\mathrm{\Gamma }{⊢}_{i}b=b^{\prime }\in B[a/x]$

$\mathrm{\Gamma }{⊢}_i(a,b)=(a^{\prime },b^{\prime })\in \sum _{x:A}B$

$\mathrm{\Gamma }{⊢}_{i}p=q\in \sum _{x:A}B$$\mathrm{\Gamma },z:\sum _{x:A}B{⊢}_{i}C(z)=C(z)\mathsf{type}$$\mathrm{\Gamma },x:A,y:B{⊢}_{i}c=c^{\prime }\in C((x,y))$

$\mathrm{\Gamma }{⊢}_i\mathsf{spread}(p;x,y.c)=\mathsf{spread}(q;x,y.c^{\prime })\in C(p)$

$\mathrm{\Gamma }{⊢}_{i}a=b\in A$

$\mathrm{\Gamma }{⊢}_i\mathsf{axiom}=\mathsf{axiom}\in {\mathsf{Eq}}_A(a,b)$

$\mathrm{\Gamma }{⊢}_{i}a=a^{\prime }\in A$$\mathrm{\Gamma }{⊢}_{i}p=p\in B[a/x]$

$\mathrm{\Gamma }{⊢}_{i}a=a^{\prime }\in \{x:A\mid B\}$

$\mathrm{\Gamma }{⊢}_{i}a=a^{\prime }\in \{x:A\mid B\}$

$\mathrm{\Gamma }{⊢}_{i}a=a^{\prime }\in A$

$\mathrm{\Gamma }{⊢}_{i}a=a\in \{x:A\mid B\}$

$\mathrm{\Gamma }{⊢}_{i}B[a/x]\mathsf{inhabited}$

The quotient side condition of definition 91.36 fixes the old level $i$ and defines ${\mathsf{Inh}}_i(P)⟺\mathrm{\exists }u.{\mathsf{Mem}}_i(u;P).$ Every relation program $E(a,b)$ is an old-system type ${\mathsf{Ty}}_i(E(a,b))$, and its functionality clause is stated with ${\mathsf{TyEq}}_i$. This prevents the admissibility test from referring recursively to the quotient extension. The separately proved closure ${\mathcal{C}}_i^{\mathsf{q}}$ repeats evaluation and every integer, $\mathrm{\Pi }$, $\mathrm{\Sigma }$, equality, and set generator over the extended systems, then adds (91.19); hence old nonuniverse formers may range over quotient types. It retains each old ${\mathcal{U}}_i$ with its original PER and gives the expanded hierarchy fresh tags ${\mathcal{U}}_i^{\mathsf{q}}$. Thus quotient types inhabit only the fresh extended universes, and old-universe equality is unchanged. Its member judgments carry a superscript $\mathsf{q}$. It is not the frozen artifact closure. The quotient PER is written $R_{A/E}^{(i)}$ because its inhabitance test is indexed. Lemma 91.37 proves that old-level inhabitance is unchanged at larger strata; hence inherited and freshly regenerated quotient triples receive logically equivalent relations.

Full-Timpl bidirectional checking and certificate replay

The three modes, inversion oracles, and priority convention are those of definition 48.16. The following is the complete local rule card used by Chapters 110 and 112; no omitted constructor schema is implicit.

The opening presyntax calculation uses four earlier, syntax-directed rules. They are distinct from the full-Timpl card because their surface terms store the domain and codomain annotations directly.

$\mathrm{\Gamma }⊢{\tau }_0\Leftarrow \mathsf{type}⇝A$$\mathrm{\Gamma },x:A⊢{\tau }_1\Leftarrow \mathsf{type}⇝B$

$\mathrm{\Gamma }⊢\mathsf{Pi}({\tau }_0;x.{\tau }_1)\Leftarrow \mathsf{type}⇝\prod _{x:A}B$

$(x:A)\in \mathrm{\Gamma }$$\mathrm{\Gamma }⊢C\equiv A\mathsf{type}$

$\mathrm{\Gamma }⊢x:C⇝x$

$\mathrm{\Gamma }⊢{\tau }_0\Leftarrow \mathsf{type}⇝A$$\mathrm{\Gamma },x:A⊢{\tau }_1\Leftarrow \mathsf{type}⇝B$$\mathrm{\Gamma },x:A⊢e:B⇝b$$\mathrm{\Gamma }⊢C\equiv \prod _{x:A}B\mathsf{type}$

$\mathrm{\Gamma }⊢\mathsf{lam}({\tau }_0;x.{\tau }_1;x.e):C⇝\lambda (x:A).b$

$\mathrm{\Gamma }⊢{\tau }_0\Leftarrow \mathsf{type}⇝A$$\mathrm{\Gamma },x:A⊢{\tau }_1\Leftarrow \mathsf{type}⇝B$$\mathrm{\Gamma }⊢e_0:\prod _{x:A}B⇝f$$\mathrm{\Gamma }⊢e_1:A⇝a$$\mathrm{\Gamma }⊢C\equiv B[a/x]\mathsf{type}$

$\mathrm{\Gamma }⊢\mathsf{app}({\tau }_0;x.{\tau }_1;e_0;e_1):C⇝fa$

$\mathrm{\Gamma }⊢{\tau }_0\Leftarrow \mathsf{type}⇝A$$\mathrm{\Gamma },x:A⊢{\tau }_1\Leftarrow \mathsf{type}⇝B$

$\mathrm{\Gamma }⊢\prod _{x:{\tau }_0}^{ϵ,\varrho }{\tau }_1\Leftarrow \mathsf{type}⇝\prod _{x:A}^{ϵ,\varrho }B$

$\mathrm{\Gamma }⊢{\tau }_0\Leftarrow \mathsf{type}⇝A$$\mathrm{\Gamma },x:A⊢{\tau }_1\Leftarrow \mathsf{type}⇝B$

$\mathrm{\Gamma }⊢\sum _{x:{\tau }_0}{\tau }_1\Leftarrow \mathsf{type}⇝\sum _{x:A}B$

$\mathrm{\Gamma }⊢\tau \Leftarrow \mathsf{type}⇝A$$\mathrm{\Gamma }⊢e_0\Leftarrow A⇝a$$\mathrm{\Gamma }⊢e_1\Leftarrow A⇝b$

$\mathrm{\Gamma }⊢{\mathsf{Id}}_{\tau }(e_0,e_1)\Leftarrow \mathsf{type}⇝{\mathsf{Id}}_A(a,b)$

$\mathrm{\Gamma }⊢\mathbf{1}\Leftarrow \mathsf{type}⇝\mathbf{1}$

$\mathrm{\Gamma }⊢\mathbb{N}\Leftarrow \mathsf{type}⇝\mathbb{N}$

$\mathrm{\Gamma }⊢\mathbf{2}\Leftarrow \mathsf{type}⇝\mathbf{2}$

$\mathrm{\Gamma }⊢\tau \Leftarrow {\mathcal{U}}_i⇝A$$\mathrm{\Gamma }⊢e\Leftarrow \mathbb{N}⇝n$

$\mathrm{\Gamma }⊢\mathsf{Vec}[i](\tau ,e)\Leftarrow \mathsf{type}⇝\mathsf{Vec}(A,n)$

$\mathrm{\Gamma }⊢{\mathcal{U}}_i\Leftarrow \mathsf{type}⇝{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢e\Rightarrow C⇝a$$\mathrm{unUniv}(\mathrm{\Gamma },C)=i$

$\mathrm{\Gamma }⊢e\Leftarrow \mathsf{type}⇝a$

Rule Ty-El is that bridge: it first synthesizes a universe element and then returns the elaborated code as a type.

Dependent elimination synthesizes its result by substituting the elaborated scrutinee into the motive. Variables, fixed-type constructors, and annotations also synthesize.

$(x:A)\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x\Rightarrow A⇝x$

$\mathrm{\Gamma }⊢e_0\Rightarrow C⇝f$$\mathrm{unPiMeta}(\mathrm{\Gamma },C)=(ϵ,\varrho ,A,x.B)$$\mathrm{\Gamma }⊢e_1\Leftarrow A⇝a$

$\mathrm{\Gamma }⊢e_0{}^{ϵ,\varrho }{e}_1\Rightarrow B[a/x]⇝f{}^{ϵ,\varrho }a$

$\mathrm{\Gamma }⊢e\Rightarrow C⇝p$$\mathrm{unSg}(\mathrm{\Gamma },C)=(A,x.B)$

$\mathrm{\Gamma }⊢{\mathsf{pr}}_1(e)\Rightarrow A⇝{\mathsf{pr}}_1(p)$

$\mathrm{\Gamma }⊢e\Rightarrow C⇝p$$\mathrm{unSg}(\mathrm{\Gamma },C)=(A,x.B)$

$\mathrm{\Gamma }⊢{\mathsf{pr}}_2(e)\Rightarrow B[{\mathsf{pr}}_1(p)/x]⇝{\mathsf{pr}}_2(p)$

$\mathrm{\Gamma }⊢\star \Rightarrow \mathbf{1}⇝\star$

$\mathrm{\Gamma }⊢\mathsf{0}\Rightarrow \mathbb{N}⇝\mathsf{0}$

$\mathrm{\Gamma }⊢e\Leftarrow \mathbb{N}⇝n$

$\mathrm{\Gamma }⊢\mathsf{suc}(e)\Rightarrow \mathbb{N}⇝\mathsf{suc}(n)$

$\mathrm{\Gamma }⊢\mathsf{tt}\Rightarrow \mathbf{2}⇝\mathsf{tt}$

$\mathrm{\Gamma }⊢\mathsf{ff}\Rightarrow \mathbf{2}⇝\mathsf{ff}$

$\mathrm{\Gamma }⊢\tau \Leftarrow \mathsf{type}⇝A$$\mathrm{\Gamma }⊢e\Leftarrow A⇝a$

$\mathrm{\Gamma }⊢(e:\tau )\Rightarrow A⇝a$

$\mathrm{\Gamma }⊢e\Rightarrow D⇝b$$\mathrm{\Gamma }⊢D\iff \mathbf{2}\mathsf{type}$$\mathrm{\Gamma },k:\mathbf{2}⊢\tau \Leftarrow \mathsf{type}⇝C$$\mathrm{\Gamma }⊢e_t\Leftarrow C[\mathsf{tt}/k]⇝c_t$$\mathrm{\Gamma }⊢e_f\Leftarrow C[\mathsf{ff}/k]⇝c_f$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbf{2}}(k.\tau ;e_t,e_f;e)\Rightarrow C[b/k]⇝{\mathsf{ind}}_{\mathbf{2}}(k.C;c_t,c_f;b)$

$\mathrm{\Gamma }⊢e\Rightarrow D⇝m$$\mathrm{\Gamma }⊢D\iff \mathbb{N}\mathsf{type}$$\mathrm{\Gamma },k:\mathbb{N}⊢\tau \Leftarrow \mathsf{type}⇝C$$\mathrm{\Gamma }⊢e_z\Leftarrow C[\mathsf{0}/k]⇝c_z$$\mathrm{\Gamma },n:\mathbb{N},y:C[n/k]⊢e_s\Leftarrow C[\mathsf{suc}(n)/k]⇝c_s$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbb{N}}(k.\tau ;e_z;n.y.e_s;e)\Rightarrow C[m/k]⇝{\mathsf{ind}}_{\mathbb{N}}(k.C;c_z;n.y.c_s;m)$

$\mathrm{\Gamma }⊢q\Rightarrow D⇝q^{\prime }$$\mathrm{unId}(\mathrm{\Gamma },D)=(A,a,b)$$\mathrm{\Gamma },x:A,y:A,p:{\mathsf{Id}}_A(x,y)⊢\tau \Leftarrow \mathsf{type}⇝C$$\mathrm{\Gamma },z:A⊢e\Leftarrow C[z/x,z/y,{\mathsf{refl}}_z/p]⇝c$

$\mathrm{\Gamma }⊢\mathsf{J}(x.y.p.\tau ;z.e;q)\Rightarrow C[a/x,b/y,q^{\prime }/p]⇝{\mathsf{J}}_{A;a;b}(x.y.p.C;z.c;q^{\prime })$

The vector constructors and eliminator expose every parameter needed by the kernel rule. The bracketed lists below are stored certificate fields, not inferred surface arguments. Write ${\mathsf{Nil}}_i[\tau ]$ for the annotated nil form, ${\mathsf{Cons}}_i[\tau ;\overrightarrow{e}]$ for annotated cons, where $\overrightarrow{e}=(e_n,e_a,e_{xs})$, and ${\mathsf{Ind}}_{i,j}$ for annotated vector elimination. Its stored fields, in order, are ${\tau }_A$, $n.v.{\tau }_P$, $e_0$, $n.a.xs.q.e_s$, $e_m$, and $e_{ys}$. Put $P_0:=P[\mathsf{0}/n,{\mathsf{Nil}}_i[A]/v]$ and $P_s:=P[\mathsf{suc}(n)/n,{\mathsf{Cons}}_i[A;(n,a,xs)]/v]$. For the eliminator rule also abbreviate

$\mathrm{\Gamma }⊢\tau \Leftarrow {\mathcal{U}}_i⇝A$

$\mathrm{\Gamma }⊢{\mathsf{Nil}}_i[\tau ]\Rightarrow \mathsf{Vec}(A,\mathsf{0})⇝{\mathsf{Nil}}_i[A]$

$\mathrm{\Gamma }⊢\tau \Leftarrow {\mathcal{U}}_i⇝A$$\mathrm{\Gamma }⊢e_n\Leftarrow \mathbb{N}⇝n$$\mathrm{\Gamma }⊢e_a\Leftarrow A⇝a$$\mathrm{\Gamma }⊢e_{xs}\Leftarrow \mathsf{Vec}(A,n)⇝xs$

$\mathrm{\Gamma }⊢{\mathsf{Cons}}_i[\tau ;\overrightarrow{e}]\Rightarrow \mathsf{Vec}(A,\mathsf{suc}(n))⇝{\mathsf{Cons}}_i[A;(n,a,xs)]$

For Syn-VecInd, abbreviate the complete surface and core nodes by

$\mathrm{\Gamma }⊢{\tau }_A\Leftarrow {\mathcal{U}}_i⇝A$$\mathrm{\Gamma }⊢e_m\Leftarrow \mathbb{N}⇝m$$\mathrm{\Gamma }⊢e_{ys}\Leftarrow \mathsf{Vec}(A,m)⇝ys$$\mathrm{\Gamma },n:\mathbb{N},v:\mathsf{Vec}(A,n)⊢{\tau }_P\Leftarrow {\mathcal{U}}_j⇝P$$\mathrm{\Gamma }⊢e_0\Leftarrow P_0⇝p_0$${\mathrm{\Delta }}_s⊢e_s\Leftarrow P_s⇝p_s$

$\mathrm{\Gamma }⊢E_V\Rightarrow P[m/n,ys/v]⇝a_V$

Introduction forms check against a constructor recovered from the expected type; dedicated introduction and code rules take priority over the fallback that synthesizes a type and compares it with the expected type.

$\mathrm{unPiMeta}(\mathrm{\Gamma },C)=(ϵ,\varrho ,A,x.B)$$\mathrm{\Gamma },x:A⊢e\Leftarrow B⇝b$

$\mathrm{\Gamma }⊢{\lambda }^{ϵ,\varrho }x.e\Leftarrow C⇝{\lambda }^{ϵ,\varrho }(x:A).b$

$\mathrm{unSg}(\mathrm{\Gamma },C)=(A,x.B)$$\mathrm{\Gamma }⊢e_0\Leftarrow A⇝a$$\mathrm{\Gamma }⊢e_1\Leftarrow B[a/x]⇝b$

$\mathrm{\Gamma }⊢(e_0,e_1)\Leftarrow C⇝(a,b)$

$\mathrm{unId}(\mathrm{\Gamma },C)=(A,a,b)$$\mathrm{\Gamma }⊢e\Leftarrow A⇝c$$\mathrm{\Gamma }⊢c\iff a:A$$\mathrm{\Gamma }⊢a\iff b:A$

$\mathrm{\Gamma }⊢\mathsf{refl}(e)\Leftarrow C⇝{\mathsf{refl}}_c$

$\mathrm{\Gamma }⊢e\Rightarrow C^{\prime }⇝a$$\mathrm{\Gamma }⊢C\iff C^{\prime }\mathsf{type}$

$\mathrm{\Gamma }⊢e\Leftarrow C⇝a$

For Russell universes the expected universe supplies the level. These are term-checking rules: they are what permit a type expression to occur as a universe element.

$\mathrm{unUniv}(\mathrm{\Gamma },C)=i$

$\mathrm{\Gamma }⊢\mathbf{1}\Leftarrow C⇝\mathbf{1}$

$\mathrm{unUniv}(\mathrm{\Gamma },C)=i$

$\mathrm{\Gamma }⊢\mathbb{N}\Leftarrow C⇝\mathbb{N}$

$\mathrm{unUniv}(\mathrm{\Gamma },C)=i$

$\mathrm{\Gamma }⊢\mathbf{2}\Leftarrow C⇝\mathbf{2}$

$\mathrm{\Gamma }⊢{\mathcal{U}}_j\Leftarrow C⇝{\mathcal{U}}_j$

$\mathrm{unUniv}(\mathrm{\Gamma },C)=i$$\mathrm{\Gamma }⊢{\tau }_0\Leftarrow {\mathcal{U}}_i⇝A$$\mathrm{\Gamma },x:A⊢{\tau }_1\Leftarrow {\mathcal{U}}_i⇝B$

$\mathrm{\Gamma }⊢\prod _{x:{\tau }_0}^{ϵ,\varrho }{\tau }_1\Leftarrow C⇝\prod _{x:A}^{ϵ,\varrho }B$

$\mathrm{unUniv}(\mathrm{\Gamma },C)=i$$\mathrm{\Gamma }⊢{\tau }_0\Leftarrow {\mathcal{U}}_i⇝A$$\mathrm{\Gamma },x:A⊢{\tau }_1\Leftarrow {\mathcal{U}}_i⇝B$

$\mathrm{\Gamma }⊢\sum _{x:{\tau }_0}{\tau }_1\Leftarrow C⇝\sum _{x:A}B$

$\mathrm{unUniv}(\mathrm{\Gamma },C)=i$$\mathrm{\Gamma }⊢\tau \Leftarrow {\mathcal{U}}_i⇝A$$\mathrm{\Gamma }⊢e_0\Leftarrow A⇝a$$\mathrm{\Gamma }⊢e_1\Leftarrow A⇝b$

$\mathrm{\Gamma }⊢{\mathsf{Id}}_{\tau }(e_0,e_1)\Leftarrow C⇝{\mathsf{Id}}_A(a,b)$

$\mathrm{unUniv}(\mathrm{\Gamma },C)=i+1$$\mathrm{\Gamma }⊢e\Leftarrow {\mathcal{U}}_i⇝A$

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_i(e)\Leftarrow C⇝{\mathsf{Lift}}_{i}A$

$\mathrm{unUniv}(\mathrm{\Gamma },C)=i$$\mathrm{\Gamma }⊢\tau \Leftarrow {\mathcal{U}}_i⇝A$$\mathrm{\Gamma }⊢e\Leftarrow \mathbb{N}⇝n$

$\mathrm{\Gamma }⊢\mathsf{Vec}[i](\tau ,e)\Leftarrow C⇝\mathsf{Vec}(A,n)$

The code rules use the formation and lift rules of definition 29.1 and definition 29.10. Equality is consulted only by the two comparison premises and inside the inversion operations. Everywhere else information flows structurally.

The rule cards are executed in the following total priority order. In type mode inspect the head in the order $${\mathrm{\Pi }}^{ϵ,\varrho },\mathrm{\Sigma },\mathsf{Id},\mathbf{1},\mathbf{2},\mathbb{N},\mathsf{Vec}[i],{\mathcal{U}}_i;\text{otherwise try Ty-El.}$$ In synthesis mode inspect the head in the order In checking mode first try, in order, the recognized heads ${\lambda }^{ϵ,\varrho }$, pair, reflexivity, and the universe-code heads $\mathbf{1},\mathbb{N},\mathbf{2},\mathcal{U},{\mathrm{\Pi }}^{ϵ,\varrho },\mathrm{\Sigma },\mathsf{Id},\mathsf{Lift},\mathsf{Vec}$; only an unrecognized head reaches Chk-Conv. Within a selected clause, premises run top to bottom. A failed premise rejects the query; there is no backtracking to a later clause.

Proof of Proposition 1

Proof. For each mode and head constructor, exactly one clause is eligible. Its premises are evaluated in the fixed order stated by the algorithm; a failed premise returns failure. All outputs are determined by recursive outputs and the deterministic oracles. In particular, Ty-El uses the single output of $\mathrm{unUniv}$, not a choice of universe level.

For termination, order calls lexicographically by the size of the surface subject and the mode order . Every recursive call is on a proper subexpression, except the premise of Ty-El and that of Chk-Conv; those preserve the subject and strictly decrease the mode. Context extension and substitution in an output do not create recursive queries. Hence no call chain is infinite. ◻

The annotations in the source tree can serve as a certificate rather than as trusted elaborator state.

Defined declarations carry a finite map $D$ from declared names to their elaborated types and bodies. The two variable rules and the declaration-list rules are

$(x:A)\in \mathrm{\Gamma }$$x\notin \mathrm{dom}D$

$\mathrm{\Gamma };D⊢x\Rightarrow A⇝x$

$D(x)=(A,a)$

$\mathrm{\Gamma };D⊢x\Rightarrow A⇝a^{\uparrow \mathrm{\Gamma }}$

$\mathrm{\Gamma };D⊢\epsilon \mathsf{ok}$

$\mathrm{\Gamma };D⊢\tau \Leftarrow \mathsf{type}⇝A$$\mathrm{\Gamma };D⊢e\Leftarrow A⇝a$$\mathrm{\Gamma },x:A;D[x\mapsto (A,a)]⊢ds\mathsf{ok}$

$\mathrm{\Gamma };D⊢(\mathsf{def}x:\tau =e);ds\mathsf{ok}$

Here $a^{\uparrow \mathrm{\Gamma }}$ is the ordered weakening of the stored body through declarations following $x$. The accepted initial state is $\cdot ;\mathrm{\varnothing }⊢ds\mathsf{ok}$.

Ranked normal forms and semantic computability

Chapter 49 uses four mutually inductive judgments: neutral terms $\mathrm{\Gamma }⊢u\mathsf{ne}A$, eta-long normal terms $\mathrm{\Gamma }⊢v\mathsf{nf}A$, normal types $\mathrm{\Gamma }⊢A\mathsf{nf}\mathsf{type}$, and normal universe codes $\mathrm{\Gamma }⊢c\mathsf{nf}{\mathcal{U}}_i$. They are generated mutually by the following complete rules.

Neutral terms:

$(x:A)\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x\mathsf{ne}A$

$\mathrm{\Gamma }⊢u\mathsf{ne}\prod _{x:A}^{ϵ,\varrho }B$$\mathrm{\Gamma }⊢v\mathsf{nf}A$

$\mathrm{\Gamma }⊢u{}^{ϵ,\varrho }v\mathsf{ne}B[v/x]$

$\mathrm{\Gamma }⊢u\mathsf{ne}\sum _{x:A}B$

$\mathrm{\Gamma }⊢{\mathsf{pr}}_1(u)\mathsf{ne}A$

$\mathrm{\Gamma }⊢u\mathsf{ne}\sum _{x:A}B$

$\mathrm{\Gamma }⊢{\mathsf{pr}}_2(u)\mathsf{ne}B[{\mathsf{pr}}_1(u)/x]$

$\mathrm{\Gamma },x:\mathbf{2}⊢C\mathsf{nf}\mathsf{type}$$\mathrm{\Gamma }⊢v_t\mathsf{nf}C[\mathsf{tt}/x]$$\mathrm{\Gamma }⊢v_f\mathsf{nf}C[\mathsf{ff}/x]$$\mathrm{\Gamma }⊢u\mathsf{ne}\mathbf{2}$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbf{2}}(x.C;v_t,v_f,u)\mathsf{ne}C[u/x]$

$\mathrm{\Gamma },x:\mathbb{N}⊢C\mathsf{nf}\mathsf{type}$$\mathrm{\Gamma }⊢v_0\mathsf{nf}C[\mathsf{0}/x]$$\mathrm{\Gamma }⊢v_s\mathsf{nf}{\mathsf{Step}}_{\mathbb{N}}(C)$$\mathrm{\Gamma }⊢u\mathsf{ne}\mathbb{N}$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbb{N}}(x.C;v_0,v_s,u)\mathsf{ne}C[u/x]$

$\mathrm{\Gamma }⊢A\mathsf{nf}\mathsf{type}$$\mathrm{\Gamma }⊢v_a\mathsf{nf}A$$\mathrm{\Gamma }⊢v_b\mathsf{nf}A$$\mathrm{\Gamma },x:A,y:A,p:{\mathsf{Id}}_A(x,y)⊢C\mathsf{nf}\mathsf{type}$$\mathrm{\Gamma },z:A⊢v\mathsf{nf}C[z/x,z/y,{\mathsf{refl}}_z/p]$$\mathrm{\Gamma }⊢u\mathsf{ne}{\mathsf{Id}}_A(v_a,v_b)$

$\mathrm{\Gamma }⊢{\mathsf{J}}_{A;v_a;v_b}(x.y.p.C;z.v;u)\mathsf{ne}C[v_a/x,v_b/y,u/p]$

$\mathrm{\Gamma }⊢c\mathsf{nf}{\mathcal{U}}_{\ell }$$\mathrm{\Gamma },n:\mathbb{N},v:\mathsf{Vec}(c,n)⊢P\mathsf{nf}\mathsf{type}$$\mathrm{\Gamma }⊢v_0\mathsf{nf}{P}_0$$\mathrm{\Gamma }⊢v_s\mathsf{nf}{P}_s$$\mathrm{\Gamma }⊢w\mathsf{nf}\mathbb{N}$$\mathrm{\Gamma }⊢u\mathsf{ne}\mathsf{Vec}(c,w)$

$\mathrm{\Gamma }⊢\mathsf{vind}(n.v.P;v_0;n.a.xs.q.v_s;w,u)\mathsf{ne}P[w/n,u/v]$

Here $P_0$ and $P_s$ are the base and successor method types of Vec-elim, including its full $n,a,xs,q$ successor context.

Normal terms:

$\mathrm{\Gamma }⊢A\mathsf{nf}\mathsf{type}$$\mathrm{\Gamma },x:A⊢v\mathsf{nf}B$

$\mathrm{\Gamma }⊢{\lambda }^{ϵ,\varrho }(x:A).v\mathsf{nf}\prod _{x:A}^{ϵ,\varrho }B$

$\mathrm{\Gamma }⊢v\mathsf{nf}A$$\mathrm{\Gamma }⊢w\mathsf{nf}B[v/x]$

$\mathrm{\Gamma }⊢(v,w)\mathsf{nf}\sum _{x:A}B$

$\mathrm{\Gamma }⊢\star \mathsf{nf}\mathbf{1}$

$\mathrm{\Gamma }⊢\mathsf{tt}\mathsf{nf}\mathbf{2}$

$\mathrm{\Gamma }⊢\mathsf{ff}\mathsf{nf}\mathbf{2}$

$\mathrm{\Gamma }⊢\mathsf{0}\mathsf{nf}\mathbb{N}$

$\mathrm{\Gamma }⊢v\mathsf{nf}\mathbb{N}$

$\mathrm{\Gamma }⊢\mathsf{suc}(v)\mathsf{nf}\mathbb{N}$

$\mathrm{\Gamma }⊢v\mathsf{nf}A$$\mathrm{\Gamma }⊢a\equiv v:A$$\mathrm{\Gamma }⊢b\equiv v:A$

$\mathrm{\Gamma }⊢{\mathsf{refl}}_v\mathsf{nf}{\mathsf{Id}}_A(a,b)$

$\mathrm{\Gamma }⊢n\equiv \mathsf{0}:\mathbb{N}$

$\mathrm{\Gamma }⊢\mathsf{vnil}\mathsf{nf}\mathsf{Vec}(c,n)$

$\mathrm{\Gamma }⊢v_n\mathsf{nf}\mathbb{N}$$\mathrm{\Gamma }⊢v_a\mathsf{nf}c$$\mathrm{\Gamma }⊢v_{xs}\mathsf{nf}\mathsf{Vec}(c,v_n)$$\mathrm{\Gamma }⊢n\equiv \mathsf{suc}(v_n):\mathbb{N}$

$\mathrm{\Gamma }⊢\mathsf{vcons}(v_n,v_a,v_{xs})\mathsf{nf}\mathsf{Vec}(c,n)$

$\mathrm{\Gamma }⊢u\mathsf{ne}A$$A\mathsf{positive}$

$\mathrm{\Gamma }⊢u\mathsf{nf}A$

Normal universe codes:

$\mathrm{\Gamma }⊢K\mathsf{nf}{\mathcal{U}}_{\ell }$

$\mathrm{\Gamma }⊢{\mathcal{U}}_k\mathsf{nf}{\mathcal{U}}_{\ell }$

$\mathrm{\Gamma }⊢c\mathsf{nf}{\mathcal{U}}_{\ell }$$\mathrm{\Gamma },x:c⊢d\mathsf{nf}{\mathcal{U}}_{\ell }$

$\mathrm{\Gamma }⊢\prod _{x:c}^{ϵ,\varrho }d\mathsf{nf}{\mathcal{U}}_{\ell }$

$\mathrm{\Gamma }⊢c\mathsf{nf}{\mathcal{U}}_{\ell }$$\mathrm{\Gamma },x:c⊢d\mathsf{nf}{\mathcal{U}}_{\ell }$

$\mathrm{\Gamma }⊢\sum _{x:c}d\mathsf{nf}{\mathcal{U}}_{\ell }$

$\mathrm{\Gamma }⊢c\mathsf{nf}{\mathcal{U}}_{\ell }$$\mathrm{\Gamma }⊢v\mathsf{nf}c$$\mathrm{\Gamma }⊢w\mathsf{nf}c$

$\mathrm{\Gamma }⊢{\mathsf{Id}}_c(v,w)\mathsf{nf}{\mathcal{U}}_{\ell }$

$\mathrm{\Gamma }⊢c\mathsf{nf}{\mathcal{U}}_{\ell }$$\mathrm{\Gamma }⊢v\mathsf{nf}\mathbb{N}$

$\mathrm{\Gamma }⊢\mathsf{Vec}(c,v)\mathsf{nf}{\mathcal{U}}_{\ell }$

$\mathrm{\Gamma }⊢c\mathsf{nf}{\mathcal{U}}_{\ell }$$c\mathsf{stuck}$

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_{\ell }(c)\mathsf{nf}{\mathcal{U}}_{\ell +1}$

where $K\in \{\mathbf{1},\mathbf{2},\mathbb{N}\}$.

Normal types:

$\mathrm{\Gamma }⊢{\mathcal{U}}_{\ell }\mathsf{nf}\mathsf{type}$

$\mathrm{\Gamma }⊢A\mathsf{nf}\mathsf{type}$$\mathrm{\Gamma },x:A⊢B\mathsf{nf}\mathsf{type}$

$\mathrm{\Gamma }⊢\prod _{x:A}^{ϵ,\varrho }B\mathsf{nf}\mathsf{type}$

$\mathrm{\Gamma }⊢A\mathsf{nf}\mathsf{type}$$\mathrm{\Gamma },x:A⊢B\mathsf{nf}\mathsf{type}$

$\mathrm{\Gamma }⊢\sum _{x:A}B\mathsf{nf}\mathsf{type}$

$\mathrm{\Gamma }⊢K\mathsf{nf}\mathsf{type}$

$\mathrm{\Gamma }⊢A\mathsf{nf}\mathsf{type}$$\mathrm{\Gamma }⊢v\mathsf{nf}A$$\mathrm{\Gamma }⊢w\mathsf{nf}A$

$\mathrm{\Gamma }⊢{\mathsf{Id}}_A(v,w)\mathsf{nf}\mathsf{type}$

$\mathrm{\Gamma }⊢c\mathsf{nf}{\mathcal{U}}_{\ell }$$\mathrm{\Gamma }⊢v\mathsf{nf}\mathbb{N}$

$\mathrm{\Gamma }⊢\mathsf{Vec}(c,v)\mathsf{nf}\mathsf{type}$

$\mathrm{\Gamma }⊢u\mathsf{ne}{\mathcal{U}}_{\ell }$

$\mathrm{\Gamma }⊢u\mathsf{nf}\mathsf{type}$

Here positive means Boolean, natural, identity, vector, universe, or neutral type. A code is stuck exactly when it is neutral, vector-headed, or lift-headed. Consequently a lift may head a normal code but never a normal type; the element field of a vector is the one code-valued field in a normal type.

Semantic code equality $\alpha :\mathcal{A}{\approx }_i\mathcal{B}$ and semantic type equality $\delta :\mathcal{A}\approx \mathcal{B}$ are ranked proof trees. Write $D_{\mathrm{\Psi }}$ for the values admissible at the displayed support telescope. Membership is the support-indexed judgment $$\eta :(d,e)\in {\mathsf{Elt}}_{\mathrm{\Psi }}(\alpha ),{\mathsf{Elt}}_{\mathrm{\Psi }}(\alpha )\subseteq D_{\mathrm{\Psi }}\times D_{\mathrm{\Psi }}.$$ Its formation includes $d,e\in D_{\mathrm{\Psi }}$ and a $\mathrm{\Psi }$-admissibility derivation for $\eta$; there is no unindexed membership judgment on raw $D$. In particular, Unit has ${\mathsf{Elt}}_{\mathrm{\Psi }}({\mathsf{u}}_i)=D_{\mathrm{\Psi }}\times D_{\mathrm{\Psi }}$, not $D\times D$. The generators, in formation order, are Unit, Boolean, natural, smaller universe, product, sum, identity, vector, lift, and neutral code. A ranked derivation is formed at a finite support telescope $\mathrm{\Psi }$ whose levels are the initial segment $0,\dots ,|\mathrm{\Psi }|-1$ and whose declarations classify every neutral occurrence in each endpoint and membership witness. There is no sparse-support compression step. A typed semantic substitution $\sigma :\mathrm{\Psi }\Rightarrow \mathrm{\Phi }$ assigns a value in $D_{\mathrm{\Phi }}$ at each transported declaration, with membership evidence at $\mathrm{\Phi }$. An iterated typed target weakening additionally has a structural action on neutral syntax: it fixes old levels and transports stored semantic fields, so its image is still neutral. This action is distinct from arbitrary semantic substitution, which may expose a redex. Arbitrary source instantiation, for $e\in D_{\mathrm{\Phi }}$ with its transported membership evidence, is $(\sigma ,e):\mathrm{\Psi }.\mathcal{A}\Rightarrow \mathrm{\Phi }$. Put $\mathcal{B}:={\sigma }_{\ast }\mathcal{A}$. Target weakening and the canonical fresh lift have the exact types $$\mathsf{wk}\circ \sigma :\mathrm{\Psi }\Rightarrow \mathrm{\Phi }.\mathcal{B},{\sigma }^{\uparrow }:\mathrm{\Psi }.\mathcal{A}\Rightarrow \mathrm{\Phi }.\mathcal{B},$$ with ${\sigma }^{\uparrow }=(\mathsf{wk}\circ \sigma ,{\uparrow }_{(\mathsf{wk}\circ \sigma {)}_{\ast }\mathcal{A}}({\mathsf{x}}_{|\mathrm{\Phi }|}))$. The classifier $(\mathsf{wk}\circ \sigma {)}_{\ast }\mathcal{A}$ lives over $\mathrm{\Phi }.\mathcal{B}$ and classifies only the last component. The paired lift likewise targets $\mathbf{\Phi }.({\mathit{\sigma }}_{\ast }\alpha )$; its fresh pair is classified there by $(\mathsf{wk}\circ \mathit{\sigma }{)}_{\ast }\alpha$. Composition satisfies $\tau \circ (\sigma ,e)=(\tau \circ \sigma ,{\tau }_{\ast }e)$. A dependent-family premise is natural under paired typed substitutions carrying evidence that their two assignments preserve corresponding classifiers. For $\mathit{\sigma }:\mathbf{\Psi }\Rightarrow \mathbf{\Phi }$, products quantify over every $\zeta :(d,e)\in {\mathsf{Elt}}_{\mathrm{\Phi }}({\mathit{\sigma }}_{\ast }\alpha )$; formation of $\zeta$ supplies $d,e\in D_{\mathrm{\Phi }}$. Sums store support-indexed first-component evidence and the corresponding fiber evidence at the same support; identity stores a clique containing both endpoints and both reflexivity witnesses; vectors recurse on ranked natural length evidence. For a neutral-code generator with endpoints $\mathcal{N}={\mathsf{up}}_{{\hat{\mathcal{U}}}_i}(k)$ and ${\mathcal{N}}^{\prime }={\mathsf{up}}_{{\hat{\mathcal{U}}}_i}(k^{\prime })$, its elements are exactly ${\mathsf{up}}_{\mathcal{N}}(q)$ and ${\mathsf{up}}_{{\mathcal{N}}^{\prime }}(q^{\prime })$ for world-indexed related $q,q^{\prime }$ at the displayed support; there are no unbound carrier annotations. Semantic types use the same generators, except that a vector records a code premise and its semantic embedding, a universe at $i$ has code equality ${\approx }_i$ as its elements, and the code-lift generator is replaced by left and right peeling. A comparison involving code levels $i_1,\dots ,i_r$ is ordered first by the multiset $[i_1(\overrightarrow{0}),\dots ,i_r(\overrightarrow{0})]$ and then by the Hessenberg sum of all construction and membership ranks. This measure strictly decreases under universe descent, transitivity, cross-level vector transport, and peeling.

The syntax–value relation is first defined without erasing that evidence: $$\begin{array}{c}\mathrm{\Delta }{⊩}_{\delta ,\eta }a\sim d,\delta :\mathcal{A}\approx \mathcal{A}@{\mathrm{\Psi }}_{\mathrm{\Delta }},\eta :(d,d)\in \mathsf{Elt}(\delta ),\\ \mathrm{\Delta }⊢a:{\mathsf{Q}}_{|\mathrm{\Delta }|}(\mathcal{A}),\delta ,\eta ,d\text{ are }{\mathrm{\Psi }}_{\mathrm{\Delta }}\text{-admissible},\end{array}$$ where ${\mathrm{\Psi }}_{\mathrm{\Delta }}$ is the semantic classifier telescope of $\mathrm{\Delta }$. It is constructed by nested recursion. The outer order is the multiset of active code heights followed by generator rank; at one fixed generator the inner order is membership rank. Thus a product may call the already constructed relation at its strict domain or family generator with an argument witness of arbitrary rank. It does not compare that witness with the enclosing function witness. Unit adds nothing; Boolean and natural evidence select constructor or neutral equations; natural successor recurses on predecessor membership evidence. A product premise $\alpha ,\beta$ requires, for every syntactic world embedding $\omega :\mathrm{\Delta }\hookrightarrow {\mathrm{\Delta }}^{\prime }$, its induced typed classifier weakening ${\omega }_{\mathrm{\Psi }}:{\mathrm{\Psi }}_{\mathrm{\Delta }}\Rightarrow {\mathrm{\Psi }}_{{\mathrm{\Delta }}^{\prime }}$, and every indexed argument witness $\zeta$, the application witness at the target-world family premise ${\beta }_{{\omega }_{\mathrm{\Psi }},\zeta }$ for ${\omega }_{\ast }a{}^{ϵ,\varrho }b$. Quotations, reification, reflection, neutral readback, closures, ranked evidence, and stored judgments are transported by the corresponding ${\omega }_{\ast }$ or $({\omega }_{\mathrm{\Psi }}{)}_{\ast }$ action; in particular, for $n=|\mathrm{\Delta }|$ and $n^{\prime }=|{\mathrm{\Delta }}^{\prime }|$, $({\omega }_{\mathrm{\Psi }}{)}_{\ast }{\mathsf{Q}}_n(\mathcal{A}){=}_{\alpha }{\mathsf{Q}}_{n^{\prime }}(({\omega }_{\mathrm{\Psi }}{)}_{\ast }\mathcal{A})$. The canonical embedding fixes old levels, while its binder lift sends the source fresh level $n$ to the target fresh level $n^{\prime }$; dependent premise families are reindexed by precomposition and still range over every target-world argument, not merely arguments in the image of ${\omega }_{\mathrm{\Psi }}$. Their naturality equation is ${\tau }_{\ast }{\beta }_{\sigma ,\zeta }={\beta }_{\tau \circ \sigma ,{\tau }_{\ast }\zeta }$. A fresh readback binder uses ${\sigma }^{\uparrow }$; an arbitrary future related argument uses $(\mathsf{wk}\circ \sigma ,e)$ and never the canonical lift. A sum recurses at its two stored component premises. Identity reflexivity recurses at the carrier premise and stores both endpoint equations. Vector cons recurses at the semantic embedding of its code premise and at the shorter vector generator. Universe evidence is a code self-derivation and stores both code and type quotation equations; neutral type evidence stores its neutral readback equation. Paired lift peels recurse at their lower-ranked core. Fresh variables and every stuck neutral carry the world-indexed premise $k{\approx }_{\mathrm{\Psi }}^{\mathrm{ne}}k$ required by reflection, equivalently membership in the readback-defined field $K_{\mathrm{\Psi }}$. The neutral relation is a partial equivalence relation on all $\mathrm{\Psi }$-admissible neutrals and an equivalence relation only after restriction to $K_{\mathrm{\Psi }}$. Its field condition quantifies over typed future weakenings from $\mathrm{\Psi }$ and reads back only at the exact target length. Quotation and reification at support $\mathrm{\Psi }$ use depth $|\mathrm{\Psi }|$; larger depths arise only after an explicit typed world extension. Thus every recursive call descends in the displayed construction order. Same-endpoint, cross-level, bridge, and peel maps state evidence independence as exact indexed equivalences before the shorter notation $\mathrm{\Delta }⊩a\sim d:\mathcal{A}$ erases $\delta$ and $\eta$. Quotation is proved simultaneously under realizing substitutions. In the product case, an arbitrary future argument extends the raw and semantic substitutions together; beta reduction exposes the quoted body, and the strict family induction hypothesis proves its indexed relation. In the sum case, the first quotation selects the transported fiber before the second is converted and quoted.

The fundamental lemma uses two independent quantifiers. Its semantic half fixes an arbitrary support telescope $\mathrm{\Psi }$ and ranked environment witnesses $\rho {\approx }_{\mathrm{\Psi }}{\rho }^{\prime }:\mathrm{\Gamma }$. Semantic extension by $\zeta :(d,e)\in {\mathsf{Elt}}_{\mathrm{\Psi }}(\alpha )$ is well formed because membership itself supplies $d,e\in D_{\mathrm{\Psi }}$; “arbitrary” therefore means arbitrary among values admissible at that displayed support. Its syntactic half separately fixes a context $\mathrm{\Delta }$ and a valid pair supported by ${\mathrm{\Psi }}_{\mathrm{\Delta }}$. No semantic derivation is assigned the world $|\mathrm{\Delta }|$ merely because the syntactic half mentions $\mathrm{\Delta }$.

Timpl surface elaboration

The state-passing generation judgments are Output contexts extend inputs, and premises thread them from left to right. The atomic, checked-hole, direction-changing, and lambda rules are

$x:A\in \mathrm{\Gamma }$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢x\Rightarrow x:A⊣\mathcal{L};\mathcal{M};\varnothing ;\varnothing$

$c[\overrightarrow{\ell }]:A\text{ is a fully level-instantiated signature atom}$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢c[\overrightarrow{\ell }]\Rightarrow c[\overrightarrow{\ell }]:A⊣\mathcal{L};\mathcal{M};\varnothing ;\varnothing$

$?\alpha \text{ fresh}{\mathcal{M}}^{\prime }=\mathcal{M},?\alpha :[\mathrm{\Gamma }⊢A]$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢\mathrm{\_}\Leftarrow A⇝?\alpha [{\mathrm{id}}_{\mathrm{\Gamma }}]⊣\mathcal{L};{\mathcal{M}}^{\prime };\varnothing ;\varnothing$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢e\Rightarrow a:B⊣{\mathcal{L}}^{\prime };{\mathcal{M}}^{\prime };\mathcal{C};\mathcal{U}$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢e\Leftarrow A⇝a⊣{\mathcal{L}}^{\prime };{\mathcal{M}}^{\prime };(\mathcal{C},\mathrm{\Gamma }⊢A\doteq B\mathsf{type});\mathcal{U}$

$\mathsf{whnf}(A)=\prod _{x:B}^{ϵ,\varrho }C$$\mathcal{L};\mathcal{M};\mathrm{\Gamma },x:B⊢e\Leftarrow C⇝b⊣{\mathcal{L}}^{\prime };{\mathcal{M}}^{\prime };\mathcal{C};\mathcal{U}$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢{\lambda }^{ϵ,\varrho }x.e\Leftarrow A⇝{\lambda }^{ϵ,\varrho }(x:B).b⊣{\mathcal{L}}^{\prime };{\mathcal{M}}^{\prime };\mathcal{C};\mathcal{U}$

In E-Chk-Lam, the surface abstraction and exposed product must agree in both explicitness and relevance. A mismatch in either bit is rejected before the body is checked. Universe membership is generated by

$p,q\text{ well-formed level expressions}$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢{\mathcal{U}}_p\Leftarrow {\mathcal{U}}_q⇝{\mathcal{U}}_p⊣\mathcal{L};\mathcal{M};\varnothing ;(p+1\le q)$

The remaining generation clauses and the complete policy-aligned clauses are displayed next. Together with the six clauses above, this is the complete finite rule inventory; the rule families after the display specify solving and certificate rechecking.

$?u\text{ fresh}?{\alpha }_A,?\alpha \text{ fresh}$${\mathcal{L}}^{\prime }=\mathcal{L},?u$${\mathcal{M}}^{\prime }=\mathcal{M},?{\alpha }_A:[\mathrm{\Gamma }⊢{\mathcal{U}}_{?u}],?\alpha :[\mathrm{\Gamma }⊢?{\alpha }_A[{\mathrm{id}}_{\mathrm{\Gamma }}]]$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢\mathrm{\_}\Rightarrow ?\alpha [{\mathrm{id}}_{\mathrm{\Gamma }}]:?{\alpha }_A[{\mathrm{id}}_{\mathrm{\Gamma }}]⊣{\mathcal{L}}^{\prime };{\mathcal{M}}^{\prime };\varnothing ;\varnothing$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢A\Leftarrow \mathsf{type}⇝A^{\prime }⊣{\mathcal{L}}_1;{\mathcal{M}}_1;{\mathcal{C}}_1;{\mathcal{U}}_1$${\mathcal{L}}_1;{\mathcal{M}}_1;\mathrm{\Gamma }⊢e\Leftarrow A^{\prime }⇝a⊣{\mathcal{L}}_2;{\mathcal{M}}_2;{\mathcal{C}}_2;{\mathcal{U}}_2$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢(e:A)\Rightarrow a:A^{\prime }⊣{\mathcal{L}}_2;{\mathcal{M}}_2;({\mathcal{C}}_1,{\mathcal{C}}_2);({\mathcal{U}}_1,{\mathcal{U}}_2)$

$?u\text{ fresh}?{\alpha }_A\text{ fresh}$${\mathcal{L}}^{\prime }=\mathcal{L},?u{\mathcal{M}}^{\prime }=\mathcal{M},?{\alpha }_A:[\mathrm{\Gamma }⊢{\mathcal{U}}_{?u}]$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢\mathrm{\_}\Leftarrow \mathsf{type}⇝?{\alpha }_A[{\mathrm{id}}_{\mathrm{\Gamma }}]⊣{\mathcal{L}}^{\prime };{\mathcal{M}}^{\prime };\varnothing ;\varnothing$

Type formation is a separate inductive judgment, not an implicit appeal to a maximum universe. In E-Ty-Vec, ${\mathsf{level}}_{\mathcal{L}}(\hat{\ell })=(\ell ,{\mathcal{L}}_0)$ means $\ell$ is the written well-formed level and ${\mathcal{L}}_0=\mathcal{L}$, or $\ell =?u$ is fresh and ${\mathcal{L}}_0=\mathcal{L},?u$.

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢e\Rightarrow a:T⊣{\mathcal{L}}^{\prime };{\mathcal{M}}^{\prime };\mathcal{C};\mathcal{U}$$\mathsf{whnf}(T)={\mathcal{U}}_u$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢e\Leftarrow \mathsf{type}⇝a⊣{\mathcal{L}}^{\prime };{\mathcal{M}}^{\prime };\mathcal{C};\mathcal{U}$

$p\text{ a well-formed level expression}$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢{\mathcal{U}}_p\Leftarrow \mathsf{type}⇝{\mathcal{U}}_p⊣\mathcal{L};\mathcal{M};\varnothing ;\varnothing$

$D\in \{\mathbf{1},\mathbf{2},\mathbb{N}\}$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢D\Leftarrow \mathsf{type}⇝D⊣\mathcal{L};\mathcal{M};\varnothing ;\varnothing$

${\mathrm{\Xi }}_0⊢A\Leftarrow \mathsf{type}⇝A^{\prime }⊣{\mathrm{\Omega }}_1$${\mathrm{\Xi }}_1⊢e_0\Leftarrow A^{\prime }⇝a_0⊣{\mathrm{\Omega }}_2$${\mathrm{\Xi }}_2⊢e_1\Leftarrow A^{\prime }⇝a_1⊣{\mathrm{\Omega }}_3$

${\mathrm{\Xi }}_0⊢{\mathsf{Id}}_A(e_0,e_1)\Leftarrow \mathsf{type}⇝{\mathsf{Id}}_{A^{\prime }}(a_0,a_1)⊣{\mathrm{\Omega }}_1\diamond {\mathrm{\Omega }}_2\diamond {\mathrm{\Omega }}_3$

${\mathsf{level}}_{\mathcal{L}}(\hat{\ell })=(\ell ,{\mathcal{L}}_0)$${\mathrm{\Xi }}_{\ell }:={\mathcal{L}}_0;\mathcal{M};\mathrm{\Gamma }$${\mathrm{\Xi }}_{\ell }⊢A\Leftarrow \mathsf{type}⇝A^{\prime }⊣{\mathrm{\Omega }}_1$${\mathrm{\Xi }}_1⊢n\Leftarrow \mathbb{N}⇝n^{\prime }⊣{\mathrm{\Omega }}_2$

${\mathrm{\Xi }}_0⊢\mathsf{Vec}[\hat{\ell }](A,n)\Leftarrow \mathsf{type}⇝\mathsf{Vec}(A^{\prime },n^{\prime })⊣({\mathrm{\Omega }}_1\diamond {\mathrm{\Omega }}_2)\oplus \mathrm{\Gamma }⊢A^{\prime }\dot{\in }{\mathcal{U}}_{\ell }$

Thus the legal input $\mathsf{Vec}[0]((x:\mathbb{N})\to \mathbb{N},\mathsf{0})$ first elaborates its product element type by E-Ty-Pi; the resulting guard is then discharged by U-Pi. No term-synthesis rule for a product is required.

The binding type formers thread the domain output into the opened codomain.

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢A\Leftarrow \mathsf{type}⇝A^{\prime }⊣{\mathcal{L}}_1;{\mathcal{M}}_1;{\mathcal{C}}_1;{\mathcal{U}}_1$${\mathcal{L}}_1;{\mathcal{M}}_1;\mathrm{\Gamma },x:A^{\prime }⊢B\Leftarrow \mathsf{type}⇝B^{\prime }⊣{\mathcal{L}}_2;{\mathcal{M}}_2;{\mathcal{C}}_2;{\mathcal{U}}_2$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢\prod _{x:A}^{ϵ,\varrho }B\Leftarrow \mathsf{type}⇝\prod _{x:A^{\prime }}^{ϵ,\varrho }{B}^{\prime }⊣{\mathcal{L}}_2;{\mathcal{M}}_2;({\mathcal{C}}_1,{\mathcal{C}}_2);({\mathcal{U}}_1,{\mathcal{U}}_2)$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢A\Leftarrow \mathsf{type}⇝A^{\prime }⊣{\mathcal{L}}_1;{\mathcal{M}}_1;{\mathcal{C}}_1;{\mathcal{U}}_1$${\mathcal{L}}_1;{\mathcal{M}}_1;\mathrm{\Gamma },x:A^{\prime }⊢B\Leftarrow \mathsf{type}⇝B^{\prime }⊣{\mathcal{L}}_2;{\mathcal{M}}_2;{\mathcal{C}}_2;{\mathcal{U}}_2$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢\sum _{x:A}B\Leftarrow \mathsf{type}⇝\sum _{x:A^{\prime }}{B}^{\prime }⊣{\mathcal{L}}_2;{\mathcal{M}}_2;({\mathcal{C}}_1,{\mathcal{C}}_2);({\mathcal{U}}_1,{\mathcal{U}}_2)$

Type-mode rule selection is deterministic. Inspect the outer constructor in this priority order: hole, universe literal, nullary base, identity, vector, product, and Sigma. Rule E-Ty-El is the fallback only for an atom outside those seven syntactic classes whose synthesis exposes a universe. It is therefore never tried after a recognized type-former rule has failed, and no surface type expression selects two type-mode clauses.

Pairs and projections have the following exact clauses. The weak-head premises are tests; failure gives no derivation.

$\mathsf{whnf}(A)=\sum _{x:B}C$$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢e_0\Leftarrow B⇝a_0⊣{\mathcal{L}}_1;{\mathcal{M}}_1;{\mathcal{C}}_1;{\mathcal{U}}_1$${\mathcal{L}}_1;{\mathcal{M}}_1;\mathrm{\Gamma }⊢e_1\Leftarrow C[a_0/x]⇝a_1⊣{\mathcal{L}}_2;{\mathcal{M}}_2;{\mathcal{C}}_2;{\mathcal{U}}_2$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢(e_0,e_1)\Leftarrow A⇝(a_0,a_1)⊣{\mathcal{L}}_2;{\mathcal{M}}_2;({\mathcal{C}}_1,{\mathcal{C}}_2);({\mathcal{U}}_1,{\mathcal{U}}_2)$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢e\Rightarrow a:A⊣{\mathcal{L}}^{\prime };{\mathcal{M}}^{\prime };\mathcal{C};\mathcal{U}$$\mathsf{whnf}(A)=\sum _{x:B}C$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢{\mathsf{pr}}_1(e)\Rightarrow {\mathsf{pr}}_1(a):B⊣{\mathcal{L}}^{\prime };{\mathcal{M}}^{\prime };\mathcal{C};\mathcal{U}$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢e\Rightarrow a:A⊣{\mathcal{L}}^{\prime };{\mathcal{M}}^{\prime };\mathcal{C};\mathcal{U}$$\mathsf{whnf}(A)=\sum _{x:B}C$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢{\mathsf{pr}}_2(e)\Rightarrow {\mathsf{pr}}_2(a):C[{\mathsf{pr}}_1(a)/x]⊣{\mathcal{L}}^{\prime };{\mathcal{M}}^{\prime };\mathcal{C};\mathcal{U}$

Ordinary application is the least relation generated by the next four rules. Rule priority is part of the definition: insertion precedes the explicit case, a written implicit argument precedes insertion, and E-Spine-Done applies only when the written spine is empty and the exposed head is not an implicit product.

${\mathrm{\Xi }}_0⊢e\Rightarrow a:A⊣{\mathrm{\Omega }}_1$${\mathrm{\Xi }}_1⊢(a:A)@\overrightarrow{q}⟹b:B⊣{\mathrm{\Omega }}_2$

${\mathrm{\Xi }}_0⊢e\overrightarrow{q}\Rightarrow b:B⊣{\mathrm{\Omega }}_1\diamond {\mathrm{\Omega }}_2$

$\overrightarrow{q}=\varnothing \mathsf{whnf}(A)\ne \prod _{x:B}^{\mathsf{imp},\varrho }C$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }⊢(a:A)@\varnothing ⟹a:A⊣\mathcal{L};\mathcal{M};\varnothing ;\varnothing$

$\mathsf{whnf}(A)=\prod _{x:B}^{\mathsf{imp},\varrho }C$$\overrightarrow{q}=\varnothing \text{ or its first marker is }\mathsf{exp}$$?\alpha \text{ fresh}{\mathcal{M}}_1=\mathcal{M},?\alpha :[\mathrm{\Gamma }⊢B]$$m_{\alpha }:=?\alpha [{\mathrm{id}}_{\mathrm{\Gamma }}]$${\mathrm{\Xi }}_1⊢(a{}^{\mathsf{imp},\varrho }{m}_{\alpha }:C[m_{\alpha }/x])@\overrightarrow{q}⟹b:D⊣{\mathrm{\Omega }}_2$

${\mathrm{\Xi }}_0⊢(a:A)@\overrightarrow{q}⟹b:D⊣{\mathrm{\Omega }}_2$

$\mathsf{whnf}(A)=\prod _{x:B}^{ϵ,\varrho }C$${\mathrm{\Xi }}_0⊢e\Leftarrow B⇝d⊣{\mathrm{\Omega }}_1$${\mathrm{\Xi }}_1⊢(a{}^{ϵ,\varrho }d:C[d/x])@\overrightarrow{q}⟹b:D⊣{\mathrm{\Omega }}_2$

${\mathrm{\Xi }}_0⊢(a:A)@(e^{ϵ},\overrightarrow{q})⟹b:D⊣{\mathrm{\Omega }}_1\diamond {\mathrm{\Omega }}_2$

A flexible or rigid nonproduct head and an explicitness mismatch have no rule. Consequently this relation inserts one unique consecutive block of implicit arguments and never guesses a relevance bit.

Finally let a signature entry have level parameters $\overrightarrow{u}$, result $R$, and dependency-ordered argument telescope $((x_i:B_i{)}^{{ϵ}_i,{\varrho }_i,{\omega }_i}{)}_{i=1}^n$. Written levels are copied; omitted levels are replaced from left to right by fresh level metavariables. This deterministic operation is written ${\mathsf{levels}}_h(\overrightarrow{\hat{\ell }};\mathcal{L})=(\overrightarrow{\ell };{\mathcal{L}}_0)$. The signature-head and telescope rules are:

${\mathsf{levels}}_h(\overrightarrow{\hat{\ell }};\mathcal{L})=(\overrightarrow{\ell };{\mathcal{L}}_0)$${\mathrm{\Xi }}_{\ell }:={\mathcal{L}}_0;\mathcal{M};\mathrm{\Gamma }$${\mathrm{\Xi }}_{\ell }{⊢}_h(h[\overrightarrow{\ell }];{\mathrm{\Delta }}_h[\overrightarrow{\ell }/\overrightarrow{u}];R[\overrightarrow{\ell }/\overrightarrow{u}])@\overrightarrow{q}⟹b:B⊣{\mathrm{\Omega }}_1$

${\mathrm{\Xi }}_0⊢h[\overrightarrow{\hat{\ell }}]⟨\overrightarrow{q}⟩\Rightarrow b:B⊣{\mathrm{\Omega }}_1$

${\mathrm{\Delta }}_h=\varnothing \overrightarrow{q}=\varnothing$

$\mathcal{L};\mathcal{M};\mathrm{\Gamma }{⊢}_h(a;\varnothing ;R)@\varnothing ⟹a:R⊣\mathcal{L};\mathcal{M};\varnothing ;\varnothing$

${\mathrm{\Delta }}_h=(x:B{)}^{\mathsf{imp},\varrho ,\mathsf{infer}},\mathrm{\Delta }$$\overrightarrow{q}=\varnothing \text{ or its first marker is }\mathsf{exp}$$?\alpha \text{ fresh}{\mathcal{M}}_1=\mathcal{M},?\alpha :[\mathrm{\Gamma }⊢B]$$m_{\alpha }:=?\alpha [{\mathrm{id}}_{\mathrm{\Gamma }}]$${\mathrm{\Xi }}_1{⊢}_h(a{}^{\mathsf{imp},\varrho }{m}_{\alpha };\mathrm{\Delta }[m_{\alpha }/x];R[m_{\alpha }/x])@\overrightarrow{q}⟹b:D⊣{\mathrm{\Omega }}_2$

${\mathrm{\Xi }}_0{⊢}_h(a;{\mathrm{\Delta }}_h;R)@\overrightarrow{q}⟹b:D⊣{\mathrm{\Omega }}_2$

${\mathrm{\Delta }}_h=(x:B{)}^{ϵ,\varrho ,\omega },\mathrm{\Delta }$${\mathrm{\Xi }}_0⊢e\Leftarrow B⇝d⊣{\mathrm{\Omega }}_1$${\mathrm{\Xi }}_1{⊢}_h(a{}^{ϵ,\varrho }d;\mathrm{\Delta }[d/x];R[d/x])@\overrightarrow{q}⟹b:D⊣{\mathrm{\Omega }}_2$

${\mathrm{\Xi }}_0{⊢}_h(a;{\mathrm{\Delta }}_h;R)@(e^{ϵ},\overrightarrow{q})⟹b:D⊣{\mathrm{\Omega }}_1\diamond {\mathrm{\Omega }}_2$

$x:A\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x{⇝}_{\mathsf{P}}x:A$

$c[\overrightarrow{\ell }]:A\text{ is a fully instantiated signature atom}$

$\mathrm{\Gamma }⊢c[\overrightarrow{\ell }]{⇝}_{\mathsf{P}}c[\overrightarrow{\ell }]:A$

$\mathrm{\Gamma }⊢a:Aa,A\text{ contain no metavariables}$

$\mathrm{\Gamma }⊢\mathrm{\_}{⇝}_{\mathsf{P}}a:A$

$\mathrm{\Gamma }⊢A{⇝}_{\mathsf{P}}^{\mathsf{type}}{A}^{\prime }\mathrm{\Gamma }⊢e{⇝}_{\mathsf{P}}a:A^{\prime }$

$\mathrm{\Gamma }⊢(e:A){⇝}_{\mathsf{P}}a:A^{\prime }$

$\mathrm{\Gamma }⊢B\mathsf{type}\mathrm{\Gamma },x:B⊢C\mathsf{type}$$\mathrm{\Gamma },x:B⊢e{⇝}_{\mathsf{P}}b:C$

$\mathrm{\Gamma }⊢{\lambda }^{ϵ,\varrho }x.e{⇝}_{\mathsf{P}}{\lambda }^{ϵ,\varrho }(x:B).b:\prod _{x:B}^{ϵ,\varrho }C$

$\mathrm{\Gamma }⊢B\mathsf{type}\mathrm{\Gamma },x:B⊢C\mathsf{type}$$\mathrm{\Gamma }⊢e_0{⇝}_{\mathsf{P}}a:B$$\mathrm{\Gamma }⊢e_1{⇝}_{\mathsf{P}}b:C[a/x]$

$\mathrm{\Gamma }⊢(e_0,e_1){⇝}_{\mathsf{P}}(a,b):\sum _{x:B}C$

Rules P-Lam and P-Pair are the two genuinely checking-directed introductions. They display the expected type that generation weak-head inverts, copy the product metadata, and substitute the first pair component into the second component’s type. Atoms and every declared constructor or eliminator instead use P-Atom or the exact signature-head relation below; there is no duplicate introduction route. Type formation belongs to the separate relation below; it is not a term introduction into a guessed common universe.

For a surface vector level, ${\mathsf{level}}_{\mathsf{P}}(\hat{\ell })=\ell$ copies a written level and, when the level is omitted, selects the metavariable-free formation witness stored by the candidate elaboration. The type relation for this policy is exactly:

$e\not\equiv \mathrm{\_}$$\mathrm{\Gamma }⊢e{⇝}_{\mathsf{P}}a:T$$\mathsf{whnf}(T)={\mathcal{U}}_u$

$\mathrm{\Gamma }⊢e{⇝}_{\mathsf{P}}^{\mathsf{type}}a$

$p\text{ is a well-formed level expression}$

$\mathrm{\Gamma }⊢{\mathcal{U}}_p{⇝}_{\mathsf{P}}^{\mathsf{type}}{\mathcal{U}}_p$

$D\in \{\mathbf{1},\mathbf{2},\mathbb{N}\}$

$\mathrm{\Gamma }⊢D{⇝}_{\mathsf{P}}^{\mathsf{type}}D$

$\mathrm{\Gamma }⊢A{⇝}_{\mathsf{P}}^{\mathsf{type}}{A}^{\prime }$$\mathrm{\Gamma }⊢e_0{⇝}_{\mathsf{P}}{a}_0:A^{\prime }$$\mathrm{\Gamma }⊢e_1{⇝}_{\mathsf{P}}{a}_1:A^{\prime }$

$\mathrm{\Gamma }⊢{\mathsf{Id}}_A(e_0,e_1){⇝}_{\mathsf{P}}^{\mathsf{type}}{\mathsf{Id}}_{A^{\prime }}(a_0,a_1)$

${\mathsf{level}}_{\mathsf{P}}(\hat{\ell })=\ell$$\mathrm{\Gamma }⊢A{⇝}_{\mathsf{P}}^{\mathsf{type}}{A}^{\prime }$$\mathrm{\Gamma }⊢A^{\prime }:{\mathcal{U}}_{\ell }$$\mathrm{\Gamma }⊢n{⇝}_{\mathsf{P}}{n}^{\prime }:\mathbb{N}$

$\mathrm{\Gamma }⊢\mathsf{Vec}[\hat{\ell }](A,n){⇝}_{\mathsf{P}}^{\mathsf{type}}\mathsf{Vec}(A^{\prime },n^{\prime })$

$\mathrm{\Gamma }⊢A{⇝}_{\mathsf{P}}^{\mathsf{type}}{A}^{\prime }$$\mathrm{\Gamma },x:A^{\prime }⊢B{⇝}_{\mathsf{P}}^{\mathsf{type}}{B}^{\prime }$

$\mathrm{\Gamma }⊢\prod _{x:A}^{ϵ,\varrho }B{⇝}_{\mathsf{P}}^{\mathsf{type}}\prod _{x:A^{\prime }}^{ϵ,\varrho }{B}^{\prime }$

$\mathrm{\Gamma }⊢A{⇝}_{\mathsf{P}}^{\mathsf{type}}{A}^{\prime }$$\mathrm{\Gamma },x:A^{\prime }⊢B{⇝}_{\mathsf{P}}^{\mathsf{type}}{B}^{\prime }$

$\mathrm{\Gamma }⊢\sum _{x:A}B{⇝}_{\mathsf{P}}^{\mathsf{type}}\sum _{x:A^{\prime }}{B}^{\prime }$

There is deliberately no P-Ty-Hole. Rule E-Ty-Hole remains part of general constraint generation, but its fresh universe may remain ambiguous, and a mixed-level type need not inhabit any universe at all. The decidable completeness policy therefore requires written annotation types; it still admits explicit mixed-level $\mathrm{\Pi }$- and $\mathrm{\Sigma }$-types through P-Ty-Pi/P-Ty-Sigma. The syntactic side condition on P-Ty-El prevents the term-hole rule from reconstructing a whole omitted type by a second route. Rule P-Ty-Vec separately records the particular universe membership required by vector formation, including an omitted vector level determined by guard compilation.

Ordinary applications have no alternative insertion choice:

$\mathrm{\Gamma }⊢e{⇝}_{\mathsf{P}}a:A$$\mathrm{\Gamma }⊢(a:A)@\overrightarrow{q}{⇝}_{\mathsf{P}}b:B$

$\mathrm{\Gamma }⊢e\overrightarrow{q}{⇝}_{\mathsf{P}}b:B$

$\mathsf{whnf}(A)\text{ is not an implicit product}$

$\mathrm{\Gamma }⊢(a:A)@\varnothing {⇝}_{\mathsf{P}}a:A$

$\mathsf{whnf}(A)=\prod _{x:B}^{\mathsf{imp},\varrho }C$$\overrightarrow{q}=\varnothing \text{ or begins with an explicit marker}$$\mathrm{\Gamma }⊢d:Bd\text{ is the stored omitted core argument}$$\mathrm{\Gamma }⊢(a{}^{\mathsf{imp},\varrho }d:C[d/x])@\overrightarrow{q}{⇝}_{\mathsf{P}}b:D$

$\mathrm{\Gamma }⊢(a:A)@\overrightarrow{q}{⇝}_{\mathsf{P}}b:D$

$\mathsf{whnf}(A)=\prod _{x:B}^{ϵ,\varrho }C$$\mathrm{\Gamma }⊢e{⇝}_{\mathsf{P}}d:B$$\mathrm{\Gamma }⊢(a{}^{ϵ,\varrho }d:C[d/x])@\overrightarrow{q}{⇝}_{\mathsf{P}}b:D$

$\mathrm{\Gamma }⊢(a:A)@(e^{ϵ},\overrightarrow{q}){⇝}_{\mathsf{P}}b:D$

The remaining rule is indexed by the same finite signature telescope as E-Syn-Head. For the external-level telescope of $h$, define ${\mathsf{levels}}_{h,\mathsf{P}}(\overrightarrow{\hat{\ell }})=\overrightarrow{\ell }$ positionwise: copy a written level exactly, and at an omitted position select the metavariable-free level witness stored by the candidate elaboration.

$h:[\overrightarrow{u}]{\mathrm{\Delta }}_h\to R{\mathsf{levels}}_{h,\mathsf{P}}(\overrightarrow{\hat{\ell }})=\overrightarrow{\ell }$$\mathrm{\Gamma }{⊢}_h(h[\overrightarrow{\ell }];{\mathrm{\Delta }}_h[\overrightarrow{\ell }/\overrightarrow{u}];R[\overrightarrow{\ell }/\overrightarrow{u}])@\overrightarrow{q}{⇝}_{\mathsf{P}}b:B$

$\mathrm{\Gamma }⊢h[\overrightarrow{\hat{\ell }}]⟨\overrightarrow{q}⟩{⇝}_{\mathsf{P}}b:B$

The auxiliary head judgment has exactly the three telescope clauses E-Head-Done, E-Head-Infer, and E-Head-Write, replacing each generation premise by ${⇝}_{\mathsf{P}}$ and replacing each inferred metavariable by its stored metavariable-free core witness. In particular, there is still no omission clause for a written motive. This completes the inductive policy relation and fixes every implicit, external-level, binder, and motive choice used by the completeness proof.

Annotations thread type checking into subject checking. Pair checking Annotations thread type checking into subject checking. Pair checking weak-head inverts a $\mathrm{\Sigma }$-type and threads the first component into the second. Application uses the auxiliary spine clauses of definition 112.6: insert every consecutive declared implicit binder, then check the written explicit argument. Each emitted core application copies the exposed product’s explicitness and relevance; a mismatch of written and exposed explicitness is rejected. A flexible head is outside the direct fragment until an annotation exposes a product with declared relevance. Every nonbinding declared head—including program constants, constructors, and eliminators—uses the finite signature schema: traverse its declaration telescope in dependency order, create omitted level and implicit metavariables, check each written argument at its substituted domain, and return the complete core head at its substituted result, copying both bits from every declaration-telescope binder to its application node. Motives are written inputs. The two binding schemas form $A\Leftarrow \mathsf{type}$, open the written binder in $\mathrm{\Gamma },x:A^{\prime }$, form $B\Leftarrow \mathsf{type}$, and thread the domain’s output state into the body. The $\mathrm{\Pi }$-schema returns $\prod _{x:A^{\prime }}^{ϵ,\varrho }{B}^{\prime }$ as a well-formed type and copies its written metadata; the $\mathrm{\Sigma }$-schema returns $\sum _{x:A^{\prime }}{B}^{\prime }$ as a well-formed type and has no such metadata. The finite type-mode clauses use the exact formation premises of every remaining Timpl former. In particular, a variable or declared constant synthesizing a universe type is returned as a type by U-El; a type-mode hole declares a fresh universe element. The vector clause is exactly E-Ty-Vec of definition 112.6: it first elaborates the element by the type-mode judgment, checks the length at $\mathbb{N}$, and appends the suspended guard $\mathrm{\Gamma }⊢A^{\prime }\dot{\in }{\mathcal{U}}_{\ell }$ to the guard projection of $\mathcal{C}$. Thus $\mathcal{C}$ is an ordered equation list together with an ordered guard list, and no guard is sent to the object unifier. After object substitution, the exact compiler of definition 112.11 follows the Timpl formation rules: universes emit $p+1\le \ell$; base types emit $0\le \ell$; products and sums recurse over domain and codomain; identity and vector types recurse over their element type; a rigid neutral synthesized at ${\mathcal{U}}_q$ emits $\ell {\doteq }_{\mathsf{L}}q$; and a flexible head returns outside. These emitted level constraints join the same stratified level problem as the constraints generated during traversal. These binding and nonbinding schemas, together with the displayed atomic, hole, direction-changing, application, pair, projection, and annotation clauses, are the complete finite generation definition.

The type-mode hole belongs only to general constraint generation. The decidable completeness policy of definition 112.31 has no P-Ty-Hole, and the side condition on P-Ty-El forbids reconstructing a whole type through the term-hole rule.

Object constraints have form $\mathrm{\Gamma }⊢A\doteq B\mathsf{type}$ or $\mathrm{\Gamma }⊢(s:S)\doteq (t:T)$. A type equation compares well-formed types without placing them in a common universe. For a term equation, solve the type equality first, convert to a homogeneous term equation, weak-head normalize, and delete every reflexive normal equation before head classification. Equal rigid heads decompose left to right; unequal heads fail. A direct-pattern flex–rigid equation assigns the contextual abstraction exactly under the occurs, scope, dependency-order, and type checks of definition 112.18. That type check must succeed after equality substitution without using a residual formation bound; otherwise this fixed policy reports outside. Flex–flex uses the dependency-closed telescope intersection and metacontext insertion of definition 112.20. A flexible neutral with a following application or stuck eliminator, pruning, and any other non-pattern occurrence produce the distinct result outside the direct fragment, not unsatisfiable. Rigid comparison of two universes transfers a strict level equality into the level state. The equality pass immediately orients and substitutes it through the combined state before a suspended term task is exposed; a distinct rigid equality rejects there. Thus every later object assignment is genuinely well typed. An empty object state is still not success until the residual formation bounds have passed the bound solver.

Normalize a zero/successor/maximum level expression by distributing successor over maximum, retaining the largest offset for each external parameter, and deleting dominated numeral atoms. Two rigid level expressions agree under all external-parameter valuations exactly when these declaration-ordered normal forms are identical. Level constraints generated during syntax traversal or emitted during object simplification form the stratified problem of definition 112.12. A fresh equality metavariable receives at most one dependency-ordered assignment $q{\doteq }_{\mathsf{L}}e$; strict universe comparison uses this equality, never a cumulative lift. These assignments are substituted on demand before dependent object work. The remaining formation bounds are edges $p+k\le q$ with a bound metavariable on the right. A zero-weight edge from zero seeds every bound vertex. Positive cycles fail and acyclic path maxima give the least residual solution. The independent rechecker clauses of definition 112.27 check all written motives, vector and Boolean premises, external levels, explicitness, and relevance bits.

Shared-DAG unification

These three cards fix the represented problem, the complete root-class transition, and its pointer-machine schedule. They are the exact signatures for the Chapter 113 MGU and linearity statements.

The Timpl-clauses compiler

The source patterns are $$p::=x\mid c(p_1,\dots ,p_k)\mid .t\mid !.$$ Rows are linear and ordered. A constructor or absurd pattern in an erased column is a relevance error. In the first surviving row, the compiler chooses that row’s leftmost blocking pattern among the runtime columns. Before inspecting a later row’s assertions, it applies ordered priority: if the first surviving row contains only variables and dots, it validates only those dots, returns that row’s leaf, and discards every later row as redundant without validating it. At a split of $x:D(\overrightarrow{u})$, each constructor $c:(\overrightarrow{y}:{\mathrm{\Delta }}_c)\to D({\overrightarrow{v}}_c)$ generates $(\overrightarrow{u};x){\equiv }_{\mathrm{\Xi };D}({\overrightarrow{v}}_c;c(\overrightarrow{y}))$. The restricted indexed unifier returns a dependency-preserving substitution, a negative certificate, or stuck. The first specializes the whole frontier and recurses, the second omits that constructor, and the third returns $\mathsf{stuckEq}$ with its ordered residual equations. A dot is checked only when its row becomes the least surviving candidate; an absurd pattern succeeds only when every constructor has a negative certificate.

The compiler has exactly seven outcomes: The uncovered result alone carries a symbolic coverage witness. The two stuck forms distinguish unsolved indexed unification from a constructor pattern forced against a neutral image; the three bad forms reject a row against the source card. No additional abort result is implicit.

The restricted unifier consumes the leftmost equation and uses the fixed schedule Solution, indexed self-check plus Injectivity, Conflict, then Cycle; generated equations are prepended in telescope order and solutions are substituted globally. Variables inherited from the pre-split frontier are tagged old and constructor-telescope variables fresh. For a distinct variable–variable equation, the canonical orientation eliminates a fresh variable before an old one and otherwise the later telescope variable before the earlier one. It uses the first orientation whose occurs check succeeds and whose eliminand $x$ can be moved rightward, by the unique stable sequence of adjacent exchanges, to just after the rightmost later declaration free in its solution term. Every declaration crossed must be independent of $x$, and all other relative order is preserved. Thus the successor-vector constraint preserves old $r$ and solves fresh $q:=r$; $x=x$ still has no deletion rule. Specialization processes the selected column exactly once. Matching constructor patterns expose subpatterns, different heads delete a row, variables record the forced constructor, dots retain a row-local judgmental-equality obligation, and an absurd pattern retains a row-local reachable-absurd marker. In the latter three retained cases, the row also receives one fresh variable pattern for each declaration of the constructor telescope. A matching constructor row receives its constructor subpatterns, whose number is that same telescope length. Thus replacing one selected frontier declaration by ${\mathrm{\Delta }}_c$ replaces its selected pattern in every retained row by exactly $|{\mathrm{\Delta }}_c|$ patterns. For any other declaration eliminated by the substitution, a separate recursive forced-image matcher consumes its pattern cell without adding frontier cells: matching constructor heads recurse, different heads delete, and variables, dots, and absurd patterns record a binding, obligation, or marker. A constructor pattern forced against a neutral image records a suspended task. Only when its row becomes least does the compiler retry that task: a matching head consumes it, a different head deletes the row, and a still-neutral image returns $\mathsf{stuckForce}$. Likewise a reachable-absurd marker or invalid dot is raised only for the least row; a prior successful row makes every later invalid row redundant instead.

Typed trees have exactly the forms $$\mathsf{leaf}(i,e),\mathsf{split}(x,\{c\mapsto ({\sigma }_c,{\mathcal{C}}_c)\}),\mathsf{absurd}(x,\{{\nu }_c\}).$$ An empty reachable matrix is an uncovered-constructor error. Tree translation uses only Timpl eliminators; a recursive leaf may use only the direct-child component supplied by its structural eliminator. The generated judgmental equations are exactly the reachable leaf equations, with ordered-row priority.