Lectures onType Theory
Chapter 111
Chapter 111Core route

Canonicity, Normalization, and Decidable Conversion

A closed Boolean may be hidden beneath binders, applications, and eliminators; for example b0:=(λf.fff)(λx.ind2(y.2;ff,tt,x)):2 reduces to tt. Two different questions are hidden in that calculation. Is every closed Boolean judgmentally one of the two constructors? And do open terms—the terms a kernel actually compares—have computable canonical representatives?

A predicate tested only at closed instantiations can classify b0, but it contains no datum for an open variable of function type. A kernel comparison therefore needs a context-indexed predicate stable under substitution into a larger context. Stability under weakening alone is insufficient: a dependent function must accept arguments containing variables introduced in the larger context. The normalization proof below is forced by that obstruction. Its logical relation records an action by finite semantic substitutions, and readback turns the resulting semantic evidence into the canonical representatives needed by conversion.

The canonicity theorem

Canonicity asserts that closed terms compute; the proved instance here says that every closed boolean of TΠ2 is judgmentally a constructor.

Definition 49.1 — Canonical forms

The canonical forms of closed Boolean type are the constructor terms tt and ff. Recall from definition 1.36 that the numerals are the closed terms sucm(0) for m a meta-level natural number, where suc0(0):=0 and sucm+1(0):=suc(sucm(0)).

Convention 111.2 — Ambient metatheory

The set-valued computability proof in this section is carried out in ZFC. Its syntax, derivations, and every indexed family below are sets; Replacement and Power Set form the required products. Because TΠ2 has no object-language universes, no Grothendieck universe or inaccessible cardinal is used. The open normalization theorem for Timpl is proved locally later in this chapter, in ZFC; no published normalization theorem is used in that proof. The separate source-signature construction is comparative and remains confined to its cumulative signature TCoq.

Remark 111.3 — Why a metatheory is visible

A logical-relations proof needs an ambient theory able to form the relation and justify its recursion. When a recursively axiomatized object theory is strong enough for Gödel’s second incompleteness theorem, a normalization proof yielding its consistency cannot in general be internalized in that same theory. This structural warning does not impose a large cardinal on the weak fragment here; it explains why the ambient theory must nevertheless be named.

One half of canonicity is available at once: tt and ff cannot be judgmentally equal.

Proposition 49.3

There is no TΠ2 derivation of ttff:2.

Proof of Proposition 49.3

Proof. Use the two-point set model of exactly the named calculus TΠ2. Interpret a context as the set of its environments, Π as dependent function space, and 2 as {0,1}, with its eliminator defined by the two cases. Induction on a derivation shows that every structural, Π-, and Boolean rule preserves this interpretation: the two computation cases are the defining equations of application and case analysis, and congruence and conversion use equality of functions and elements. Thus a derivation of ttff:2 would imply 0=1, which is false. ◻

Remark 49.4

A syntactically shorter proof, though not a model-free one, is available in the larger base signature: if ttff:2, then by congruence Id2(tt,tt)Id2(tt,ff) type, so the conversion rule turns refl into a closed term of Id2(tt,ff); applying the map of example 30.12 yields a closed term of 0. Under the set-theoretic assumptions of convention 48.28, this contradicts corollary 90.7. That theorem is itself proved by a set model; the alternative is shorter in object-language syntax, not independent of semantics.

The other half is the statement to be proved.

Target B (Boolean canonicity). Let b:2 in the fragment with the structural rules, Π, and 2, denoted TΠ2. Then at least one of btt:2 and bff:2 holds; with proposition 49.3 that makes it exactly one. The numbered form and its proof are theorem 49.2.

Remark 49.5

Canonicity is stated per type. For a fragment containing N, its natural-number instance is the assertion n:Nnsucm(0):Nfor a unique m. The Boolean theorem of this section does not establish that assertion: the computability predicate and fundamental lemma must first be extended with the N rules. Likewise, canonicity at 0 would imply consistency, while identity-type canonicity would identify every closed p:IdA(a,b) with reflexivity and hence give ab:A. None of these larger-signature consequences is used in this chapter.

Remark 49.6

Canonicity concerns the empty context only. In context x:2, the variable x is judgmentally equal to neither constructor. If xtt, substitution of ff for x would give fftt, contradicting proposition 49.3; substitution of tt refutes xff in the same way. Variables manufacture non-canonical terms at every type. Closed TΠ2 terms reduce to canonical form; open terms may remain neutral.

Exercise 49.2

★☆☆ Work in the base signature through chapter 30, and assume identity-type canonicity and Boolean separation for that signature. From v:0 use 0-elimination to construct a closed term of Id2(tt,ff) and derive a contradiction. State why this proves consistency of the named base, and why Boolean canonicity alone does not supply the identity-type conclusion.

Computability: proof of canonicity

We now prove Target B by a proof-relevant computability construction. Its evidence-carrying predicates are the elementary form of the gluing model used later for universes.

Convention 49.8 — The fragment T_0

In this section TΠ2 denotes the fragment of the base theory with: the structural rules (definition 26.22); x:AB with β and η (definition 27.2); and 2 with its dependent eliminator ind2(x.C;c0,c1,b) and its two computation rules (definition 28.7). There are no universes; the extension to the full base theory is discussed in remark 49.13, remark 49.10. Premises of rules are compressed per convention 26.14.

The normal forms used below are η-long: a neutral function is reified as a lambda that applies the neutral to a fresh reflected variable. Kernel implementations may use weak-head reduction internally, but no oriented reduction relation is needed in the Tait proof or in the normalization theorem stated here. In particular, Π-η is used as expansion during readback, not as a proposed left-to-right rewriting step.

We write WTm(,A) for the set of well-typed raw terms a with a:A; the symbol Tm is reserved for a term-family component when working with categories with families. For a meta-level statement P, the subsingleton {kP} denotes {x{k}P}: it contains k if P holds and is empty otherwise.

A direct induction on Γt:A that asks only whether the closed instance t[γ] computes fails at application. The induction hypothesis for f:x:AB must be usable at every closed a:A[γ], and its result must land in the changing fiber B[γ,a/x]; a Boolean-valued predicate on f contains neither the argument evidence nor that fiber. This failed attempt forces the proof-relevant, type-indexed assignment below.

Definition 49.9 — Computability assignment

Work under convention 111.2. Fix a default set returned by a term clause whose stated domain condition fails; a malformed type clause returns the constantly empty family. The fundamental lemma proves that neither fallback is reached on well-typed inputs. A computability assignment attaches to each raw expression both its closed instance and evidence indexed by its type. To every raw expression t of TΠ2 with free variables among Γ=(x1:A1,,xn:An) assign, by structural recursion on t, an operation t on a computable closing instantiation (γ,γ). Here γ=(a1,,an) is a list of closed terms and γ=(a1,,an) is its evidence list. We write t[γ] for simultaneous substitution.

For a raw domain annotation A, put DA(γ,γ):=aWTm(,A[γ])A(γ,γ)(a). This is a set. For the clauses below, abbreviate abs:=λ(x:A).b,E:=ind2(x.C;c0,c1,b),test:=b(γ,γ). The term clauses are: xi(γ,γ):=aitt(γ,γ):=1,ff(γ,γ):=0,abs(γ,γ):=[(a,a)DA(γ,γ)b((γ,a),(γ,a))](fa)(γ,γ):=f(γ,γ)(a[γ],a(γ,γ))E(γ,γ):={c0(γ,γ)if test=1,c1(γ,γ)if test=0. The application clause is used only when the displayed pair lies in the domain of f(γ,γ); application returns otherwise. The clauses for type expressions produce families of sets, indexed by closed terms: 2(γ,γ):=b{1btt:2}{0bff:2}(x:AB)(γ,γ):=faWTm(,A[γ])  aA(γ,γ)(a)B((γ,a),(γ,a))(fa) Finally, the sets of computable closing instantiations for contexts: :={((),())}(Γ,x:A):={((γ,a),(γ,a))|(γ,γ)Γ,aWTm(,A[γ]), aA(γ,γ)(a)} The membership test in the context clause is total even before the fundamental lemma: when A(γ,γ) is not a family, the fallback convention makes the test false. The abstraction clause is a set function on the displayed set DA, rather than an unrestricted proper-class operation. The fundamental lemma subsequently proves that this fallback is never reached by a computable closing instantiation.

Example 111.10 — The assignment computes

For e:=(λx.x)tt in the empty context, the semantic calculation is e((),())=application(λx.x)((),())(tt,1)=abstractionx((tt),(1))=variable1. The resulting witness lies in 2((),())(e) because ett. Thus application consumes both the closed argument and its computability evidence, exactly as required by the failed direct induction.

Remark 49.10

Evidence is a structure, not a property: 2(b) is a set that could a priori contain both 0 and 1. Nothing in definition 49.9 presumes that the two disjuncts exclude each other — that is proposition 49.3, proved by a model, not by the recursion. Proof-relevance is idle in TΠ2 but indispensable for universes: a computability predicate for c:U0 must be defined by recursion on evidence that c is convertible to a type constructor, and if c were convertible both to 2 and to some x:AB the recursion would be ambiguous. Taking evidence as data — the evidence for c contains the computability family for Elt(c) — dissolves the ambiguity.

The assignment interacts with substitution exactly as evaluation does.

Lemma 49.11 — Weakening and substitution for (-)^

Let t have free variables among (Γ,x:A) and let (γ,γ)Γ.

  1. If x is not free in t, then t((γ,a),(γ,a))=t(γ,γ) for all (a,a).

  2. For a with free variables among Γ, (t[a/x])(γ,γ)=t((γ,a[γ]),(γ,a(γ,γ))).

Proof of Lemma 49.11 — Weakening and substitution for (-)^

Proof. Proceed simultaneously by structural induction on t. For a variable y, clause (1) is lookup in the unchanged part of the instantiation. For clause (2), the case y=x reads a(γ,γ)=a(γ,γ); the case yx is again unchanged lookup. For either Boolean constant, both clauses reduce to reflexivity.

For application, the induction hypotheses give f1=f2 and a1=a2; congruence of meta-level application gives f1(a1)=f2(a2). For λy.b, alpha-rename y away from x, a, and γ. The induction hypothesis for the stored domain annotation identifies the two sets DA; apply the body induction hypothesis after extending both instantiations by an arbitrary pair (c,c); extensionality of meta-level functions gives the displayed equality of semantic abstractions. For the Π-type clause, apply the body induction hypothesis after adjoining an arbitrary pair (c,c), then use extensionality at every factor of the dependent product.

For Boolean elimination, the scrutinee induction hypothesis gives equal values r1=r2{0,1}, so both eliminators select the same branch. If that value is 1, the true-branch induction hypothesis equates the returned evidence; if it is 0, the false-branch induction hypothesis does. The motive induction hypothesis equates the selected fibers. ◻

Lemma 49.12 — Fundamental lemma of computability

Let (γ,γ)Γ. Then, in TΠ2:

  1. If ΓA type, then A(γ,γ) is a family of sets indexed by WTm(,A[γ]), invariant under judgmental equality: ab:A[γ]impliesA(γ,γ)(a)=A(γ,γ)(b).

  2. If ΓAB type, then A(γ,γ)=B(γ,γ).

  3. If Γt:A, then t(γ,γ)A(γ,γ)(t[γ]).

  4. If Γts:A, then t(γ,γ)=s(γ,γ)A(γ,γ)(t[γ]).

Proof of Lemma 49.12 — Fundamental lemma of computability

Proof. Induct simultaneously on the four judgment forms in clauses (a)–(d): type formation yields an equality-invariant computability family, type equality equates such families, typing yields evidence, and term equality equates evidence. Begin with dependent-product formation.

(a), Π-formation. By induction hypothesis (a) for A and, for each (a,a), for B at the extended instantiation, each displayed product is a set by Replacement and Power Set in convention 111.2. For invariance, suppose fg:x:A[γ]B[γ]. For each admissible (a,a), congruence of application gives faga:B[γ][a/x], so the factors agree by induction hypothesis (a) for B; hence the products agree. (The 2 case is transitivity.)

(c), variable rule. By definition of Γ, xi(γ,γ)=ai, which lies in Ai()(ai); and xi[γ]=ai.

(c), Π-introduction. Let Γ,x:Ab:B. We must show that the evidence (λx.b)(γ,γ) lies in the product over (a,a) of B((γ,a),(γ,a))((λx.b[γ])a). Fix (a,a). By induction hypothesis (c) for b, b((γ,a),(γ,a))B((γ,a),(γ,a))(b[γ][a/x]). The β-rule gives (λx.b[γ])ab[γ][a/x]:B[γ][a/x], so by invariance (a) for B the two fibers coincide, and the clause for (λx.b) produces exactly the required dependent function.

(c), Π-elimination. Let Γf:x:AB and Γa:A. By induction hypotheses (c), f(γ,γ) is a dependent function as above and a(γ,γ)A(γ,γ)(a[γ]); instantiating at (a[γ], a(γ,γ)) gives an element of B((γ,a[γ]),(γ,a(γ,γ)))(f[γ]a[γ]), which by lemma 49.11(2) is the required set (B[a/x])(γ,γ)((fa)[γ]).

(c), Boolean elimination. Let e:=ind2(x.C;c0,c1,b). The scrutinee induction hypothesis gives b(γ,γ){1b[γ]tt}{0b[γ]ff}. Hence its value is either 1 or 0. In the first case, membership and 01 give a derivation q:b[γ]tt:2. The branch induction hypothesis gives evidence for c0[γ] in the fiber of (C[tt/x]). Substitution congruence along q, followed by the 2 computation rule, gives C[b/x][γ]C[tt/x][γ] type,e[γ]c0[γ]:C[b/x][γ]. Clauses (a)–(b) and lemma 49.11(2) therefore move the branch evidence to the required fiber (C[b/x])(γ,γ)(e[γ]); the semantic eliminator clause returns exactly that evidence because the scrutinee value is 1. If the value is 0, use b[γ]ff, the c1 induction hypothesis, and the false computation rule. This proves the dependent eliminator typing case rather than only its two computation equalities.

(d), β. With notation as in the introduction case, ((λx.b)a)(γ,γ)=applicationandabstractionb((γ,a[γ]),(γ,a(γ,γ)))=lemma49.11(2)(b[a/x])(γ,γ).

(d), 2-computation. tt(γ,γ)=1, so the eliminator clause selects c0(γ,γ), which is ind2(x.C;c0,c1,tt)(γ,γ) by definition; membership in the correct fiber uses invariance (a) for C as in the introduction case. For ff, the evidence value is 0, so the eliminator clause selects c1(γ,γ). Invariance (a) for C identifies its fiber with the one selected by substituting ff for x, which gives the required membership for 2-comp2.

(d), η. Let Γf:x:AB with x not free in f. For each (a,a), (λx.fx)(γ,γ)(a,a)=abstraction,application,variable(fx)((γ,a),(γ,a))=lemma49.11(1)f(γ,γ)(a,a). The two dependent functions agree pointwise, hence are equal.

(d), congruences and equivalence rules; (c), conversion rule. Congruences combine induction hypotheses (d) pointwise; symmetry and transitivity are those of meta-level equality; the conversion rule combines (c) with (b). More explicitly, λ-congruence applies the induction hypothesis for the bodies at every computable (a,a); Boolean-eliminator congruence uses the induction hypotheses for the motive, both branches, and the scrutinee, after which both semantic eliminators choose the same branch. For Π-congruence in (b), the domain induction hypothesis gives A(γ,γ)=A(γ,γ), and, for every (a,a) in this common index set, the codomain induction hypothesis gives B((γ,a),(γ,a))=B((γ,a),(γ,a)). Thus the two dependent products are equal. In the structural cases, lemma 49.11(1) is the weakening equation and clause (2) is the substitution equation; exchange permutes the instantiation list and contraction replaces its final two equal coordinates by the diagonal. Together with the explicit Π and 2 cases above, these equations establish clauses (a)–(d) for every last rule of TΠ2. ◻

Theorem 49.2 — Boolean canonicity for the elementary fragment

Let b:2 in TΠ2. Then exactly one of btt:2orbff:2 holds.

Proof of Theorem 49.2 — Boolean canonicity for the elementary fragment

Proof. Let b:2. Instantiate lemma 49.12(c) at the empty instantiation ((),()): b((),())2((),())(b)={1btt:2}{0bff:2}. This set is inhabited, so at least one disjunct holds. At most one holds by proposition 49.3 and transitivity. ◻

Remark 49.13 — The full base theory

The elementary assignment illustrates the closed-term half of the general construction. For the non-universe formers of the base theory its first clauses are: 1(γ,γ)(u):={0}0(γ,γ)(v):=N(γ,γ)(n):={mNnsucm(0):N} (x:AB)(γ,γ)(p) is the set of pairs of evidence for pr1p and for pr2p at the correspondingly instantiated B; and IdA(a,b)(γ,γ)(p) is the set of pairs (q,r) in which q is a derivation of a[γ]b[γ]:A[γ] and r is a derivation of prefla[γ]:IdA[γ](a[γ],b[γ]). The endpoint derivation q makes the displayed reflexivity proof well typed; the proof derivation r then validates the computation rule of J (definition 30.1): congruence replaces p by refla[γ], after which the J computation rule selects the reflexivity branch. Universes require the proof-relevant clause sketched in remark 49.10: evidence for c:Ui is a pair of a constructor form for c and a computability family for its elements. W-evidence must additionally be inductive in the semantic subtrees.

Listing these clauses does not prove their substitution stability, and that is the exact reason the rest of the chapter does not proceed by enlarging (). Each clause above evaluates a term at a closing instantiation; a term under a binder has none, and the two exercises below are the only consequences that closed instantiations alone can carry. The open construction that replaces (), and the theorem it proves for the kernel signature, are definition 111.65 and theorem 111.76.

Exercise 49.3

★★☆ Prove lemma 49.11. (Structural induction on t; the variable clauses are the base cases, and the binder cases use α-renaming as fixed by definition 26.1.)

Exercise 49.4

★★☆ Reconstruct from lemma 49.12 the ξ-rule for λ, congruence for ind2, and part (b) for the Π-congruence rule. For each reconstruction, display the exact extended instantiation and the induction hypothesis that identifies the two semantic outputs.

Exercise 49.5

★★☆ Using the N clause of remark 49.13 and clauses for 0, suc, indN, prove canonicity at N (remark 49.5). Where does the induction need the evidence m rather than mere inhabitation?

Exercise 49.6

★★☆ Assume that the identity-type clause of remark 49.13 satisfies the four conclusions of lemma 49.12. Prove that if p:IdA(a,b), then prefla:IdA(a,b) and ab:A. Identify the two components of the stored identity evidence; no constructor-injectivity hypothesis is needed. Explain why neither the Tait argument of section 49.2 nor theorem 49.17 supplies the assumed identity clause.

The kernel signature, its reduction, and its normal forms

Canonicity governs closed terms. The kernel of chapter 48 compares open ones: its four inversion operations and its two conversion queries are applied in an arbitrary context, and proposition 110.17 records that nothing there constructs them. Everything below is therefore carried out at the full signature named in convention 110.16, and the first task is to write that signature’s raw syntax, its computation steps, and the shape a canonical representative can have.

Convention 111.16 — Kernel raw syntax

Write Timpl for the signature of convention 110.16: the structural rules of definition 26.22; Π with β and η (definition 27.2) carrying the explicitness bit ϵ{exp,imp} and the relevance bit ϱ{runtime,erased}; Σ with both projections, both β-rules and η (definition 27.9); 1 with η (definition 27.14); 2 (definition 28.7); N (definition 28.21); intensional identity with J (definition 30.1); the strict Russell universes of definition 29.1 together with the explicit strict lifts of definition 29.10 and Lift-Id; and the vector family with the eliminator vind of definition 78.1. Its raw expressions are one sort, because U-El uses a universe element directly as a type: ::=0u+1max(,)a,A::=xULift(a)x:Aϵ,ϱBλϵ,ϱ(x:A).baϵ,ϱbx:AB(a,b)pr1(a)pr2(a)12ttffind2(x.C;a,b,c)N0suc(a)indN(x.C;a,b,c)IdA(a,b)reflaJA;a;b(x.y.p.C;z.c;q)Vec(A,a)vnilvcons(a,b,c)vind(M;p0;S;a,b),M:=n.v.P,  S:=n.a.xs.q.ps Here u ranges over external level parameters (convention 29.3), so a level expression denotes a natural number once its parameters are given values, and a judgment is a schema in those parameters. Lemma 111.19 shows that the schema may be decided symbolically. Every binder displayed before a dot is part of the raw constructor: vind binds two variables in its motive and four in its successor branch, exactly as Vec-elim does.

Two omissions from convention 111.16 are deliberate and are not repaired anywhere below: Timpl has no W-type and no coinductive former, so the theorems of this chapter say nothing about the signature Timpl-co obtained by adding one.

Remark 111.17 — What the two bits are, for reduction

The pair (ϵ,ϱ) is checked kernel syntax (convention 110.16): a formation, introduction, elimination, computation or uniqueness rule applies only when the three occurrences belonging to one binder carry the same pair. Consequently x:Aϵ,ϱB and x:Aϵ,ϱB with (ϵ,ϱ)(ϵ,ϱ) are distinct types with no rule relating them, and (λϵ,ϱ(x:A).b)ϵ,ϱa with mismatched pairs is not a redex. Erasing both bits from every occurrence maps each rule of Timpl to the corresponding rule of definition 27.2; nothing below uses more about them than this equality test.

Definition 111.18 — Level expressions in normal form

An atom is a level expression u+n with u a parameter and nN. A level expression is in level normal form when it is written max(n0, u1+n1, , uk+nk), with u1,,uk pairwise distinct parameters listed in a fixed order of parameters, and with the constant n0 present exactly when either k=0 or n0>max1jknj. Write for the expression obtained by

  1. distributing ()+1 over max and flattening nested maxima;

  2. replacing two atoms u+n, u+m on the same parameter by u+max(n,m), and merging all constants into one n0;

  3. deleting n0 when k1 and n0maxjnj.

Step (3) is not cosmetic: max(1,u+1) and u+1 denote the same function, because u+11 for every value of u, so a normal form that retained the constant 1 would not be unique.

Lemma 111.19 — Deciding level equality and level order

Let , be level expressions over parameters u1,,um, and call two expressions equivalent when they denote the same natural number under every assignment of naturals to those parameters.

  1. is in level normal form and is equivalent to .

  2. and are equivalent if and only if and are the same expression.

  3. Whether < holds under every assignment is decidable.

Proof of Lemma 111.19 — Deciding level equality and level order

Proof. (1) Each step preserves the denoted number under every assignment: max(1,2)+1=max(1+1,2+1) and max is associative, commutative and idempotent, giving step (1); max(u+n,u+m)=u+max(n,m) gives step (2); and if n0nj for some j, then uj+njnjn0 under every assignment, so deleting n0 changes nothing, giving step (3). Steps (2) and (3) leave the shape required by definition 111.18.

(2) One direction is (1). For the other, let and be equivalent normal forms. Fix a parameter uj and evaluate both at uj:=N with every other parameter 0. For N larger than every offset occurring in either expression, the value is N+nj if uj occurs with offset nj, and is a constant independent of N otherwise. Comparing the values at two such N shows that uj occurs in both normal forms or in neither, and that its offsets agree when it occurs. So the atom sets coincide; write M:=maxjnj for their common maximal offset when k1. Now evaluate both at the all-zero assignment. If k=0 both expressions are their constants, which are therefore equal. If k1, the value is n0 when the constant is present—since then n0>M—and M when it is absent. Hence the common value determines whether the constant is present and, if so, its size. The two normal forms are therefore the same expression.

(3) < holds under every assignment exactly when +1 does. A maximum is at most R exactly when each of its entries is, so test the entries of +1=max(m0,u1+m1,) separately against R:=. An atom u+m satisfies u+mR under every assignment if and only if u occurs in R with an offset nm: the condition is sufficient because u+mu+n, and necessary because otherwise R is bounded in u or grows with a smaller offset, and taking u large refutes the inequality. The constant m0 satisfies m0R under every assignment if and only if m0R(0,,0), because R is monotone in each parameter, so its minimum is at the all-zero assignment. Each test compares finitely many natural numbers. ◻

Reduction now records what the computation rules do when read from left to right. The uniqueness rules Π-η, Σ-η and 1-η are deliberately absent from it; they are not left-to-right steps, and definition 49.14 builds them into the shape of a normal form instead.

Definition 111.20 — Root contraction

Root contraction 0 is the least relation on raw expressions containing the following instances, in which every displayed Π-triple carries one and the same pair (ϵ,ϱ). (λϵ,ϱ(x:A).b)ϵ,ϱa0Πβb[a/x],pr1((a,b))0Σβ1a,pr2((a,b))0Σβ2b,ind2(x.C;ct,cf,tt)02comp1ct,ind2(x.C;ct,cf,ff)02comp2cf,indN(x.C;c0,cs,0)0Ncomp1c0,indN(x.C;c0,cs,suc(m))0Ncomp2csm(indN(x.C;c0,cs,m)),JA;a;a(x.y.p.C;z.c;refla)0Idcompc[a/z],vind(M;p0;S;0,vnil)0Veccomp1p0,vind(M;p0;S;suc(m),vcons(m,c,ys))0Veccomp2ps[m/n,c/a,ys/xs,r/q], with M,S the two binder groups of convention 111.16 and r:=vind(M;p0;S;m,ys), together with the strict-lift instances Lift(x:Aϵ,ϱB)0LiftPix:LiftAϵ,ϱLiftB,Lift(x:AB)0LiftSigx:LiftALiftB,Lift(IdA(a,b))0LiftIdIdLiftA(a,b),Lift(K)0LiftKK,Lift(Uk)0LiftHierUk for K{1,2,N}, where Lift-K abbreviates the three rules Lift-Unit, Lift-Bool, Lift-Nat of definition 29.10, and Vec-comp1, Vec-comp2 are the two equations that definition 78.1 names Vec-comp.

Remark 111.21 — The two lift instances that are missing

Definition 29.10 supplies a commuting equation for every former it lists, and Lift-Id was added with the identity type. The vector family was introduced later (definition 78.1) and no Lift-Vec equation accompanies it, so Lift(Vec(A,n))andVec(LiftA,n) are two elements of U+1 with no derivable equation between them, although Lift-El makes the first of them equal, as a type, to Vec(A,n). Neither is Vec-formation a congruence across a lift: its element premise is a term of a fixed universe, and LiftA and A never inhabit the same one. The same holds for an iterated lift Lift+1(Lift(A)), which has no equation collapsing it. Nothing below repairs the signature: the normal codes of definition 49.14 keep both stuck lifts, the conversion procedure of theorem 111.81 therefore rejects Lift(Vec(A,n))Vec(LiftA,n) at U+1, and it accepts ΓLift(Vec(A,n))Vec(A,n) type. A signature that wanted the two codes identified would have to add the equation and re-check lemma 111.74 for it.

Definition 111.22 — Reduction and weak-head reduction

One-step reduction is the compatible closure of 0: it contracts one redex in an arbitrary subexpression, including under a binder. Its reflexive-transitive closure is .

Weak-head reduction contracts only in a head position, and the head positions are fixed by the following grammar of head contexts. Its last two productions are ordered, so that exactly one hole is available in a vind node. H::=Hϵ,ϱapr1(H)pr2(H)Lift(H)ind2(x.C;ct,cf,H)indN(x.C;c0,cs,H)JA;a;b(x.y.p.C;z.c;H)vind(M;p0;S;m,H)vind(M;p0;S;H,w) The last production carries the side condition that w admit no weak-head step; the two before it are unrestricted. A weak-head step carries Ha to Hb whenever a0b; the expression Hb is then the weak-head reduct of Ha. Weak-head reduction is the reflexive-transitive closure of that step, and a raw expression is a weak-head normal form when no weak-head step applies to it. No arrow is introduced for the relation: every statement below about it names the head context and the root instance, which is what the algorithm of remark 111.86 inspects. The side condition makes the vector argument of vind the principal one and its index the secondary one; without it, an expression whose index and vector are both redexes would have two weak-head reducts.

Lemma 111.23 — Substitution, weakening, and conversion for reduction

Let γ be a substitution of raw expressions for the variables of Γ.

  1. If a0b then a[γ]0b[γ].

  2. If ab then a[γ]b[γ], and if ab then a[γ]b[γ].

  3. If Γa:A and ab, then Γab:A; if ΓA type and AB, then ΓAB type. Both statements extend to .

  4. Weak-head reduction is deterministic: an expression has at most one weak-head reduct.

Proof of Lemma 111.23 — Substitution, weakening, and conversion for reduction

Proof. (1) Inspect the ten computation instances and the five lift instances of definition 111.20. Choose the representative of each binder to avoid dom(γ) and the free variables of its images, which is possible by lemma 26.9. For Π-β the two sides become (λϵ,ϱ(x:A[γ]).b[γ+])ϵ,ϱa[γ]andb[γ+][a[γ]/x]=b[a/x][γ], the last equation being composition of capture-avoiding substitutions, where γ+ extends γ by xx. The bit pair is carried unchanged, so the instantiated pair still matches and the right-hand side is again an instance. Σ-β1,2, 2-comp1,2 and N-comp1 substitute into a subexpression only. N-comp2 and Vec-comp2 rebuild the same expression from substituted components, again by substitution composition, and Vec-comp2 additionally uses that its recursive call r is built from the very components being substituted. Id-comp needs its two endpoint annotations and its refl argument to remain the same expression after substitution, which they do because γ is applied to all four occurrences of a at once. The five lift instances are first-order rewrites of a head symbol and its arguments, and the level subscript is unaffected because levels are external.

(2) Induction on the one-step derivation, using (1) at the root and capture avoidance at each binder; then induction on the length of the reduction sequence. Weakening is the case where γ is an inclusion of contexts.

(3) Induction on ab. At the root, each instance of definition 111.20 is exactly the left-to-right reading of a computation rule of the signature, whose premises are recovered from Γa:A by inversion: for instance, if ΓindN(x.C;c0,cs,suc(m)):A, then N-elim gives Γ,x:NC type, Γc0:C[0/x], Γcs:StepN(C) and Γsuc(m):N, and N-comp2 is the required equation at C[suc(m)/x]; Conv moves it to A. The five lift instances are the equations of definition 29.10 and Lift-Id, which are equations in U+1 and hence type equations by U-El-Eq. In a compatible position the induction hypothesis supplies an equation for the redex and the congruence rule of the surrounding former—app-eq, pair-eq, pr1-eq, pr2-eq, the two eliminator congruences of definition 28.7, definition 28.21, Id-elim-eq, the Vec-elim congruence, Π-form-eq, the Σ-formation congruence of remark 27.10, Id-form-eq, or Lift-Cong—propagates it. Transitivity of judgmental equality closes .

(4) Let b be a weak-head reduct of a, so a=Ha0 with a0 a root redex and b=Ha0 for a00a0. We show that H and a0 are determined by a. The outermost symbol of a admits at most one production of the grammar of definition 111.22: application, the two projections, the two eliminators, J, Lift and vind each occur in exactly one production, except vind, which occurs in two. For a vind node the side condition decides between them: if the vector argument admits a weak-head step the first production applies and the second does not, and if it does not, only the second is available. So the decomposition proceeds deterministically down to the hole. Finally, at most one root instance applies to a0, because the left-hand sides of definition 111.20 have pairwise distinct head symbols, and where one head symbol carries several instances—ind2, indN, vind, Lift—the instances are distinguished by the constructor in the eliminated position. ◻

Definition 49.14 — Neutral and normal forms

Four judgments are defined by mutual induction: ΓuneA (u is neutral of type A), ΓvnfA (v is normal of type A), ΓAnftype (A is a normal type), and ΓcnfU (c is a normal code at level ), the last being a special case of the second. A neutral term is an elimination chain blocked on a variable; a normal term is β-normal and η-long. Premises recoverable from the rule data are compressed per convention 26.14. Every field that a raw constructor stores—a λ-domain, the three annotations of J, an eliminator motive, a refl argument, a vcons index—carries its own normality premise below; without that, two judgmentally equal terms could carry α-distinct annotations and no normal form would be canonical.

Neutrals:

(x:A)Γ
ΓxneA
ne-var
Γunex:Aϵ,ϱBΓvnfA
Γuϵ,ϱvneB[v/x]
ne-app
Γunex:AB
Γpr1(u)neA
ne-fst
Γunex:AB
Γpr2(u)neB[pr1(u)/x]
ne-snd
Γ,x:2CnftypeΓvtnfC[tt/x]ΓvfnfC[ff/x]Γune2
Γind2(x.C;vt,vf,u)neC[u/x]
ne-ind-bool
Γ,x:NCnftypeΓv0nfC[0/x]ΓvsnfStepN(C)ΓuneN
ΓindN(x.C;v0,vs,u)neC[u/x]
ne-ind-nat
ΓAnftypeΓvanfAΓvbnfAΓ,x:A,y:A,p:IdA(x,y)CnftypeΓ,z:AvnfC[z/x,z/y,reflz/p]ΓuneIdA(va,vb)
ΓJA;va;vb(x.y.p.C;z.v;u)neC[va/x,vb/y,u/p]
ne-J
ΓcnfUΓ,n:N,v:Vec(c,n)PnftypeΓv0nfP0ΓvsnfPsΓwnfNΓuneVec(c,w)
Γvind(n.v.P;v0;n.a.xs.q.vs;w,u)neP[w/n,u/v]
ne-vind

Here P0 and Ps are the two branch types of Vec-elim.

Normal terms, one group per former. A type A is positive when it is 2, N, an identity type, a vector type, a universe, or a neutral type; that is, when it is neither a Π-type, nor a Σ-type, nor 1.

ΓAnftypeΓ,x:AvnfB
Γλϵ,ϱ(x:A).vnfx:Aϵ,ϱB
nf-lam
ΓvnfAΓwnfB[v/x]
Γ(v,w)nfx:AB
nf-pair
Γnf1
nf-star
Γttnf2
nf-true
Γffnf2
nf-false
Γ0nfN
nf-zero
ΓvnfN
Γsuc(v)nfN
nf-suc
ΓvnfAΓav:AΓbv:A
ΓreflvnfIdA(a,b)
nf-refl
Γn0:N
ΓvnilnfVec(c,n)
nf-vnil
ΓvnnfNΓvanfcΓvxsnfVec(c,vn)Γnsuc(vn):N
Γvcons(vn,va,vxs)nfVec(c,n)
nf-vcons
ΓuneAA positive
ΓunfA
nf-ne

Rule nf-ne is restricted to positive types because Π-η, Σ-η, and 1-η equate a neutral of the excluded types with an expanded form (remark 49.15).

Normal codes are the normal terms whose type is a universe. They have their own rule family, one clause for each universe-closure rule of definition 29.1, definition 29.10, definition 30.1, definition 78.1, because a normal code is a normal term, not a normal type:

ΓKnfU
nf-cd-K
k<
ΓUknfU
nf-cd-univ
ΓcnfUΓ,x:cdnfU
Γx:cϵ,ϱdnfU
nf-cd-pi
ΓcnfUΓ,x:cdnfU
Γx:cdnfU
nf-cd-sg
ΓcnfUΓvnfcΓwnfc
ΓIdc(v,w)nfU
nf-cd-id
ΓcnfUΓvnfN
ΓVec(c,v)nfU
nf-cd-vec
ΓcnfUc stuck
ΓLift(c)nfU+1
nf-cd-lift

with K{1,2,N}. A normal code is stuck when it is neutral, or of the form Vec(,), or of the form Liftk(); these are the three shapes across which the signature moves no lift (remark 111.21). A neutral code is normal by nf-ne, universes being positive.

Normal types:

ΓUnftype
nf-ty-univ
ΓAnftypeΓ,x:ABnftype
Γx:Aϵ,ϱBnftype
nf-ty-pi
ΓAnftypeΓ,x:ABnftype
Γx:ABnftype
nf-ty-sg
ΓKnftype
nf-ty-K
ΓAnftypeΓvnfAΓwnfA
ΓIdA(v,w)nftype
nf-ty-id
ΓcnfUΓvnfN
ΓVec(c,v)nftype
nf-ty-vec
ΓuneU
Γunftype
nf-ty-ne

Lift heads a normal code but never a normal type: by Lift-El a lift is judgmentally the type it lifts, so a normal type never mentions one except inside the code argument of nf-ty-vec, which is the single place where a normal type stores a code rather than a type. The classifier A printed in a neutral or normal judgment need not itself be normal; conversion identifies it with the classifier reconstructed from the stored fields.

Remark 49.15

The type-directedness of definition 49.14 is forced by the three uniqueness rules. A neutral u whose type is a product is not normal; its normal form is the expansion λϵ,ϱ(x:A).uϵ,ϱx, recursively expanded. A neutral at x:AB expands to the pair of its two projections. A term at 1 has normal form whatever it is. The last case is the sharpest: the same raw variable x normalizes to in the context x:1 and to x in the context x:2. A function of the raw term alone cannot choose between those two answers, so normalization must be indexed by the classifier as well.

Lemma 111.26 — Stability of the four judgments

  1. If ΓuneA and ΔΓ, then ΔuneA; likewise for normal terms, normal codes, and normal types.

  2. If ΓuneA then Γu:A; if ΓvnfA then Γv:A; if ΓAnftype then ΓA type.

  3. No expression is neutral in the empty context: there is no u with uneA.

  4. A neutral term is a weak-head normal form, and so is every normal term whose head is a constructor.

Proof of Lemma 111.26 — Stability of the four judgments

Proof. (1) Simultaneous induction on the four derivations. ne-var uses (x:A)ΓΔ; every other rule rebuilds its conclusion from induction hypotheses, and the rules with a judgmental-equality premise (nf-refl, nf-vnil, nf-vcons) use weakening for judgmental equality from definition 26.22. For a binder rule the context extension is applied to a context already extended by the bound variable, which is again a context extension.

(2) Simultaneous induction, replacing each neutral, normal, code, or type rule by the typing rule bearing the same head symbol: ne-app by Π-elim, ne-fst and ne-snd by Σ-elim1,2, ne-ind-bool by 2-elim, ne-ind-nat by N-elim, ne-J by Id-elim, ne-vind by Vec-elim, nf-lam by Π-intro, nf-pair by Σ-intro, nf-refl by Id-intro followed by Conv along the two displayed endpoint equations, nf-vnil and nf-vcons by the two constructor rules of definition 78.1 followed by Conv along the displayed index equation, each nf-cd- rule by the universe-closure rule of the same name in definition 29.1, nf-cd-lift by Lift-U, each nf-ty- rule by the corresponding formation rule, and nf-ty-vec, nf-ty-ne by U-El.

(3) Induction on the neutral derivation. The only axiom is ne-var, whose premise (x:A) is false; every other rule has a neutral premise in the same context.

(4) A weak-head step decomposes its subject as Ha0 with a0 a root redex. Induction on the neutral derivation shows that peeling head contexts off a neutral term always exposes a variable, and a variable is not the left-hand side of any instance of definition 111.20: every instance has a constructor, a λ, a pair, or a nullary type former in the eliminated position. The one production that could stop early is the secondary vind production, whose side condition is met here because ne-vind has a neutral vector argument, which by the induction hypothesis admits no weak-head step. A normal term with a constructor head admits no head context above it other than , and a constructor is not a redex. A normal code headed by Lift admits the production Lift(H), but its argument is stuck by the side condition of nf-cd-lift, and none of Lift-Pi, Lift-Sig, Lift-Id, Lift-K, Lift-Hier applies to a neutral, a Vec code, or another lift. ◻

Exercise 49.9

★☆☆ Compute the η-long normal forms of: (i) λf.f:f:2222; (ii) the variable g in context g:x:2y:22; and (iii) the variable h in context h:f:222. Use only the Π and 2 rules of definition 49.14, and write the answers with the domain annotations and the two binder bits suppressed.

Exercise 49.13

★☆☆ Show that in the base theory Γt:1 for every Γt:1, and exhibit a raw term that has type 1 in one context and type 2 in another with different normal forms. Conclude that no function of the raw term alone can be a sound and complete normalization function: readback must consult the type (remark 49.15).

Three targets

Three different assertions are in play, and a development that runs them together cannot say what its construction has bought. Canonicity is about closed data; normalization produces a canonical representative for open terms; decidable conversion is what the kernel calls. This section fixes the exact statement of each as a target. They are proved, as numbered theorems with their proofs beside them, in section 111.10, once the construction of section 49.5section 111.9 is available.

Definition 49.16 — Normalization structure

A normalization structure for a type theory consists of computable functions from derivations of types and terms into a set of abstract syntax trees with decidable equality, such that two outputs are equal exactly when the represented inputs are judgmentally equal. Thus the functions are invariant on judgmental-equality classes and injective on the resulting quotients. This is the syntax-tree form of definition 48.8.

Convention 111.28 — The normalization package ( )

Write () for the following package at a signature T: a computable nf assigning to each derivation of Γa:A a term, and to each derivation of ΓA type a type, such that

  1. Γnf(a)nfA and Γnf(A)nftype;

  2. Γanf(a):A and ΓAnf(A) type (soundness);

  3. Γab:A if and only if nf(a) and nf(b) are α-equal, and ΓAB type if and only if nf(A) and nf(B) are α-equal (completeness).

A theory satisfying () has a normalization structure (definition 49.16): encode the normal syntax tree.

The three targets, at the signature Timpl of convention 111.16, are the following.

Target C (canonicity). Every closed b:2 is judgmentally equal to exactly one of tt,ff; every closed n:N to sucm(0) for exactly one mN; every closed p:IdA(a,b) forces ab:A and prefla:IdA(a,b); and every closed vector of numeral length m is a vcons chain of length m ending in vnil.

Target N (normalization). Timpl satisfies (), and nf is idempotent.

Target D (decidable conversion). Given derivations of the inputs as in remark 48.7, the judgments ΓAB type and Γab:A are decidable in Timpl; equivalently, Timpl has an effective conversion invariant in the sense of definition 48.8.

Target C is silent about Π, Σ and 1, and deliberately so: at those three formers the corresponding statement is the uniqueness rule itself, holds in every context rather than only in the empty one, and is already available. The interesting canonical-form statements are the ones listed, all at positive types.

Proof structure.

The obstruction is stated in section 111.6: neither an induction on raw syntax nor the closed-instantiation assignment of definition 49.9 survives a binder, because the induction hypothesis for a function must be usable at arguments that do not yet exist. The construction that overcomes it occupies four steps. Section 49.5 builds a domain of semantic values, an evaluator into it, and a type-directed readback; that supplies the candidate function nf but proves nothing about it. Section 111.8 carves out of the domain the values that are semantic types, equips each with a partial equivalence relation on its elements and with a Kripke relation to syntax, and proves the two lemmas—escape and reflection—that connect the two sides. Section 111.9 proves the fundamental lemma: every derivable judgment of Timpl is valid, treated rule family by rule family. Section 111.10 then states and proves Targets N, C and D in that order, and reads the kernel’s four inversion operations off the normal types.

Exercise 49.1

★☆☆ Prove the claim of remark 49.6 directly, without invoking the normalization package (). If x:2xtt:2 were derivable, substitute xff and use Boolean separation. Give the dual substitution that rules out x:2xff:2.

Exercise 49.7

★☆☆ Show that judgmental equality of the base theory is semidecidable without any normalization theorem: enumerate derivations. Why is this useless as an implementation?

Exercise 49.8

★★☆ Suppose a type theory has a recursive signature, effectively checkable rule instances, and decidable judgmental equality. Construct a normalization structure (definition 49.16) for it. Enumerate derivations and map each typed input to the first represented term judged equal to it. Explain why the given input derivation itself guarantees termination; no classical search principle is needed.

Normalization by evaluation for the simply-typed calculus

Normalization by evaluation computes normal forms without ever rewriting syntax: it evaluates the term into a semantic domain in which stuck computations are first-class, then reads back the value as a normal form. We fix the architecture as a definition, then instantiate it in full for λ.

Convention 111.29 — Constructive reading of this section

The STLC construction below is carried out in a constructive type-theoretic metatheory with inductive syntax, dependent function types, and function extensionality for semantic equality proofs. Its functions are programs and its structural recursions terminate by the displayed inductive data; no excluded middle or choice is used. This is what turns evaluation and readback into an algorithm rather than merely a classical set function.

Definition 49.23 — NbE structure

A normalization-by-evaluation structure for a theory with designated normal and neutral forms (definition 49.14) consists of:

  1. a semantic domain: for each context Γ and type A a set [[A]](Γ) of values;

  2. evaluation: an assignment t[[t]], by structural recursion on terms, from terms in context Γ and environments ρ[[Γ]](Δ) to values, such that judgmentally equal terms evaluate to equal values;

  3. reflection from neutral forms to values and reification from values to normal forms, together with a distinguished environment ρΓ of reflected variables;

such that the composite nf(t):=([[t]]ρΓ),RawTm [[]]ρΓ [[A]]  NfRawTm, lands in normal forms of the correct type and satisfies Γtnf(t):A. If tu:A, evaluation gives equal semantic values and reification gives nf(t)=nf(u); call this equality preservation. Conversely, tnf(t):A and unf(u):A, so equal readbacks imply tu:A; call this equality reflection. Together they make comparison of normal forms a sound and complete decision procedure, without assigning the two words to opposite directions in isolation.

We build such a structure for the simply-typed λ-calculus λ of chapter 2 over a single base type ι with no constants; types are T::=ιST, with βη-equality Γts:T. Normal and neutral forms specialize definition 49.14: neutrals are variables applied to normal arguments, and nf-ne is available only at ι. We write ΔΓ when Δ extends Γ on the right, i.e. Δ=Γ,Γ; neutral and normal forms weaken along such extensions by lemma 2.14.

Three failures determine the semantic domain. If the ground type has no constants, the closed-only choice [[ι]]()= cannot interpret the open judgment x:ιx:ι. If semantic functions are only closures, then for f:ST the application fa is stuck rather than a semantic value; it must be reflected as aT(fS(a)). Finally, reifying a semantic g:ST requires a fresh variable: ΓST(g)=λ(x:S).Γ,x:ST(gΓ,x:S(Γ,x:SS(x))). The right side lives in the extended context Γ,x:S; hence a value at Γ must act uniformly at every extension ΔΓ. Neutrals, reflection, and the Kripke index below are forced by these three failures.

Definition 49.24 — Kripke domain

By recursion on the type: [[ι]](Γ):={uΓuneι}[[ST]](Γ):=ΔΓ([[S]](Δ)[[T]](Δ)) For ΔΓ, the restriction aΔ[[T]](Δ) of a[[T]](Γ) is weakening of the neutral term at ι, and restriction of the indexing family at ST: (fΔ)Θ:=fΘ. Environments: [[Γ]](Δ):=(x:T)Γ[[T]](Δ), with pointwise restriction.

Definition 49.25 — Reflection, reification, evaluation

By recursion on the type, define ΓT:{uΓuneT}[[T]](Γ) and ΓT:[[T]](Γ){vΓvnfT}: Γι(u):=uΓST(u)Δ(a):=ΔT(u ΔS(a))Γι(u):=uΓST(f):=λ(x:S).Γ,x:ST(fΓ,x:S(Γ,x:SS(x)))(x fresh) (in the reflection clause u is silently weakened to Δ). Evaluation [[t]]ρ[[T]](Δ) for Γt:T and ρ[[Γ]](Δ), by structural recursion: [[x]]ρ:=ρ(x),[[rs]]ρ:=([[r]]ρ)Δ([[s]]ρ),([[λx.t]]ρ)Θ(a):=[[t]](ρΘ,xa). The identity environment ρΓ[[Γ]](Γ) is ρΓ(x):=ΓT(x) for (x:T)Γ, and nfΓT(t):=ΓT([[t]]ρΓ).

Example 111.33

Let Γ=(f:ιι). Then [[f]]ρΓ=Γιι(f), the family af ι(a)=fa of neutral applications, so nf(f)=λ(x:ι).ι(fx)=λ(x:ι).fx, the η-expansion — which no rewriting procedure oriented left-to-right would produce. Likewise [[(λy.y)f]]ρΓ=[[f]]ρΓ already in the domain, so nf((λy.y)f)=λ(x:ι).fx: the β-redex vanishes during evaluation, not by rewriting.

Two structural lemmas connect evaluation with the Kripke action.

Lemma 49.27 — Restriction

Let Γ and Δ be λ contexts, let Γt:T, and let ρ[[Γ]](Δ). For every context ΘΔ, [[t]](ρΘ)=([[t]]ρ)Θin [[T]](Θ). For ΞΘΔ, restriction satisfies (a|Θ)|Ξ=a|Ξ and a|Δ=a for every a[[T]](Δ).

Proof of Lemma 49.27 — Restriction

Proof. Induct on t, simultaneously with its type. A variable is the corresponding environment projection, so the equation is the definition of restricted environment. Application follows by the two induction hypotheses and the Kripke action of a semantic function. For abstraction, extensionality reduces the claim at every further extension ΞΘ and semantic argument a to the induction hypothesis for the body in the extended environment (ρ|Ξ,a). Identities and composites of restrictions are componentwise identities and composites on environments; induction on the semantic type proves the same equations for semantic values. ◻

Lemma 49.28 — Evaluation and substitution

Let Γ and Δ be λ contexts, let S,T be λ types, let Γ,x:St:T and Γs:S, and let ρ[[Γ]](Δ). Then [[t[s/x]]]ρ=[[t]](ρ,x[[s]]ρ)in [[T]](Δ).

Proof of Lemma 49.28 — Evaluation and substitution

Proof. Induct on t. At x both sides are [[s]]ρ; at another variable both are the same component of ρ. Application is immediate from the two induction hypotheses. Under λy, choose y fresh for s; semantic extensionality reduces the equality to the induction hypothesis for the body in (ρ,ya). Capture avoidance gives (t0[s/x])[a/y]=t0[a/y][s/x], so the two extended environments coincide. These cases exhaust the term grammar. ◻

Theorem 49.29 — Completeness of NbE for

If Γtt:T, then [[t]]ρ=[[t]]ρ for every environment ρ; consequently nfΓT(t)=nfΓT(t).

Proof of Theorem 49.29 — Completeness of NbE for

Proof. Induction on the derivation of the equality judgment.

β: [[(λx.t)s]]ρ=evaluation[[t]](ρΔ,x[[s]]ρ)=lemma49.28[[t[s/x]]]ρ, where restriction along ΔΔ is the identity.

η: for ΘΔ and a, ([[λx.tx]]ρ)Θ(a)=evaluation([[t]](ρΘ))Θ(a)=lemma49.27(([[t]]ρ)Θ)Θ(a)=restrictionatfunctiontype([[t]]ρ)Θ(a). Thus the semantic families are equal.

Congruences, equivalence rules: pointwise from the induction hypotheses, and by reflexivity, symmetry, transitivity of meta-level equality. ◻

Soundness requires relating values back to terms. The relation is a Kripke logical relation: a family of relations indexed by types and stable under context extension.

Definition 49.30 — Kripke logical relation

For Γt:T and a[[T]](Γ) define Γta:T by recursion on T:

  • Γtu:ι iff Γtu:ι (recall u is a neutral term);

  • Γtf:ST iff for all ΔΓ and all s,a with Δsa:S, we have ΔtsfΔ(a):T.

The relation is closed under judgmental equality on the left and under restriction on the right: if Γtt:T and Γta:T then Γta:T; if ΔΓ then ΔtaΔ:T. For the base type the first claim is transitivity of judgmental equality and the second is weakening. At ST, apply the induction hypotheses at T after quantifying over a further extension and an argument related at S; the restriction claim uses functoriality of the Kripke family. This induction on T proves both closure properties simultaneously.

Lemma 49.31 — Adequacy

By mutual induction on T:

  1. if Γta:T, then ΓtΓT(a):T;

  2. if Γtu:T with ΓuneT, then ΓtΓT(u):T.

Proof of Lemma 49.31 — Adequacy

Proof. At ι both parts are the definitions, since reflection and reification are identities there.

At ST, (a): let Γtf, and let x be fresh. By (b) at S (a smaller type), Γ,x:SxS(x):S; hence by the definition of the relation, Γ,x:StxfΓ,x:S(S(x)). By (a) at T, Γ,x:StxT(fΓ,x:S(S(x))):T. The ξ-congruence and η then give Γtλx.:ST, and the right-hand side is precisely ΓST(f).

(b): let Γtu:ST with u neutral, and let ΔΓ, Δsa:S. By (a) at S, ΔsΔS(a):S, so by congruence Δtsu ΔS(a):T, the right side a neutral (ne-app, u weakened). By (b) at T, ΔtsΔT(u ΔS(a))=ΓST(u)Δ(a), as required. ◻

Lemma 49.32 — Fundamental lemma for

Let Γt:T, and let γ be a substitution and ρ an environment with Δγ(x)ρ(x):S for every (x:S)Γ. Then Δt[γ][[t]]ρ:T.

Proof of Lemma 49.32 — Fundamental lemma for

Proof. Induction on the typing derivation. Variables are the hypothesis. Application combines the induction hypotheses with the definition of the relation at ST (taking ΔΔ). For abstraction: given ΘΔ and Θsa:S, the induction hypothesis for the body at the extended substitution and environment (restricted along Θ, using closure under restriction) gives Θt[γ,s/x][[t]](ρΘ,xa); since Θ(λx.t[γ])st[γ,s/x]:T by β, closure of the relation under judgmental equality concludes. ◻

Theorem 49.33 — Soundness of NbE for

ΓtnfΓT(t):T for every Γt:T.

Proof of Theorem 49.33 — Soundness of NbE for

Proof. By lemma 49.31(b) with t=u=x, the identity substitution and the identity environment are related: ΓxρΓ(x):S for each (x:S)Γ. By lemma 49.32, Γt[[t]]ρΓ:T; by lemma 49.31(a), ΓtΓT([[t]]ρΓ):T, which is the claim. ◻

Corollary 49.34

βη-equality of λ is decidable, and nfΓT constitutes a normalization structure (definition 49.16) for λ.

Proof of Corollary 49.34

Proof. theorem 49.29, theorem 49.33 give completeness and soundness; injectivity into syntax trees follows: equal terms have equal normal forms, and terms with equal normal forms are equal via theorem 49.33. Computability of nf holds because every clause of definition 49.24, definition 49.25 is a structural program under convention 111.29. ◻

Remark 111.42 — Effectivity for

The function type [[ST]] lives in the constructive metatheory of convention 111.29. Evaluation represents its definable elements by finite closures containing a term body and an environment, and application runs a closure. Reification recurses on the finite object-language type, so normalization terminates on every typed input. A first-order implementation may defunctionalize those closures or use an untyped value domain with de Bruijn levels as in section 49.5; this changes the representation, not the effectivity claim. The algebraic formulation likewise uses only constructive metatheory.

Exercise 49.10

★★★ Prove lemma 49.27, lemma 49.28 and the two closure properties asserted in definition 49.30. Compare lemma 49.28 clause by clause with lemma 49.11: the computability assignment of section 49.2 is an evaluation.

Exercise 49.11

★★★ Show that nfΓT(v)=v for every ΓvnfT, by mutual induction with the statement [[u]]ρΓ=ΓT(u) for ΓuneT. Conclude that normal forms are canonical representatives: each judgmental equality class contains exactly one normal form.

Exercise 49.12

★★★ Extend definition 49.24, definition 49.25 to λ with 2 and its non-dependent recursor: take [[2]](Γ):={tt,ff}{uΓune2}, define the semantic recursor by cases, and verify the two computation-rule cases in the proof of theorem 49.29.

Two failed normalizers

The simply-typed construction of section 49.4 is complete, and the temptation is to replay it one step at a time. Two plausible first attempts are written out here, because each failure fixes a feature of the construction that follows.

First attempt: rewrite, then expand.

The first strategy a reader is likely to try is the one that works for untyped β-reduction: contract redexes until none remains, then η-expand the result. Write rw for that two-phase procedure. Three separate things go wrong, and only the first is the expected one.

The termination of the rewriting phase is the theorem being proved, so rw cannot be used to prove it. That objection is familiar and by itself would leave the design intact.

The second failure is fatal to the phase separation. Expanding after rewriting requires knowing, for each subterm, whether its type is a Π-type, and the type is itself a term that must be computed first. In the context Γ0:=(X:U0, n:N),T:=indN(x.U0; 2, λk.λr.2r, n), the type T is a Π-type when n is a positive numeral and 2 when n is 0; at suc(suc(0)) it is a Π-type of arity two. A variable f:T must be expanded to λ(y1:2).λ(y2:2).fy1y2 in the third case and left alone in the first, and rw can learn which only by running the same computation on the type. So the expansion phase is not after the rewriting phase; it is interleaved with it.

The third failure kills the expansion phase outright. At 1, rule 1-η is not an expansion: it replaces every term by . In Γ0,u:1 the raw variable u must normalize to , while in Γ0,u:2 the same raw variable must normalize to u. No function of the raw term alone returns both answers, so rw cannot even be given the right type. What survives is: computation and η must be performed by one operation, and that operation must receive the type.

Second attempt: induction on the typing derivation.

Repair the interface, then, and define a normal form N(D) by structural induction on a derivation D of Γa:A, in the hope of proving ΓN(D)nfA and ΓaN(D):A at the same time. The constructor cases go through. The application case does not. Its premises give ΓN(Df)nfx:Aϵ,ϱB,ΓN(Da)nfA, and by nf-lam the first is λϵ,ϱ(x:A).v for some normal v. The normal form of fϵ,ϱa should then be the normal form of v[N(Da)/x]—but that expression is not a subderivation of D, and it is not smaller in any measure the induction has. Substituting a normal term into a normal term creates new redexes, which is precisely the phenomenon the theorem is about.

The repair is the one already used twice in this book, in section 49.2 and in definition 49.30: do not induct on the derivation for the conclusion you want; induct on the type for a stronger, hereditary statement, and derive the conclusion. The statement must, however, be strong enough in two directions that the elementary assignment of definition 49.9 is not.

First, it must be indexed by a context and stable under extending it. The assignment () evaluates a term at a closing instantiation, and Γ contains only closed terms. Under nf-lam the body must be normalized in Γ,x:A, where no closing instantiation for x exists and none can be manufactured: in Timpl the type A may be a variable of U0, which has no closed inhabitant at all. Hence the predicate is indexed by ΔΓ and its evidence restricts along extensions, exactly as [[ST]] was in definition 49.24.

The type index cannot be a syntactic type. In the failed first attempt the classifier T had to be computed before its shape was visible; so the recursion must be on the value of the type, computed by the same evaluator that computes values of terms. Together with stability under context extension and the strict universes, this forces a semantic type to carry three pieces of data at once: a value that classifies computation, a ranked element relation, and restriction maps along context embeddings. A plain value, a plain predicate, or a family without restriction maps loses one of these three requirements.

Values, evaluation, and readback for the kernel signature

Both failures of section 111.6 asked for the same thing: one operation that computes and η-expands together, directed by the value of the classifier. This section builds the operation. It is an algorithm and nothing more; not one of its clauses is justified until section 111.9.

Definition 49.36 — Untyped value domain

Use finite closures rather than a mixed-variance domain equation. Values, neutral values, environments, and closures are the least mutually inductive sets generated below. An environment is a finite list of values. A closure of arity r is either ρ;x1,,xr.borliftclλ(χ)orstepcl1(F)orstepcl2(F,d), where b is raw syntax, ρ is an environment, and χ has arity r. The second form is used only for the codomain of a lifted type former; the last two are the finite closure tags for the derived natural-step type. Thus closures contain syntax and finite data; they do not contain set-theoretic functions. Dd,e,A,C::=lamϵ,ϱ(χ)etaϵ,ϱ(k;A;χ)::=pair(d,e)^tt^ff^::=0^suc^(d)refl^(d)::=vnil^vcons^(d,e,d)::=Π^ϵ,ϱ(A,F)Σ^(A,F)1^2^N^::=Id^(A,d,e)Vec^(C,d)::=U^λLift^λ(C)upA(k),Dnek::=xmappϵ,ϱ(k;A;d)::=fst(k)snd(k)::=ind2^(F;dt;df;k)indN^(F;d0;ds;k)::=J^(ϑ;k)::=vind^(V;ς;dm;k). In Π^, Σ^ and in the two inductive eliminator nodes, F is an arity-one closure; in J^, F has arity three and g arity one; in vind^, F has arity two and G arity four, matching the binders in convention 111.16. Closure execution is the least relation χ@(d1,,dr)e with rules

ρ,d1,,drbe
ρ;x1,,xr.b@(d1,,dr)e
Clos-Raw
χ@delift^λ(e)=e
liftclλ(χ)@de
Clos-Lift
F@dC
stepcl1(F)@dΠ^exp,runtime(C,stepcl2(F,d))
Clos-Step-1
F@suc^(d)C
stepcl2(F,d)@eC
Clos-Step-2

The evaluation, semantic-operation, and reflection judgments used in these premises are printed in definition 111.44, definition 111.45, definition 49.37. The four definitions are one simultaneous least graph; the forward presentation only keeps the clause tables readable. It is positive: every recursive occurrence is a premise of a rule, never the domain of a stored function. When the graph has the unique output e, write χ(d)=e.

The grammar just displayed is the raw representation. Mathematically, identify two raw values when no finite execution context built from these graph rules and ending in a constructor or neutral readback distinguishes them. This contextual equivalence is, by its definition, an equivalence and a congruence for every displayed constructor and graph rule; its quotient is a set because the raw grammar is a set. In particular, ρ;x.b[γ] and [[γ]]ρ;x.b have the same execution behavior, by rule induction. Below D denotes this quotient. An implementation keeps the finite representatives; the quotient is used only to state substitution and weakening without choosing a closure representation.

To keep the displays below readable, abbreviate the two parameter blocks that never change during an elimination: ϑ:=(A;F;g;da;db),ς:=(F;d0;G), A stuck identity node is then written J^(ϑ;k) and a stuck vector node vind^(V;ς;dm;k).

The field V is the semantic vector type stored in the up node of the neutral principal argument. It is the only place from which readback can recover the element code, and definition 111.44 is arranged so that it is always available there.

The subscript m of xm is a de Bruijn level. The subscripts λ on U^λ and Lift^λ are canonical symbolic level normal forms from definition 111.18; no assignment to an external level parameter is stored in a value.

Definition 111.44 — Semantic operations

Application, projection, the four eliminators, and lifting act on values as follows. The equations present the clauses of least evaluation graphs; a case not listed has no derivation. In particular, they do not assert total set functions on arbitrary values. lamϵ,ϱ(χ)ϵ,ϱd:=e(χ@de),etaϵ,ϱ(k;A;F)ϵ,ϱd:=F(d)(appϵ,ϱ(k;A;d)),upΠ^ϵ,ϱ(A,F)(k)ϵ,ϱd:=upF(d)(appϵ,ϱ(k;A;d)),fstv(pair(d,e)):=d,fstv(upΣ^(A,F)(k)):=upA(fst(k)),sndv(pair(d,e)):=e,sndv(upΣ^(A,F)(k)):=upF(d1)(snd(k)),:=d1:=upA(fst(k)). ifv(F;dt;df;tt^):=dt,ifv(F;dt;df;ff^):=df,ifv(F;dt;df;up2^(k)):=upF(up2^(k))(ind2^(F;dt;df;k)),recv(F;d0;ds;0^):=d0,recv(F;d0;ds;suc^(d)):=dsdrecv(F;d0;ds;d),recv(F;d0;ds;upN^(k)):=upF(upN^(k))(indN^(F;d0;ds;k)),jv(ϑ;refl^(d)):=g(d),jv(ϑ;upI(k)):=upF(da,db,upI(k))(J^(ϑ;k)). The two applications in the suc^ clause are exp,runtime, because StepN(C) of definition 28.21 is the explicit, runtime-relevant product in Timpl. The vector eliminator takes its motive F of two arguments and its successor branch G of four, and inspects its vector argument first: vrv(ς;dm;upV(k)):=upF(dm,upV(k))(vind^(V;ς;dm;k)),vrv(ς;0^;vnil^):=d0,vrv(ς;suc^(m);vcons^(m,a,xs)):=G(m, a, xs, vrv(ς;m;xs)). Only the first clause builds a stuck node, and it is reached only when the vector value is neutral, in which case that value carries its own semantic type V; no external argument is needed. A stuck node whose index is neutral while its vector is a constructor never arises on a well-typed input, because the element relation at a vector type of neutral length contains only neutral values (definition 111.58); on any other input no rule applies. Lifting is lift^λ(K):=K(K{1^,2^,N^}),lift^λ(U^μ):=U^μ,lift^λ(Π^ϵ,ϱ(A,F)):=Π^ϵ,ϱ(lift^λA, liftclλ(F)),lift^λ(Σ^(A,F)):=Σ^(lift^λA, liftclλ(F)),lift^λ(Id^(A,d,e)):=Id^(lift^λA,d,e),lift^λ(C):=Lift^λ(C), in the three remaining cases C=Vec^(,), C=Lift^j(), and C=upU^j(). These are exactly the five contraction instances of definition 111.20 together with the two stuck shapes of remark 111.21.

Definition 111.45 — Evaluation

An environment is a finite list ρ of values. The judgment ρad is the least evaluation relation generated by the following clauses together with the closure-execution and semantic- operation clauses of definition 49.36, definition 111.44. We write [[a]]ρ=d only when a derivation of that judgment has been fixed. No clause consults a typing derivation. [[xj]]ρ:=ρ(j),[[U]]ρ:=U^,[[Lift(a)]]ρ:=lift^([[a]]ρ),[[1]]ρ:=1^,[[2]]ρ:=2^,[[N]]ρ:=N^,[[]]ρ:=^,[[tt]]ρ:=tt^,[[ff]]ρ:=ff^,[[0]]ρ:=0^,[[suc(a)]]ρ:=suc^([[a]]ρ),[[refla]]ρ:=refl^([[a]]ρ), [[x:Aϵ,ϱB]]ρ:=Π^ϵ,ϱ([[A]]ρ,ρ;x.B),[[x:AB]]ρ:=Σ^([[A]]ρ,ρ;x.B),[[λϵ,ϱ(x:A).b]]ρ:=lamϵ,ϱ(ρ;x.b),[[aϵ,ϱb]]ρ:=[[a]]ρϵ,ϱ[[b]]ρ,[[(a,b)]]ρ:=pair([[a]]ρ,[[b]]ρ),[[pr1(a)]]ρ:=fstv([[a]]ρ),[[pr2(a)]]ρ:=sndv([[a]]ρ),[[IdA(a,b)]]ρ:=Id^([[A]]ρ,[[a]]ρ,[[b]]ρ),[[Vec(A,n)]]ρ:=Vec^([[A]]ρ,[[n]]ρ),[[vnil]]ρ:=vnil^,[[vcons(n,a,xs)]]ρ:=vcons^([[n]]ρ,[[a]]ρ,[[xs]]ρ). The four eliminators evaluate to the corresponding semantic operation. Each motive and each multiple binder becomes a finite closure of the displayed arity: [[ind2(x.C;ct,cf,b)]]ρ:=ifv(ρ;x.C; [[ct]]ρ; [[cf]]ρ; [[b]]ρ),[[indN(x.C;c0,cs,m)]]ρ:=recv(ρ;x.C; [[c0]]ρ; [[cs]]ρ; [[m]]ρ),[[JA;a;b(x.y.p.C;z.c;q)]]ρ:=jv(ϑρ; [[q]]ρ),[[vind(M;p0;S;m,ys)]]ρ:=vrv(ςρ; [[m]]ρ; [[ys]]ρ), where the two parameter blocks are ϑρ:=([[A]]ρ; FC; gc; [[a]]ρ; [[b]]ρ),ςρ:=(FP; [[p0]]ρ; Gps),FC:=ρ;x,y,p.C,gc:=ρ;z.c,FP:=ρ;m,ys.P,Gps:=ρ;m,a,xs,ih.ps.

The graphs are deterministic. Simultaneous rule induction on evaluation, closure execution, and the semantic-operation graphs proves that two derivations with the same inputs have the same final constructor and then the same output by their induction hypotheses. They are intentionally partial on raw input. Their definedness on every well-typed input is proved by lemma 111.74, not assumed in this definition. Readback runs in the other direction and is indexed by a de Bruijn level n, the number of variables already introduced.

Definition 49.37 — Type-directed readback

Fix a context Δ=(x0:A0,,xn1:An1) and read the level xm as the variable xm. Reflection, reification, type quotation, code quotation, and neutral readback are the least mutually inductive graphs generated by the following clauses. Recursive calls in an equation are premises of its graph rule; the display does not assert a total recursive function on arbitrary values. Write vnA:=A(xn) for the unique output when that graph is defined. Definedness and uniqueness on related inputs are proved in lemma 111.63.

Reflection η-expands at the three uniqueness formers and stops elsewhere: Π^ϵ,ϱ(A,F)(k):=etaϵ,ϱ(k;A;F),Σ^(A,F)(k):=pair(d1, F(d1)(snd(k))),d1:=A(fst(k)),1^(k):=^,A(k):=upA(k)for every other head A. Reification is the mirror image: Π^ϵ,ϱ(A,F)n(d):=λϵ,ϱ(xn:Qn(A)).F(vnA)n+1(dϵ,ϱvnA),Σ^(A,F)n(d):=(An(d1),F(d1)n(sndv(d))),d1:=fstv(d),1^n(d):=,2^n(tt^):=tt,2^n(ff^):=ff,N^n(0^):=0,N^n(suc^(d)):=suc(N^n(d)),Id^(A,da,db)n(refl^(d)):=reflAn(d),Vec^(C,dm)n(vnil^):=vnil,Vec^(C,dm)n(vcons^(m,a,xs)):=vcons(N^n(m), Cn(a), Vec^(C,m)n(xs)),U^in(C):=Qnc(C),An(upB(k)):=Rn(k)for A positive. Every annotation the output stores—the λ-domain, the refl argument, the vcons index—is itself produced by Qn or n, never copied from the input. That is what makes an α-comparison of outputs meaningful: two judgmentally equal inputs whose annotations differ, such as λ(x:Lift0N).x and λ(x:N).x, receive the same normal form because both domains are requoted from the same semantic value.

Type quotation deletes lifts, because Lift-El makes LiftA the type A; code quotation keeps them: Qn(Lift^λ(C)):=Qn(C),Qnc(Lift^λ(C)):=Liftλ(Qnc(C)),Qn(U^λ):=Uλ,Qnc(U^λ):=Uλ,Qn(K):=K,Qnc(K):=K(K{1,2,N}),Qn(upU^i(k)):=Rn(k),Qnc(upU^i(k)):=Rn(k), and on the four structured heads both operations descend, writing Q uniformly for either of them: Qn(Π^ϵ,ϱ(A,F)):=xn:Qn(A)ϵ,ϱQn+1(F(vnA)),Qn(Σ^(A,F)):=xn:Qn(A)Qn+1(F(vnA)),Qn(Id^(A,d,e)):=IdQn(A)(An(d),An(e)),Qn(Vec^(C,d)):=Vec(Qnc(C), N^n(d)). The vector clause uses Qc in both readings, which is what remark 111.21 forces: the element of a vector type is a code, and no equation moves a lift across Vec.

Neutral readback rebuilds the syntactic elimination, reading back the principal argument and reifying every stored argument at the semantic type under which it was stored: Rn(xm):=xm,Rn(appϵ,ϱ(k;A;d)):=Rn(k)ϵ,ϱAn(d),Rn(fst(k)):=pr1(Rn(k)),Rn(snd(k)):=pr2(Rn(k)), Rn(ind2^(F;dt;df;k)):=ind2(xn.Qn+1(F(vn2^));:=F(tt^)n(dt), F(ff^)n(df), Rn(k)),Rn(indN^(F;d0;ds;k)):=indN(xn.Qn+1(F(vnN^));:=F(0^)n(d0), S(F)n(ds), Rn(k)),Rn(J^(ϑ;k)):=JQn(A);va;vb(MJ; SJ; Rn(k)),va:=An(da),vb:=An(db),MJ:=xn.xn+1.xn+2.Qn+3(F(w0,w1,w2)),SJ:=xn.F(w,w,refl^(w))n+1(g(w)), with w:=vnA, with w0,w1 the reflected variables of A at levels n,n+1 and w2:=vn+2Id^(A,w0,w1), and with the semantic value of StepN given by S(F):=Π^exp,runtime(N^,stepcl1(F)). Finally, for V=Vec^(C,d), Rn(vind^(V;ς;dm;k)):=vind(Mv; v0; Sv; N^n(dm), Rn(k)),Mv:=xn.xn+1.Qn+2(F(a1,a2)),v0:=F(0^,vnil^)n(d0),Sv:=xn.xn+1.xn+2.xn+3.Fsn+4(G(b1,b2,b3,b4)),Fs:=F(suc^(b1),vcons^(b1,b2,b3)), where a1:=vnN^, a2:=vn+1Vec^(C,a1), b1:=vnN^, b2:=vn+1C, b3:=vn+2Vec^(C,b1) and b4:=vn+3F(b1,b3). The element code C is read off the stored V; it is the only field of the node that does not also occur as an argument of vrv.

The identity environment of Δ is ρΔ:=([[A0]]ρ0(x0),), formed left to right so that ρj is the prefix already built, and nfΔA(a):=[[A]]ρΔ|Δ|([[a]]ρΔ),nfΔ(A):=Q|Δ|([[A]]ρΔ).

The level parameter of readback is not inert. Extending a context changes the fresh levels chosen under every binder, so the required weakening lemma must transport the readback graphs as well as the typing judgment.

Definition 111.47 — Telescope-indexed semantic substitutions

A semantic telescope is built by Ψ::=Ψ.A, where A may depend on the values assigned to the declarations of Ψ. Its length is |Ψ|. A semantic value, closure, environment, or ranked witness is Ψ-admissible when every free neutral level belongs to the initial segment j<|Ψ|, every such occurrence carries the classifier supplied by the jth declaration of Ψ, and every stored raw closure is closed by its displayed environment. Admissibility is formation data: every ranked construction below is defined relative to a displayed initial telescope Ψ. We do not first form an object with sparse levels and then compress those levels. Passage to a larger initial segment is an explicit typed target weakening, and passage through a binder is one of the typed extensions below. Thus no unclassified intermediate level is formed.

Write DΨD for the set of Ψ-admissible values. When the ranked relations are introduced in definition 111.58, their membership judgment will have the support-explicit form η:(d,e)EltΨ(α). It is formable only when α is formed at Ψ, when d,eDΨ, and when the membership derivation η is itself Ψ-admissible. Consequently membership at Ψ can never certify a value containing the fresh level |Ψ|; that value first belongs to the explicitly extended target world.

A semantic substitution σ:ΨΦ assigns a semantic value in DΦ to every declaration of the source telescope Ψ. Its typing witnesses, once the ranked relations have been constructed, require the jth assigned value to belong to the support-Φ element relation of the jth classifier after the preceding assignments. The untyped action graph on D is determined by replacing level j by that value and then executing every semantic operation. Thus a substituted neutral may compute. Closures are acted on through their stored environments.

One special action must remain distinct. If ω:ΨΦ is an iterated typed target weakening and kDne is neutral syntax, then ωk denotes the induced structural neutral weakening: it fixes each old level j<|Ψ| and recursively transports the stored semantic fields. It is not the action of an arbitrary semantic substitution on a bare neutral. The equivariance equations below relate structural neutral weakening to the semantic action on reflected values. In particular ωk remains in Dne, so neutral readback at the target length is well formed.

The four operations below have different types and will not be denoted by one operation.

  1. If σ:ΨΦ, eDΦ, and e has the transported classifier σA at Φ, then (σ,e):Ψ.AΦ is arbitrary source extension.

  2. If Φ.B is well formed, the weakening substitution wkΦ,B:ΦΦ.B sends each old declaration to its weakened semantic value. Hence wkσ:ΨΦ.B is target weakening.

  3. Put B:=σA and vΦ,A:=(wkσ)A(x|Φ|). The canonical lift is σ:=(wkσ,vΦ,A):Ψ.AΦ.B. Here wkΦ,B:ΦΦ.B, whereas (wkσ)A is a classifier over Φ.B. It classifies the displayed fresh reflection, not the target declaration and not the bare neutral x|Φ|.

  4. If τ:ΦΞ, composition acts componentwise and arbitrary extension satisfies the typed equation τ(σ,e)=(τσ,τe):Ψ.AΞ. Target weakening satisfies (wkτ)σ=wk(τσ), and canonical lifts satisfy τσ=(τσ):Ψ.AΞ.((τσ)A), where τ:Φ.(σA)Ξ.(τσA).

The identity is defined recursively: id:=(),idΨ.A:=(wkidΨ,wkA(x|Ψ|)). For a syntactic weakening ω:ΔΔ, the corresponding semantic substitution is the iterated target weakening; write ωa and ωJ for raw weakening and its action on a judgment. General semantic substitution has a raw action only when paired with a realizing raw substitution in definition 111.68. Action on ranked relation evidence requires the typed relational witness of definition 111.57.

Lemma 111.48 — Substitution and renaming equivariance

Let σ:ΨΦ and let all displayed inputs be Ψ-admissible. The following maps are defined and satisfy the displayed equations.

  1. Evaluation, closure execution, application, projections, the four eliminators, and semantic lifting commute with σ; for example,

    σ(χ@de):(σχ)@(σd)σe. Moreover id=id, (τσ)=τσ. Closure execution under an instantiated source binder uses (σ,e) and equation 111.2; readback under a fresh target binder uses σ and equation 111.1.

  2. Let ω:ΨΦ be an iterated typed target weakening and put n=|Ψ|, n=|Φ|. Reflection, reification, type quotation, code quotation, and neutral readback are equivariant: ωA(k)=ωA(ωk),ωAn(d)=αωAn(ωd),ωQn(A)=αQn(ωA),ωQnc(C)=αQnc(ωC),ωRn(k)=αRn(ωk).

  3. If the same ω is induced by a syntactic weakening ΔΔ and J is any typing, type-equality, term-equality, neutral, normal-term, normal-type, or normal-code judgment, then ωJ is derivable in the target world. Its type is the right-hand quotation in (2), not the untransported quotation at depth n.

Proof of Lemma 111.48 — Substitution and renaming equivariance

Proof. Prove (1) by simultaneous induction on the displayed graph. The variable case is the defining equation for σ. A closure uses the induction hypothesis for its environment. An instantiated source binder uses equation 111.2; a fresh target binder uses the canonical lift of equation 111.1. The composition equations follow by a second induction on the same graph. In particular, target gap variables may occur in the substituted value e and are retained on both sides.

For (2)–(3), specialize to iterated target weakening ω. A raw closure uses the induction hypothesis for its environment and uses ω across each binder; Clos-Lift, Clos-Step-1, and Clos-Step-2 then commute with the corresponding semantic operation. Application and both projections use their immediate induction hypotheses. Boolean and natural elimination use the motive and branch hypotheses and preserve the constructor or stuck choice. Identity elimination transports the carrier, motive, branch, two endpoints, and principal neutral. Vector elimination transports its stored vector type, motive, base, successor method, index, and principal neutral. These are all semantic-operation rule families.

For (2), induction on the readback graph treats a binder by ω; hence its freshly reflected value at the source classifier is sent to the freshly reflected value at the target classifier. The Π and Σ clauses therefore give alpha-equal binders and the induction hypothesis gives their dependent bodies. Identity and vector clauses use the reification and code- quotation hypotheses for every stored component. Each neutral eliminator uses the corresponding complete list from the preceding paragraph. The remaining clauses have no binder and follow structurally.

Finally weakening, alpha-conversion, and the equations of (2) prove (3), rule by rule for the seven named judgment forms. ◻

Remark 49.35 — Effectivity

Every object in definition 49.36 is finite first-order data. Raw closures store a body and an environment; the other three closure tags perform the displayed lift and natural-step operations. Execution, evaluation, semantic operations, and readback are inductive graphs. Determinism is a simultaneous induction on their derivations. The finitely many multi-arity and derived tags are required by the Timpl binders.

That finite representation does not by itself prove definedness. Applying a raw closure runs an arbitrary body, and readback at Π^(A,F) calls F on a freshly reflected variable, so neither the value nor the level n decreases. What does decrease is the ranked derivation of semantic typehood: every recursive call of , , Qn and Qnc is at a semantic type named by a premise of the generator just used, and those premises are ordered by a well-founded multiset of symbolic-level heights followed by the Hessenberg sum of derivation ranks. The semantic-type construction below verifies strict descent for every clause. Neutral readback is the exception: it recurses on the structure of its neutral argument and reifies stored components at stored types that are not controlled by any ambient type. Definedness of Rn on the neutral values that actually occur is therefore not assumed but proved, at the point where each such value is built, in lemma 111.74; it is exactly membership in the readback-defined field KΨ, equivalently self-relatedness under Ψne, of definition 111.52. Totality of nf on well-typed input is thus a theorem (theorem 111.76), not a property of the program text.

Example 111.50 — Three readbacks

Let Δ0:=(X:U0, f:XX, u:1), so |Δ0|=3 and, writing X:=upU^0(x0), ρΔ0=(X, Π^(X,(X);x.X)(x1), ^). Then nfΔ0XX(f)=λϵ,ϱ(x3:X).fϵ,ϱx3,nfΔ01(u)=,nfΔ0(Lift0(X))=X. The first is η-expansion produced by reflection, not by a rewriting step; the second is the collapse that defeated rw in section 111.6, and it happens because 1^ returns ^ before the variable is ever stored; the third deletes a lift because Qn does, while nfΔ0U1(Lift0(X))=Lift0(X) keeps it, since the same value is read back there by Qnc.

Exercise 49.14

★★★ Reconstruct the Σ clauses of definition 49.36, definition 111.44, definition 111.45, definition 49.37 from the single requirement that readback be η-long: the values pair(d,d) and Σ^(A,F), the two semantic projections on a pair and on a neutral, the evaluation clauses, the reflection clause, and the reification clause Σ^(A,F)(d)=(A(d1),F(d1)(d2)), where d1,d2 are the semantic projections of d. Then check both β-rules on a constructor pair and Σ-η on a reflected neutral.

Semantic types

Not every value is a type, and the values that are types must carry the data that readback consumes. Remark 49.10 already named the danger: if “A is a semantic type” were a mere property, a value could be a type in two ways and the recursion assigning it a set of elements would be ambiguous. The definition below therefore makes semantic typehood a proof-relevant relation and defines the elements by recursion on its derivations; lemma 111.62 then proves that the recursion is unambiguous after all.

Because the universes are strict, a level cannot be forgotten, and the construction is stratified twice: first the level-i codes, whose level matters because U-Hier places Uj in Ui only for ji; then the semantic types, in which a lift is invisible because Lift-El makes it so.

Convention 111.51 — Ambient metatheory for the kernel signature

Section 111.8Section 111.10 are carried out in ZFC. External level parameters remain formal. A subscript i,j,λ or μ below ranges over the canonical symbolic level forms of definition 111.18; i+1 means normalization after successor. Write ij when i<j under every assignment of the external parameters. Both equality and are decided on the symbolic forms by lemma 111.19. In particular, evaluation never chooses an ambient assignment and never replaces a symbolic level by a numeral.

The domain D of definition 49.36 is a set. The proof-relevant code relations below are constructed as ranked well-founded trees, not postulated as an inductive–recursive type. Replacement therefore makes the relations and their element relations sets; no inaccessible cardinal is used.

Definition 111.52 — World-indexed related neutral values

Let k,kDne be Ψ-admissible. Write kΨnek when, for every iterated typed target weakening ω:ΨΦ, there is a raw expression a such that R|Φ|(ωk)=aandR|Φ|(ωk)=a. Graph determinism makes a unique. Thus future readback depths occur only as the lengths of explicit future worlds.

The readback-defined field at Ψ is KΨ:={kDnek is Ψ-admissible, andfor every iterated typed target weakening ω:ΨΦ,there is an a with R|Φ|(ωk)=a}. Admissibility alone does not imply membership in KΨ. The relation Ψne is therefore treated as a partial equivalence relation on all Ψ-admissible neutrals, with field KΨ, rather than as a reflexive relation on that entire set. When a ranked generator is displayed at support Ψ, an omitted subscript on ne means Ψ.

Example 111.53 — An admissible neutral outside the readback-defined field

Fix ϵ=exp and ϱ=runtime, and form the raw terms L:=λϵ,ϱ(z:1).zϵ,ϱz,Ω:=Lϵ,ϱL. Put F1:=;u.1,B:=Π^ϵ,ϱ(1^,F1),d:=lamϵ,ϱ(;y.Ω). Let Ψ:=.Π^ϵ,ϱ(B,F1),k:=appϵ,ϱ(x0;B;d). The only free neutral of k is x0, the stored domain is the domain of its classifier in Ψ, and both displayed raw closures are closed by their environments. Hence k is Ψ-admissible.

At the identity weakening, R1(k) requires B1(d). Product reification applies d to the fresh reflected 1 argument, so closure execution must evaluate Ω. No finite derivation does so: a derivation for LL would contain, below its two lambda evaluations, a strictly shorter derivation of the same closure application produced by the body zz. Induction on derivation height rules out such a derivation. Therefore kKΨandkΨnek. The example uses ill-typed raw syntax inside a closed closure. It does not challenge totality on well-typed inputs; it explains why every later neutral formation argument proves self-relatedness instead of appealing only to admissibility.

Lemma 111.54 — Neutral relatedness is a partial equivalence relation

For every support telescope Ψ:

  1. Ψne is symmetric and transitive on the set of Ψ-admissible neutrals;

  2. for every Ψ-admissible k, kΨnek if and only if kKΨ;

  3. the restriction of Ψne to KΨ is an equivalence relation.

Proof of Lemma 111.54 — Neutral relatedness is a partial equivalence relation

Proof. For symmetry, fix ω:ΨΦ and reverse the two equalities with their common readback output. For transitivity, suppose k0Ψnek1 and k1Ψnek2. At ω, let a be the common output for the first premise and b the common output for the second. Determinism of the readback graph on ωk1 gives a=b, so all three readbacks have one common output. Quantifying this construction over ω proves transitivity.

The definition of kΨnek asks for exactly one defined readback after every typed target weakening; by graph determinism this is exactly kKΨ. Hence the restriction to KΨ is reflexive, and the first part supplies symmetry and transitivity there. ◻

Lemma 111.55 — World-indexed neutral formation

If j<|Ψ|, then xjΨnexj. If Ψ.A is well formed, then in particular x|Ψ|Ψ.Anex|Ψ|. More generally, take one of the seven nonvariable neutral constructors app, fst, snd, ind2^, indN^, J^, vind^. Two Ψ-admissible instances are related whenever their principal neutral fields are related at Ψ and, after every typed target weakening ω:ΨΦ, each pair of transported semantic fields used by readback has defined, unique, equal quotation or reification output at depth |Φ| and at its displayed typed binder extensions.

Proof of Lemma 111.55 — World-indexed neutral formation

Proof. Fix ω:ΨΦ. The variable equation is R|Φ|(ωxj)=ωxj. For application and the two projections, unfold their neutral-readback equations: the principal outputs agree by the neutral premise, and the application argument outputs agree by the transported stored-field premise. Boolean and natural elimination additionally use, in order, the motive, base branches, step branch, and principal hypotheses. Identity elimination uses the carrier, endpoints, three-variable motive, reflexivity branch, and principal hypotheses. Vector elimination uses the stored vector type, two-variable motive, base, four-variable successor method, index, and principal hypotheses. Thus both readback graphs have one common output at the exact target depth |Φ|; graph determinism makes it unique. Quantifying over typed future worlds Φ is exactly definition 111.52. ◻

Lemma 111.56 — World equivariance of neutral relatedness

If kΨnek and ω:ΨΦ is iterated target weakening, then ωkΦneωk.

Proof of Lemma 111.56 — World equivariance of neutral relatedness

Proof. Given a further typed weakening τ:ΦΞ, apply the defining condition at τω:ΨΞ. Functoriality identifies its two inputs with τ(ωk) and τ(ωk). Their readbacks at the exact depth |Ξ| have the same unique output, which is the defining condition at Φ. ◻

Definition 111.57 — Natural dependent-family evidence

Every ranked code or semantic-type derivation is formed at a finite support telescope Ψ. Its declarations classify the endpoints, closure fields, and ranked premises as they are introduced, and its levels are the initial segment 0,,|Ψ|1. Support is not reconstructed from an erased derivation. Write α@Ψ to retain this formation index. Given α:AiA@Ψ,F,F:DD, a relational support telescope Ψ consists of two endpoint telescopes with the same finite variable positions and ranked relatedness evidence for corresponding classifiers. Its extension Ψ.α has endpoint telescopes Ψ.A and Ψ.A and uses α as its final classifier relation. A relational world substitution for this data is a pair σ=(σ0,σ1;q):ΨΦ of telescope-indexed semantic substitutions together with ranked witnesses q showing, declaration by declaration, that the two assigned values lie in the transported element relation of that declaration. Its action on α is written σα and has endpoints σ0A and σ1A. Its operations are: The identity idΨ:ΨΨ has the recursively reflected components of definition 111.47. Put β:=σα. Target weakening is wkσ:ΨΦ.β. The canonical fresh lift has type σ:Ψ.αΦ.β. Its final pair is classified by (wkσ)α over the already-extended target Φ.β. Thus the relation classifying the fresh pair is not the declaration used to extend Φ. If ζ:(d,e)EltΦ(σα), binder extension is the distinct operation (σ,d,e;ζ):Ψ.αΦ. It adjoins (d,e;ζ) to q without weakening the target. Formation of ζ gives d,eDΦ, so arbitrary variables of Φ may occur in d,e, but no level outside Φ may occur. Composition is typed by τ(σ,d,e;ζ)=(τσ,τ0d,τ1e;τζ), which is the relational instance of equation 111.2. Canonical lift is used only when a fresh target declaration is introduced.

A natural dependent-family premise β assigns, to every relational world substitution σ:ΨΦ and every ranked witness ζ:(d,e)EltΦ(σα), a ranked derivation (111.2)βσ,ζ:(σ0F)(d)i(σ1F)(e)@Φ. It also carries the naturality equation τ(βσ,ζ)=βτσ,τζ(τ:ΦΞ), after the definitional closure-execution and substitution-composition equations of lemma 111.48. Semantic-type family premises are defined by replacing i with .

Reindexing along a relational ν:ΨΨ is precomposition: (νβ)σ,ζ:=βσν,ζ(σ:ΨΦ). Equation 111.1, Equation 111.3 prove that reindexing through a binder lift retains target gap variables. No inverse or restriction to the image of ν is used. For a self- derivation and a diagonal relational substitution, boldface and the two identical assignment subscripts are omitted: in particular, Ψ may denote the diagonal relational telescope Ψ, and idΨ then denotes its paired reflected identity.

Definition 111.58 — Semantic codes

For every initial support telescope Ψ and canonical symbolic level i, define a relation i@Ψ on DΨ, related codes at level i, and for each derivation α:AiB@Ψ a proof-relevant relation EltΨ(α)DΨ×DΨ, by the ranked construction below. A judgment η:(d,e)EltΨ(α) therefore contains three formation facts: dDΨ, eDΨ, and η is Ψ-admissible. These facts are premises of membership, not consequences reconstructed from an erased pair. Write ACi@Ψ for AiA@Ψ; omit @Ψ only when the enclosing evidence fixes it. Each generator is displayed with the data it needs, followed by the element relation it defines. A support index is omitted inside a generator whose premises already display it. Derivations and membership evidence carry the initial telescope of definition 111.57; their action by typed semantic substitutions is constructed with their ranks. Write ui and ni for the displayed Unit and natural self-generator derivations at level i; these names refer to evidence, not yet to a derivation-independent relation.

Here is the promised construction. The symbolic order is well founded: if ij, then evaluating every parameter at zero gives i(0)<j(0), so an infinite -descending chain would give an infinite descending chain of natural numbers. Proceed by well-founded recursion on i under . At a fixed i, build proof trees in ordinal stages. A generator enters stage ξ+1 only when every same-level code premise has already entered some stage below ξ+1; a universe premise may instead use the completed construction at ji. For a dependent family of premises, Replacement supplies their set of ranks and the generator is assigned one plus its supremum. The element relation of a new proof tree is then the displayed set expression in the already-defined premise relations. At support Ψ, the Boolean, natural, and vector clauses use their displayed least positive subrelations of DΨ×DΨ. Membership in every such relation is also proof relevant: a membership derivation records its outer constructor and has rank one greater than the supremum of its recursive membership premises. In particular, predecessor evidence for naturals and tail evidence for vectors have smaller rank. A vector-type generator is ranked above both its element-code premise and its length evidence; the semantic embedding of that code premise is recorded below the vector generator. Limit stages take unions of proof trees, not unions of the relations attached to one tree. Put h(i):=i(0). Thus every occurrence of Elt is at a smaller triple (h(i),ξ,μ) in lexicographic order, where ξ is the construction rank and μ is the membership rank; a nonrecursive membership premise has μ=0. A smaller symbolic level has smaller h, a same-level generator premise has smaller ξ, and a natural or vector predecessor has smaller μ. This constructs both the proof-relevant codes and their element relations; it also records the rank used by the later readback induction.

Unit.

1^i1^, with element relation DΨ×DΨ at support Ψ. Its nullary membership constructor takes the two displayed Ψ-admissibility derivations as premises.

Booleans.

2^i2^, with element relation the least one containing (tt^,tt^), (ff^,ff^), and (up2^(k),up2^(k)) for every knek.

Naturals.

N^iN^, with element relation the least one containing (0^,0^), containing (suc^(d),suc^(e)) whenever it contains (d,e), and containing the related neutrals as in the Boolean clause.

Universes.

U^jiU^j for ji, with element relation j.

Products.

From α:AiA@Ψ and a natural dependent-family premise β as in definition 111.57, infer Π^ϵ,ϱ(A,F)iΠ^ϵ,ϱ(A,F), with element evidence at support Ψ consisting of pairs (g,h) equipped with, for every relational σ=(σ0,σ1;q):ΨΦ and ζ:(d,e)EltΦ(σα), unique application outputs gdσ0,heσ1 and evidence ησ,ζ:(gdσ0,heσ1)EltΦ(βσ,ζ). These outputs and witnesses obey the analogue of equation 111.3 under every τ:ΦΞ.

Sums.

From the same data, infer Σ^(A,F)iΣ^(A,F), with element relation {(p,q)all four projections have unique outputs,(p1,q1)EltΨ(α),(sndvp,sndvq)EltΨ(βidΨ,η1)}, where p1=fstvp and q1=fstvq, and η1:(p1,q1)EltΨ(α) is the recorded first-component witness. Substitution acts on this evidence using equation 111.3.

Identity.

From α:AiA together with (da,da) and (db,db) in Elt(α), infer Id^(A,da,db)iId^(A,da,db). For a relation R and a finite set S, write CliqueR(S) when S×SR. The element relation is the least one containing the related neutrals and containing (refl^(d),refl^(e)) precisely when CliqueElt(α)({da,db,d,da,db,e}). Thus the evidence on both sides inhabits the single endpoint equivalence class; no unprimed endpoint is privileged.

Vectors.

From γ:CiC and ν:(dn,dn)Elt(ni), infer Vec^(C,dn)iVec^(C,dn). Its element relation is defined by recursion on ν: at (0^,0^) it contains (vnil^,vnil^) and the related neutrals; at (suc^m,suc^m) over a shorter derivation ν it contains in addition every pair (vcons^(m,a,xs),vcons^(m,a,xs)) with (a,a)Elt(γ) and (xs,xs) in the relation given by ν; at related neutral lengths it contains the related neutrals only.

Lifts.

From γ:CjC with both sides stuck, infer Lift^j(C)j+1Lift^j(C), with element relation Elt(γ).

Neutral codes.

From knek put N:=upU^i(k) and N:=upU^i(k), and infer NiN. Its element relation is {(upN(k1),upN(k1))|k1nek1}. Thus the formerly implicit annotations are exactly the two endpoint codes; no arbitrary A,BD are quantified here.

A value is stuck when it is upU^j(), or Vec^(,), or Lift^j(); these are exactly the three values on which lift^ of definition 111.44 does not compute.

Definition 111.59 — Semantic types

For every initial telescope Ψ, define a relation AB@Ψ on DΨ, related semantic types, and EltΨ on its derivations, by the inductive definition with the generators of definition 111.58 at every level i read with in place of i throughout, except that

  • U^iU^i has element relation i, for every i;

  • Vec^(C,dn)Vec^(C,dn) requires CiC at a common level i, not merely CC; its generator records both the code premise γ and its structural semantic embedding γ¯. The two ranked relations and this embedding are constructed simultaneously: each code generator maps to the corresponding semantic generator, while a lift maps to two peels. Thus γ¯ is formed below the vector generator and carries the same displayed element relation and membership ranks;

  • the generator for Lift^ is replaced by the two peeling generators: from δ:CB infer Lift^j(C)B and BLift^j(C), both with element relation Elt(δ);

  • upU^i(k)upU^j(k) is generated from knek for arbitrary i,j.

This is again a ranked least relation. At stage ξ+1 a generator may use only semantic-type premises of rank at most ξ and the already constructed code relations. Peeling therefore decreases construction rank even when it leaves the symbolic universe level unchanged. The same Replacement-and-supremum argument as in definition 111.58 handles the premise family of Π^ and Σ^. Consequently Elt is defined from strictly earlier evidence in every clause. Write AT@Ψ for AA@Ψ; omit @Ψ only when the enclosing evidence fixes it.

Convention 111.60 — Suppressed world indices

The two preceding definitions attach a support to every ranked derivation. A statement in which every ranked premise and conclusion remains at one support universally quantifies over that initial telescope Ψ and may omit the repeated world annotation. In particular, η:(d,e)Elt(α) with α@Ψ is only an abbreviation for the formed judgment η:(d,e)EltΨ(α); it never denotes membership in an unindexed raw relation on D. If σ:ΨΦ, then membership in Elt(σα) is at Φ and therefore contains proofs that both endpoints lie in DΦ. Whenever a substitution changes the world, both source and target indices are displayed. This convention never permits quotation at a number unrelated to the length of its displayed support.

Remark 111.61 — Why Unit relates all admissible values at one support

At a support Ψ, the clause for 1^ relates every pair in DΨ×DΨ. That is deliberate and it is what 1-η demands: two terms of type 1 are judgmentally equal whenever they are formed at the same support, so no finer support-indexed relation could be complete. Three consequences have to be checked rather than assumed.

Reification stays defined, because 1^n ignores its argument and returns ; no clause of definition 49.37 inspects a value at 1^. Reflection likewise returns ^ without consulting the neutral.

A family over 1^ must therefore be related to itself after every semantic substitution and at every target-admissible pair: the Π^ generator quantifies βσ,ζ over all ζ:(d,e)EltΦ(σα) when σ:ΨΦ. For a family arising from a type B over x:1 this natural premise is supplied by lemma 111.74 itself: the semantic half of lemma 111.74 quantifies over EltΦ(σui)=DΦ×DΦ. Formation of the membership evidence supplies d,eDΦ, exactly the hypotheses needed by semantic extension. So the induction hypothesis for B applies at (σ0ρ,d)Φ(σ1ρ,e) and gives [[B]](σ0ρ,d)[[B]](σ1ρ,e) for all d,eDΦ. On the syntactic side the Kripke clause at 1^ imposes only Δ:1 beyond the standing element requirement, which is again vacuous here.

Finally, no other former indiscriminately relates all of DΨ at a fixed support: every other element clause requires a constructor head or a related neutral. Unit totality never crosses a support boundary; only an explicit typed substitution transports its membership evidence.

The two exceptions are the whole content of the strict-lift package. Peeling says that a lifted code is the very type it lifts, which is Lift-El; keeping the code inside Vec^ says that Vec was formed from a code and that no equation moves a lift across it, which is remark 111.21.

Lemma 111.62 — The relations are functional partial equivalences

Fix a support telescope Ψ; every unannotated derivation and membership judgment in clauses (1)–(6) is formed at Ψ in the sense of convention 111.60.

  1. i and are symmetric and transitive, and each EltΨ(α) is symmetric and transitive on DΨ.

  2. If α,α both derive AiB, then EltΨ(α)=EltΨ(α); likewise for . Hence EltΨ(AB) is well defined, and we write EltΨ(A) for EltΨ(AA).

  3. If αi:AiB and αj:AjB, then Elt(αi)=Elt(αj). The equality carries a canonical outer-constructor-preserving transport between membership derivations, with the rank bound stated in (6).

  4. If AiB then AB and the two element relations agree.

  5. If AB and AB then BB; and lift^i preserves up to peeling: lift^i(C)C whenever CCi.

  6. The equalities of element relations in (2)–(4) are realized by explicit evidence maps. For derivations δ,δ with the same semantic endpoints and η:(d,e)Elt(δ), there is evidence trδ,δ(η):(d,e)Elt(δ),trδ,δ(trδ,δ(η))=η. For code derivations αi:CiC and αj:CjC with the same endpoints, trαi,αji,j(ζ):(d,e)Elt(αj)for every ζ:(d,e)Elt(αi), and the reverse composite is the identity. A bridge θ:AB determines δA:=θ;θop and δB:=θop;θ; it supplies inverse evidence brθ(η):(d,e)Elt(δB) for every η:(d,e)Elt(δA). Finally, if δ is the non-peeling core of δ, then peelδ(η):(d,e)Elt(δ). The reverse peeling map restores evidence at δ. Every map preserves admissibility and the outer membership constructor and is natural in the support world: σtrδ,δ(η)=trσδ,σδ(ση), and, with every displayed expression well typed, σtrαi,αji,j(ζ)=trσαi,σαji,j(σζ),σbrθ(η)=brσθ(ση),σpeelδ(η)=peelσδ(ση),σunpeelδ(η)=unpeelσδ(ση). Its output rank is bounded by the Hessenberg sum of the ranks of its input evidence and the derivations defining the map.

Proof of Lemma 111.62 — The relations are functional partial equivalences

Proof. Prove simultaneously, by the rank construction of definition 111.58, definition 111.59, the five assertions below.

  1. Two derivations with the same code endpoints, or the same semantic-type endpoints, assign the same element relation.

  2. Code derivations with the same endpoints at two possibly distinct symbolic levels assign the same element relation. Equality is witnessed by a transport of ranked membership derivations that preserves their outer constructor.

  3. The code and semantic-type relations are symmetric and transitive, and every assigned element relation is symmetric and transitive.

  4. If α:AB, then its element relation equals the relations assigned to the self-derivations obtained by composing α with its converse. Thus all three may be denoted Elt(A)=Elt(α)=Elt(B).

  5. Peeling any finite spine of Lift^ preserves the assigned element relation.

The simultaneous induction uses a measure that remains valid when two code levels differ. For code evidence at levels i1,,ir, its first component is the finite multiset [h(i1),,h(ir)], ordered by the multiset extension of < on N. Its second component is the Hessenberg, or natural, sum rk(δ1)##rk(δs)#rk(η1)##rk(ηt). Order the pair lexicographically. The multiset component decreases when a universe premise replaces an ambient level by a strictly smaller one. At a fixed multiset, the natural sum decreases when any construction, peeling, or membership premise is selected, because natural sum is strictly monotone in every argument. In particular, the transitivity induction uses rk(δ)#rk(δ), not ordinal addition in a chosen order. This measure covers same-level, cross-level, transitivity, vector, and peeling calls.

For (F) and (C) at codes, distinct non-lift heads are disjoint constructors of D, so two derivations use the same generator. Apply (F) to the domain premise when the ambient levels agree, and (C) when they do not. Apply the same assertion to the smaller natural family premises. For a product, the evidence map is forced by its universal premise. Fix an arbitrary target relational substitution σ:ΨΦ and arbitrary target-domain witness ζ:(d,e)Elt(σα). First transport it backward across the inverse domain comparison: ζ:=trσα,σα(ζ). Apply the source universal function evidence to ζ, obtaining result evidence at βσ,ζ. Then transport that result forward across the family comparison to obtain evidence at βσ,ζ. The reverse comparison gives the inverse map. Under a further τ:ΦΞ, both constructions become the same construction at τσ: this is equation 111.3 together with the displayed naturality equation in (6). Hence the map is compatible both with the selected dependent fiber and with all future worlds. Sums use the same backward domain transport on their recorded first-component witness before the forward fiber transport on the second component. The displayed element relations then agree. Naturals use induction on their positive element derivations. Vectors add an inner induction on the length evidence and use (C) for their element-code premise. The constructor, successor, and neutral cases are disjoint, so the transport preserves the outer constructor and recursively transports the stored evidence.

For a universe endpoint U^k, both ambient levels must place k strictly below them; both element relations are the already completed k. A lift endpoint determines its ambient level as the normalized successor of its stored lift index, so two such derivations have the same ambient level. A neutral-code endpoint upU^k(q) likewise determines the ambient level k. These observations close the universe, lift, and neutral cases of (C).

For semantic types, (F) at a vector head may compare derivations whose element-code premises were chosen at different levels. Assertion (C) gives the required equality and membership-evidence transport before the vector clause is compared. Only peeling creates another critical pair. Define strip(Lift^jC)=strip(C) and let s(A,B) be the total number of leading lifts. Induction on s factors every semantic-type derivation into left peels, a unique non-peeling core generator, and right peels. Two left peels, or two right peels, commute by the induction hypothesis on the shorter spine. The mixed critical pair Lift^iCLift^jD can peel left then right or right then left; both paths reach CD and both inherit exactly its element relation. Nested lifts repeat this diamond with smaller s. This proves (L) and closes the only overlap in (F).

For (P), symmetry reverses every premise. At a product or sum, (S) makes the domain element relation independent of its orientation, so the family premise is available at the reversed pair. For transitivity, first use (S) to regard all three domain relations as one PER. If (d,f) belongs to it, symmetry and transitivity give (d,d); use d as the middle argument in the first family premise and then compose with the second premise at (d,f). The function case is pointwise. For the dependent-sum case, write α01:A0A1,α12:A1A2 and let α02 be their composite. To construct transitive membership, start with sum values P0,P1,P2. Put dr:=fstv(Pr) and er:=sndv(Pr) for r{0,1,2}. The two input derivations contain (d0,d1)Elt(α01),(e0,e1)Elt(βd0,d101),(d1,d2)Elt(α12),(e1,e2)Elt(βd1,d212). The common first component d1 selects the composite family premise βd0,d202:=βd0,d101;βd1,d212:F0(d0)F2(d2). The last two second-component premises compose to (e0,e2)Elt(βd0,d202). A different relational factorization through a first component d1 gives the same fiber relation and membership transport by (F) and (S); hence the output does not depend on the chosen transitivity witness.

Boolean and natural constructor cases are immediate, and a neutral middle value forces both sides into the neutral case because constructor and neutral generators are disjoint. For vectors the evidence map from premises (γi,νi) to (γj,νj) is defined by the complete recursion below. Write νr+:=suc(νr). Vi,j(zero,zero;vnil)=vnil,Vi,j(νi+,νj+;vcons(ζ,η))=vcons(trγi,γji,j(ζ),Vi,j(νi,νj;η)),Vi,j(q,q;neutral(k))=neutral(k). In the last line q,q are the two related-neutral length witnesses. Here γi and γj are the two element-code premises, possibly at different ambient levels; the second line decreases both length and tail membership rank. The three constructors are disjoint, so these clauses are total on vector membership evidence and no mixed zero/successor/neutral case exists. For identity, two reflexivity pairs give two Elt(α)-cliques with their middle witness in common; the PER laws for Elt(α) make their union a clique, so the outer reflexivity pair composes. Neutral identity evidence composes only with neutral evidence. Universe elements use (P) at the smaller symbolic level. Peeling uses the diamond above. These cases prove (P), and composing a derivation with its converse and applying (F) proves (S).

The recursive constructions just displayed define the maps in (6). Reversing the comparison defines their inverses. Their outer constructors are unchanged, and the bound on their output ranks follows by the same multiset/natural-sum induction. This simultaneous proof establishes functionality before the first use below that omits derivation evidence. Proof relevance supplies the ranks for the comparison and the peeling diamond.

(4) now follows by induction on AiB. Each generator of i other than the lift generator is a generator of , with the same Elt. For U^j with ji, the element relation is j on both sides. The lift generator maps to two applications of peeling, whose Elt is again Elt(γ).

(5) The first claim is symmetry followed by transitivity. For the second, induct on CCi: on the seven heads where lift^i computes, the result is related to C by the induction hypothesis applied to its components, since peeling is not needed for 1^,2^,N^ and U^k and the Π^, Σ^, Id^ clauses lift their components; on the three stuck heads the result is Lift^i(C), related to C by one peeling step. ◻

Lemma 111.63 — Reification is determined by relatedness

Let Ψ be an initial support telescope and put n=|Ψ|. All evidence below is formed at Ψ.

  1. If δ:AB@Ψ then both Qn graphs are defined and have the same unique output.

  2. If α:AiB@Ψ then both Qnc graphs are defined and have the same unique output.

  3. If δ:AB@Ψ and η:(d,e)EltΨ(δ) then both reification graphs are defined and have the same unique output.

  4. If kΨnek and δ:AB@Ψ, then both reflection graphs are defined; their unique outputs form a pair in EltΨ(δ).

Proof of Lemma 111.63 — Reification is determined by relatedness

Proof. Use the multiset/natural-sum measure of lemma 111.62, including both code-premise levels when a semantic vector derivation is inspected, with an inner induction on ν in the vector case and on the readback-graph derivation in the three inductively generated element relations. The induction proves existence and uniqueness together: existence follows by constructing the displayed graph clause; uniqueness follows because its premises have unique outputs and distinct outer constructors select distinct clauses. All four operations peel Lift^ first, and the peeling generators change neither side of any claim, so those cases are immediate from the induction hypothesis; clause (2) is the exception, and there both sides carry the same lift, so the clause Qnc(Lift^j(C))=Liftj(Qnc(C)) reduces it to the induction hypothesis.

Π^. For (1), Qn emits the same (ϵ,ϱ) on both sides because the generator requires them equal; the domains agree by the induction hypothesis; the codomains are F(vnA) and F(vnB). Let Ψ be the relational support carried by the product generator, and put ω=wkΨ,δ0, where δ0 is its domain premise. Its endpoint targets are Ψ.A and Ψ.B, both of length n+1. The fresh variables are related neutrals at those exact target worlds by lemma 111.55. Clause (4) at the transported domain gives ζv:(vnω0A,vnω1B)Elt(ωδ0), so the natural premise βω,ζv relates the two codomains and the induction hypothesis applies at level n+1. For (3), emits a λ on both sides; its bodies are n+1(gvnA) and n+1(hvnB), related by the product membership evidence at (ω,ζv), so the induction hypothesis applies. For (4), reflection produces two eta values. For an arbitrary relational substitution σ=(σ0,σ1;q):ΨΦ and ζ:(d,e)Elt(σδ0), applying them gives the two outputs of the simultaneous substitution-and-application graph. Inspect its last rules. If the transported heads remain stuck, the outputs are βσ,ζ(app(σ0k;σ0A;d)) and βσ,ζ(app(σ1k;σ1B;e)). The latter is the primed counterpart. The application neutrals are related at the target support: after any further typed weakening, their heads agree by world stability of neutral relatedness and their reified arguments agree by (3) at that exact future world. If substitution exposes a closure or constructor head, the matching semantic-operation rule fires on both sides; its domain and strict family premises are smaller simultaneous-induction premises and give membership directly in Elt(βσ,ζ). These are all last rules of semantic application. Naturality under a further substitution is equation 111.3.

Σ^. For (1), the domain quotations agree by the induction hypothesis at Ψ. Reify the related first projections at depth n; their common output selects the two codomain values through βidΨ,η1. The induction hypothesis at that strict family premise gives equal codomain quotations at the same exact depth. For (3), the sum membership evidence first supplies η1 for the semantic first projections. Its stored second witness has type η2:(sndvd,sndve)Elt(βidΨ,η1), so the two induction hypotheses give equal first components and then equal second components in the fiber selected by those first components. For (4), lemma 111.55 at Ψ gives fst(k)Ψnefst(k). Reflection at the domain turns that pair into the witness selecting the second fiber; the same lemma then gives related second projections at that fiber. After a typed future weakening, equation 111.3 identifies the transported selected fiber with the fiber selected in the target world.

1^. Both reifications are and both reflections are ^, which is related to itself because ^DΨ and EltΨ=DΨ×DΨ. This clause is the one that makes Elt not a subsingleton and is exactly 1-η.

2^, N^. Induct on the element derivation: a constructor pair reifies to the same constructor, with the suc^ case using the inner induction hypothesis; a related neutral pair reifies to Rn(k)=Rn(k), equal by definition 111.52. For (4), is up and the pair is related by the neutral generator.

Id^. A related pair is (refl^(d),refl^(e)) whose clique premise includes (d,e)Elt(A), reified to reflA(d) and reflB(e), equal by (3) at the smaller type; or a related neutral pair, handled as above. In (1) the two endpoints are reified at A and B and are equal by (3).

Vec^. Clause (1) reads back the two element codes with Qnc and uses (2); this is where the absence of Lift-Vec is respected, since (2) keeps a lift that (1) would have deleted. For (3), induct on ν: at 0^ both sides reify to vnil; at suc^ the three components are reified at N^, at the element code, and at the shorter vector type, each equal by an induction hypothesis; at a neutral length only neutral pairs occur.

U^i. A related pair of elements is a pair of related level-i codes, and reification at U^i is Qnc, so (3) at U^i is exactly (2). For (4), reflection at a universe is up, and two related neutrals generate a related pair of neutral codes.

Neutral type. All four claims reduce to Rn(k)=Rn(k). ◻

Lemma 111.64 — Substitution action on ranked semantic evidence

Let σ=(σ0,σ1;q):ΨΦ be relational for the displayed Ψ-admissible endpoints, closure fields, and evidence. The action of definition 111.47 extends to maps σδ:σ0Aσ1B@Φfor δ:AB,σα:σ0Ciσ1C@Φfor α:CiC,ση:(σ0d,σ1e)EltΦ(σδ)for η:(d,e)EltΨ(δ). Each map preserves a constructor outer generator. A neutral may compute after substitution; in that case its output rank is bounded by the Hessenberg sum of the input rank and the ranks in q. It preserves Ψ-admissibility as Φ-admissibility. In particular, the membership map transports both endpoint-admissibility premises and sends DΨ×DΨ into DΦ×DΦ. It is strictly functorial: idξ=ξ,(τσ)ξ=τ(σξ) for every displayed kind of evidence ξ. It commutes with the same-endpoint, cross-level, bridge, and peeling maps of lemma 111.62(6), with arbitrary source extension by equation 111.2, and with fresh canonical lift by equation 111.1.

Proof of Lemma 111.64 — Substitution action on ranked semantic evidence

Proof. Induct on the ranked derivation and its membership evidence simultaneously. The nullary code and type generators are fixed. Unit membership transports its two endpoint-admissibility derivations along σ, yielding endpoints in DΦ; the remaining nullary membership constructors are transported componentwise. For a product or sum generator supported at Ψ, act on the domain premise and reindex its natural family by equation 111.4: (σβ)τ,ζ:=βτσ,ζ(τ:ΦΞ). The endpoints agree because semantic evaluation and closure execution commute with composition. Naturality of σβ is the calculation υ(σβ)τ,ζ=equation111.3βυτσ,υζ=(σβ)υτ,υζ. For product membership, define (ση)τ,ζ to be ητσ,ζ. Thus an arbitrary target witness ζ, including one containing variables of Ξ, is passed to the source universal premise at the composite substitution; it is never pulled back through a nonexistent inverse. Sum membership transports its first-component witness and then selects (σβ)idΦ,ση1=βσ,ση1 for its second component.

Identity evidence transports the carrier premise, all six members of its clique, and the reflexivity or neutral outer constructor. Vector evidence uses the zero, successor, and neutral recursion: successor acts on the code-head witness and on the shorter tail witness. Universe evidence acts on its smaller-level code derivation. Lift evidence acts on its premise and retains the symbolic level. Neutral-code evidence acts on both endpoint annotations fixed in definition 111.58; at a variable it uses the corresponding component of q, and at a compound neutral it executes the semantic operation and applies the induction hypotheses to every stored field. Thus the result need not remain neutral, but it remains in the required element relation. Constructor cases preserve the proof-tree shape; the relational-neutral case is bounded by the ranks recorded in q. Identity and composition follow by the same induction; the product case reduces to associativity of substitution composition. An arbitrary binder instantiation uses equation 111.2; a fresh readback binder uses equation 111.1. Applying the induction to the definitions of tr and peel proves commutation with the four evidence maps. ◻

Definition 111.65 — The ranked Kripke relation between syntax and values

For a context Δ, with n:=|Δ|, let ΨΔ be its semantic classifier telescope. Let δ:AA@ΨΔ be a ranked self-derivation and let η:(d,d)EltΨΔ(δ) be ranked membership evidence formed at that same telescope. Its formation supplies dDΨΔ. Define Δδ,ηad by well-founded recursion on two nested orders. The outer generator order is g(δ):=([h(i1),,h(ir)],rk(δ)), where the multiset lists the ambient levels of the active code premises and rk(δ) is the construction rank. Order this pair lexicographically by the multiset extension and the ordinal order fixed in lemma 111.62. At a fixed δ, use an inner recursion on rk(η).

This nesting is essential. Before defining any clause at δ, define the entire membership-indexed family of relations for every strict generator premise δ0 with g(δ0)<g(δ). The product clause may therefore invoke the domain relation at an argument witness ζ of arbitrary rank: its generator α is strict, so no comparison with rk(η) or rk(ζ) is needed. Its result relation is likewise at the strict family premise βσ,ζ. Same-generator recursion occurs only for a natural predecessor and decreases rk(η). A vector successor calls the strict element-code embedding and the vector generator built from the shorter length premise; identity calls its strict carrier premise, a universe calls the smaller-level code premise, and peeling calls its strict core. These are all outer decreases. Thus this definition does not use the invalid measure rk(δ)#rk(η), which would fail for an arbitrary product argument. Every clause requires Δa:Qn(A) and uses the supplied η rather than re-deriving membership. The membership index is what lets a syntactically witnessed argument extend a related environment; without it the two halves of lemma 111.74 could not be run at the same Π-introduction. Before selecting a clause, normalize a peeling self-derivation to paired left–right peels around its unique non-peeling core δ:CC. The lift diamond in lemma 111.62 transports η to η:(d,d)Elt(δ), and Δδ,ηadΔδ,ηad. The core premise has smaller derivation rank. In the remaining clauses, named evidence is always an immediate premise of δ or η.

  • If δ is the 1^ generator, there is no further condition.

  • If δ is the 2^ generator, η is one of the three disjoint evidence forms. Respectively, either d=tt^ and Δatt:2; or d=ff^ and Δaff:2; or d=upB(k) with ΔRn(k)ne2 and ΔaRn(k):2.

  • If δ is the N^ generator, η is zero, successor evidence η, or neutral evidence. In the first case d=0^ and Δa0:N; or d=suc^(d) and there is b with Δδ,ηbd and Δasuc(b):N; or the neutral case as for 2^. The recursive call decreases rk(η).

  • If δ@ΨΔ is a product generator with domain premise α:BB@ΨΔ and natural family premise β, then for every inclusion ω:ΔΔ and every b,e with self-membership evidence ζ:(e,e)EltΨΔ(ωα) and Δωα,ζbe, the transported product generator, with Fω:=ωF, has the target-world premise βω,ζ:Fω(e)Fω(e). The transported function evidence ωη, evaluated at the identity substitution of the target world and at ζ, supplies a unique output (ωd)ϵ,ϱe and a smaller membership premise (ωη)id,ζ=ηω,ζ at βω,ζ, and Δβω,ζ,ηω,ζωaϵ,ϱb(ωd)ϵ,ϱe.

  • If δ is a sum generator with domain premise α and family premise β, then η has component premises η1 and η2, and Δα,η1pr1(a)fstv(d),ΔβidΨΔ,η1,η2pr2(a)sndv(d),

  • If δ is an identity generator with carrier premise α, then η is reflexivity evidence or neutral evidence. In the first case d=refl^(d); the clique stored by η supplies η:(d,d)Elt(α), and there is b with Δα,ηbd, Δareflb:Qn(A) and, in addition, the two endpoint equations ΔBn(da)b:Qn(B),ΔBn(db)b:Qn(B); or the neutral case. The endpoint equations are stored because typing a at IdQn(B)((da),(db)) does not by itself equate the two endpoints with b: the judgment Δreflb:IdA(a0,b0) is derivable whenever Conv applies, and nothing in it forces a0bb0. Id-comp is stated at annotations equal to the refl argument, so without these two equations the identity computation case of lemma 111.74 could not fire.

  • If δ is a vector generator, it records a code self-premise γ:CiC, its smaller semantic embedding γ¯:CC, and length evidence ν. At zero, η is nil or neutral evidence; in the nil case d=vnil^ and Δavnil:Qn(A), or the neutral case. At successor evidence ν the cons evidence η supplies ζ:(d1,d1)Elt(γ) and tail evidence η2; let δ be the vector self-generator built from γ,ν. Then d=vcons^(m,d1,d2) and there are b1,b2 with Δγ¯,ζ¯b1d1,Δδ,η2b2d2, Here ζ¯ is obtained from ζ by the transport of lemma 111.62(4),(6). That transport preserves the outer constructor. Moreover, Δavcons(N^n(m),b1,b2):Qn(A). At a neutral length, the neutral case only. The head call descends to the recorded code premise; the tail call descends in both ν and η.

  • If δ is the universe generator at i, then η is a ranked self-derivation of did, ΔaQnc(d):Ui, and ΔaQn(d) type.

  • If δ is a neutral-type generator, so A=upU^i(k0), then d=upB(k) with ΔRn(k)neRn(k0) and ΔaRn(k):Rn(k0).

The neutral case at A means: d=upB(k) with ΔRn(k)neQn(A) and ΔaRn(k):Qn(A). It is available only at the positive types of definition 49.14.

Lemma 111.66 — Kripke evidence independence

The following four indexed equivalences hold.

  1. If δ,δ:AA and η:(d,d)Elt(δ), put η:=trδ,δ(η). Then Δδ,ηadΔδ,ηad.

  2. If θ:AB, put δA:=θ;θop and δB:=θop;θ. For ηA:(d,d)Elt(δA) let ηB be its bridge transport from lemma 111.62(6). Then ΔδA,ηAadΔδB,ηBad.

  3. Let δi,δj be vector self-generators for the same endpoint Vec^(C,dm), built respectively from (γi,νi) and (γj,νj), and let ηi:(d,d)Elt(δi). Put ηj:=Vi,j(νi,νj;ηi):(d,d)Elt(δj), using trγi,γji,j on every successor head and the recursive map on its tail. Then Δδi,ηiadΔδj,ηjad.

  4. If δ has paired peeling core δ and η:=peelδ(η), then Δδ,ηadΔδ,ηad.

Proof of Lemma 111.66 — Kripke evidence independence

Proof. Prove all four claims simultaneously, before erasing evidence, by the same nested recursion as definition 111.65. The outer component is the multiset of the two ambient code heights followed by the Hessenberg sum of the compared generator ranks. After that generator pair is fixed, the inner component is the Hessenberg sum of the membership ranks being compared. An arbitrary product argument may have any membership rank, but every call made with it is at a strict domain or family generator and therefore decreases the outer component. Normalize both self-derivations to paired peeling spines. The peeling maps of lemma 111.62(6) give the same core and transport membership evidence without changing its outer constructor; each core derivation has smaller construction rank, so the natural-sum component decreases. A universe premise decreases the level multiset instead.

At Unit there is nothing to compare. At Boolean and natural types, functionality preserves the disjoint true, false, zero, successor, and neutral evidence forms. The successor case invokes the induction hypothesis on the predecessor membership evidence. At a product, let the compared self-generators have domain premises α,α and natural families β,β. Fix an arbitrary future embedding ω:ΔΔ and an arbitrary target witness ζ:(e,e)Elt(ωα). Transport it backward, ζ:=trωα,ωα(ζ), and use the induction hypothesis at the strict generator ωα to replace the target argument judgment indexed by ζ with the source one indexed by ζ. Apply the source universal premise to obtain ηω,ζ at βω,ζ. The family comparison and lemma 111.62(6) transport that result forward to the witness at βω,ζ; the induction hypothesis at this strict family generator transports the indexed result judgment. Under a further world map τ, both paths are the construction at τω, by equation 111.3 and the naturality of tr. Thus the comparison preserves the universal product clause, including its world and dependent-family indices. Reversing the maps proves the converse. At a sum, let d1=fstv(d). The map trδ,δ sends the stored first-component witness η1 to η1 and hence sends the selected family premise βid,η1 to βid,η1. Apply the induction hypothesis to Δα,η1pr1(a)d1andΔβid,η1,η2pr2(a)sndv(d) using precisely those two transported witnesses. This proves the dependent second projection at its transported fiber, rather than at an unidentified codomain. At an identity type, the transported clique contains the same reflexivity value and endpoints; recurse at the smaller carrier premise. Neutral identity evidence is literal after neutral-readback functionality.

For vectors, apply the three-clause map Vi,j displayed in the proof of lemma 111.62. Zero sends nil evidence to nil evidence. Successor sends vcons(ζ,η2) to vcons(trγi,γji,j(ζ),Vi,j(νi,νj;η2)), and the induction hypotheses apply separately to the head at the semantic embedding of γj and to the tail at the shorter vector generator. Neutral evidence is fixed. Zero, successor, and neutral lengths are disjoint, so no fourth case exists. The successor call decreases both the length and membership contribution to the natural sum; changing i to j uses the level-pair transport rather than comparing either level in an arbitrary order. At a universe, the membership evidence is itself a code self-derivation; lemma 111.62(2),(3) identifies its element relation without evaluating a level parameter. At a neutral type both sides are the same neutral-readback equations. These cases exhaust the generators and establish each displayed equivalence before any notation below forgets δ or η. Reversing every evidence map proves the reverse implications. ◻

Convention 111.67 — Erased Kripke notation

For AT, write Δad:A when there exist ranked witnesses δ:AA and η:(d,d)Elt(δ) such that Δδ,ηad. Lemma 111.66 makes the choice immaterial and transports this erased notation along AB.

Definition 111.68 — Realizing substitutions

Let ξ@Ψ be a finite tuple of Ψ-admissible semantic derivations and membership witnesses. Its support is the initial semantic telescope Ψ fixed by definition 111.47; there are no unused or unclassified levels.

A realizing substitution (σ^,σ):ΨΓ consists of a typed semantic substitution σ:ΨΨΓ, its diagonal relational witness q for ξ in the sense of definition 111.57, and a simultaneous raw substitution σ^=(b0,,b|Ψ|1) into Γ. Reading the support telescope from left to right, its jth obligation is the indexed judgment Γσδj,σηjbjσ(xj), at the substituted jth classifier.

The three extensions are distinct. If (σ^,σ):ΨΓ and Γσα,ζbe, then arbitrary source extension is (111.3)(σ^,b;σ,e):Ψ.AΓ. If ω:ΓΓ introduces target declarations, target weakening is (ωσ^;wkσ):ΨΓ. If Γ=Γ,xm:A introduces the fresh target declaration used by readback, require ΓAQm(σA) type. Its semantic classifier telescope is ΨΓ=ΨΓ.(σA), and canonical lift is (σ^,σ):=(ωσ^,xm;σ):Ψ.AΓ. Its final semantic component is (wkσ)A(xm). The classifier (wkσ)A lives over ΨΓ.(σA) and classifies that component; it is not the declaration extending ΨΓ. Reflection supplies the indexed obligation, so a bare neutral is never entered as a semantic value.

For composable realizing substitutions (σ^,b;σ,e):Ψ.AΓ and (τ^,τ):ΨΓΘ, composition is componentwise raw substitution paired with semantic composition. Substitution and weakening for typing, together with lemma 111.48, lemma 111.64, prove (τ^,τ)(σ^,b;σ,e)=((τ^,τ)(σ^,σ),b[τ^];τe):Ψ.AΘ. Writing out the semantic targets, canonical lifts satisfy (τ^,τ)(σ^,σ)=((τ^,τ)(σ^,σ)) as realizing substitutions from Ψ.A into the target context whose last semantic declaration is (τσ)A. The first equation is arbitrary instantiation; the second is fresh lifting. Neither is inferred from the other.

The two directions of the following lemma are the proof-relevant operations reify and reflect: clause (a) is reify, which turns evidence that a term is related to a value into a normal form together with the conversion certifying it, and clause (b) is reflect, which turns a neutral judgment into that evidence.

Lemma 111.69 — Escape, reflection, world stability, and quotation normality

Let AT, Δ a context, n=|Δ|. The witnesses used by an erased hypothesis are formed at the semantic classifier telescope ΨΔ, whose length is n.

  1. (Escape.) If Δad:A then ΔAn(d)nfQn(A) and ΔaAn(d):Qn(A).

  2. (Reflection.) If k is a neutral value with kΨΔnek (equivalently, kKΨΔ), ΔRn(k)neQn(A) and ΔaRn(k):Qn(A), then ΔaA(k):A.

  3. (World stability.) If Δad:A, ω:ΔΔ, let ωΨ:ΨΔΨΔ be its typed classifier-telescope weakening and, with n=|Δ|, Δaωa:Qn(ωΨA), then ΔaωΨd:ωΨA.

  4. (Transport.) If δ:AB@ΨΔ then Δad:A holds if and only if Δad:B does.

  5. (Type quotation.) If ΔAQn(A) type for some ΔA type, then ΔQn(A)nftype.

  6. (Code quotation.) If moreover ACi and ΔcQnc(A):Ui for some Δc:Ui, then ΔQnc(A)nfUi.

  7. (Element quotation.) Under the type-formation premise of (e), if δ:AA and η:(d,d)Elt(δ) are formed at ΨΔ, then Δδ,ηAn(d)d and the reified term is normal at Qn(A).

  8. (Quotation under realizing substitution.) Let δ:AA@Ψ, put n=|Ψ|, and η:(d,d)Elt(δ), and let (σ^,σ):ΨΓ be a realizing substitution, with m=|Γ|. Then ΓQn(A)[σ^]Qm(σA) type,ΓQm(σA)nftype,Γσδ,σηAn(d)[σ^]σd. If α:CiC@Ψ is among the evidence, the corresponding code equation and normality judgment are ΓQnc(C)[σ^]Qmc(σC):Ui,ΓQmc(σC)nfUi.

Proof of Lemma 111.69 — Escape, reflection, world stability, and quotation normality

Proof. Choose witnesses δ:AA and η:(d,d)Elt(δ) whenever an erased hypothesis is used. Prove (a)–(c) and (e)–(h) simultaneously by the nested recursion of definition 111.65. The outer induction is on the finite multiset of active code heights and the Hessenberg sum of the generator ranks used by the displayed claims. Once those generators are fixed, the inner induction is on the Hessenberg sum of their membership ranks. A product argument may have unbounded membership rank; every claim made about it is at the strict domain generator, and every claim about its result is at the strict natural family generator. Natural and vector predecessor calls decrease the inner rank or the recorded shorter generator. Include the strict code generator used by (f) in the outer component. Prove (b) with the canonical self-membership evidence produced by reflection in lemma 111.63(4), whose hypothesis kΨΔnek is now an explicit premise. Normalize paired peeling spines first. Their core premise has smaller derivation rank and peeling changes neither nor Qn, so the lift cases follow from the induction hypothesis. Claim (d) is exactly lemma 111.66 after evidence erasure.

The three standing requirements of definition 111.65 are discharged once and not repeated in the cases below. In (b), take ηk:(A(k),A(k))Elt(δ). This is lemma 111.63(4) at the displayed kΨΔnek premise. The typing requirement follows from lemma 111.26(2) and Conv. In (c), lemma 111.64 transports the semantic type, value, self-derivation, and membership evidence; lemma 111.48(3) transports every stored judgment to its quotation at depth n. Transitivity with the displayed equation for a supplies the left-hand conversion. This is the only valid passage from Qn(A) to Qn(ωA): weakening without world equivariance would retain the wrong fresh binder levels.

1^. (a): returns , which is normal by nf-star, and 1-η gives Δa:1. (b): the relation has no further condition. (c): the Unit generator and its stored typing equation are carried by lemma 111.48.

2^, N^. (a): in a constructor case returns that constructor, normal by nf-true, nf-false, nf-zero or, using the induction hypothesis on the smaller predecessor evidence η, nf-suc, and the stored equation is the required conversion. In the neutral case returns Rn(k), normal by nf-ne because 2 and N are positive. (b): the neutral case of the definition is the hypothesis. In (c), the constructor evidence is fixed and neutral evidence is acted on by ω; the stored equations are transported by lemma 111.48(3), and normality by lemma 111.26(1).

Π^ϵ,ϱ(B,F). (a): put Δ:=Δ,xn:Qn(B) and v:=B(xn). Then ΔxnneQn(B) by ne-var and Rn+1(xn)=xn. Moreover xnΨΔnexn by lemma 111.55, because xn is the final declaration of the explicit target world ΨΔ. Thus (b) at ωB, where ω=ωn,n+1, gives Δxnv:ωB. Let ζv be its indexed membership witness. The definition of the relation at Π^ gives Δaϵ,ϱxn(ωd)ϵ,ϱv:(ωF)(v), and (a) at the strict family premise βω,ζv gives a normal w:=(ωF)(v)n+1((ωd)ϵ,ϱv) with Δaϵ,ϱxnw:. Rule nf-lam makes λϵ,ϱ(xn:Qn(B)).w normal, and it is exactly An(d). Finally λ-eq and Π-η give aλϵ,ϱ(xn:Qn(B)).aϵ,ϱxnλϵ,ϱ(xn:Qn(B)).w. (b): let ω:ΔΔ, put n:=|Δ|, and Δbe:ωB. By (a) at ωB, ΔbωBn(e):, with the right side normal. Moreover, Rn(appϵ,ϱ(ωk;ωB;e))=Rn(ωk)ϵ,ϱωBn(e) is neutral by ne-app. After every typed future weakening from ΨΔ, its head agrees with itself by lemma 111.56, and its argument agrees with itself by lemma 111.63(3) at that future support. Hence the new application neutral is self-related at ΨΔ. Rule app-eq gives ωaϵ,ϱb that neutral. Now (b) at the strict target-world family premise βω,ζ concludes. (c): the quantifier over ΔΔ is transitive in the extension because world embeddings compose, and lemma 111.48 identifies the composite action; app-eq transports the left-hand conversion.

Σ^(B,F). (a): the two induction hypotheses give normal B(fstvd) and F(fstvd)(sndvd) with pr1(a) the first and pr2(a) the second; nf-pair makes the pair normal, and Σ-η followed by pair-eq gives a(,). (b): from fst(k) and snd(k), neutral by ne-fst and ne-snd. Reflection at the first component gives Δα,η1pr1(a)B(fst(k)). Let this value be d1. Only after fixing d1 does the second component have the fiber F(d1); reflection there, followed by pr2-eq, gives the second indexed premise. Thus both clauses use the same selected fiber. In (c), ωη1 selects ωd1, the family derivation is the target premise βω,ωη1, and ωη2 has exactly that membership type by lemma 111.64. The two projection equations then transport by lemma 111.48(3).

Id^(B,da,db). (a): in the refl^ case, (a) at B applied to Δbd:B gives a normal v:=Bn(d) with Δbv:Qn(B). Rule nf-refl requires in addition ΔBn(da)v:Qn(B) and the same for db; these are the two stored endpoint equations of definition 111.65 composed with bv, and they are not obtainable from the typing of a alone. Hence reflv=An(refl^(d)) is normal at Qn(A), and Δareflv: follows from the stored equation areflb and the Id-intro congruence along bv. The neutral case uses nf-ne, identity types being positive. (b): the neutral case is the hypothesis. In (c), the carrier witness and both endpoint equations are acted on by ω; the two equivariance equations for reification identify their target endpoints, and transitivity transports the left-hand equation.

Vec^(C,dm). (a): inspect the recorded length and vector-membership derivations. At 0^ the constructor case reifies to vnil, normal by nf-vnil because the stored equation is n0; at suc^(m) the three induction hypotheses give normal components and nf-vcons applies, its index premise being the stored equation; the neutral case uses nf-ne. For (b), related neutral evidence reflects directly. For (c), zero evidence is fixed. Successor evidence vcons(ζ,η2) is sent to vcons(trγi,γji,j(ωζ),ωη2), where j is the ambient level recorded by the transported vector generator; apply the induction hypothesis to the head at the semantic embedding of γj and to the tail at the transported shorter-length generator. Neutral evidence is transported by neutral equivariance. These are the zero, successor, and neutral clauses; no mixed clause belongs to the element relation.

Universe head. For U^i, claim (a) starts from U^i(d)=Qnc(d). The second stored equation is combined with induction hypothesis (f) at the smaller code-membership derivation. The result is a normal code at Ui; the first stored equation is the conversion. (b): a neutral k with Rn(k) neutral at Ui has Qnc(upU^i(k))=Rn(k),Qn(upU^i(k))=Rn(k). Thus both stored equations are the hypothesis. Claim (c) follows from lemma 111.48.

Neutral type. Claims (a), (b), (e), and (f) are the stored judgments. Claim (c) applies ω to their neutral and equality derivations and then uses transitivity of judgmental equality.

Claims (e)–(h), simultaneously. The induction proves the two quotation-substitution equations in (h), not just their embedding instances. For Unit, Boolean, and natural heads, substitution fixes the nullary quotations. Element evidence is Unit, a Boolean constructor or neutral, or a finite chain of natural successors ending in zero or a neutral. The zero and constructor calculations use the corresponding computation rule. A successor invokes (h) on its smaller predecessor evidence. For neutral evidence, induct on the neutral-readback graph. A variable is exactly one of the obligations of the realizing substitution. Application, the two projections, and the four eliminators apply the induction hypotheses to the stored fields and then use the matching semantic-operation clause. The world-indexed invariant of lemma 111.55 supplies normality after the operation remains stuck. This proves (h), and the identity realizing substitution gives (g); nf-star, nf-true, nf-false, nf-zero, nf-suc, and nf-ne give the displayed normal judgments.

For a product generator supported by Ψ, with n=|Ψ|, first apply the quotation- substitution induction hypothesis to its strict domain premise. To quote the codomain in a target context Γ with semantic classifier telescope Φ and length m, first form the source fresh reflection vn:=(wkΨ,B)B(xn),ζn:(vn,vn)Elt((wkΨ,B)α). Its strict source family premise is βwkΨ,ζn@Ψ.B. Now let wkΦ,σB:ΦΦ.(σB) be target weakening and reflect the fresh target variable at its transported classifier: vm:=(wkσ)B(xm),ζm:(vm,vm)Elt((wkσ)α). The canonical lifted realizing substitution is exactly (σ^,σ). Its defining equation contains no arbitrary-extension notation. Its target is Φ.(σB), its last component is classified there by (wkσ)B, and its semantic action sends vn to vm. The naturality equation for β gives the exact indexed identity (σ)βwkΨ,ζn=βwkσ,ζm:((wkσ)F)(vm)((wkσ)F)(vm). Apply (h) to the strict source premise βwkΨ,ζn under the canonical lifted realizing substitution. The displayed identity is its target index, so the induction hypothesis gives the substituted codomain equation and its normality. Rule nf-ty-pi proves the type parts of (e) and (h). Rule nf-cd-pi proves the code parts of (f) and (h).

It remains to prove the product element clause of (h). Let L:=Π^ϵ,ϱ(B,F)n(d)[σ^]. The outer readback rule makes L a lambda whose body is the source body quotation under the raw part (wkσ^,xm) of the canonical lift (σ^,σ). The target product relation asks about an arbitrary future embedding τ:ΓΓ and arbitrary indexed argument Γτσα,ζbe. Let Φ be the semantic classifier telescope of Γ and let wkτ:ΦΦ be the iterated typed target weakening induced by τ; its action is the τ in the indexed premise. First weaken the target of the realizing substitution along τ, obtaining (τσ^;wkτσ). Then instantiate the source binder by the arbitrary argument be: (111.5)(τσ^,b; wkτσ,e). This is realizing by arbitrary source extension in definition 111.68; its semantic component may contain every gap variable of Γ. Apply (h) at the strict family premise βwkτσ,ζ. It yields Γβwkτσ,ζ,ηwkτσ,ζ(F(vn)n+1(dvn))[τσ^,b]((wkτσ)d)e. By Π-β, the raw term on the left is judgmentally equal to τLϵ,ϱb; by equation 111.3, equation 111.6, its semantic index is exactly the result witness selected by τ(ση). This proves the universal product clause at every future world and every related argument. No inference from the single fresh variable to arbitrary arguments occurs. Rule nf-lam gives normality. Taking (σ^,σ) to be the identity realizing substitution, whose component obligations follow by (b) at the strict support classifiers, proves (g).

For a sum generator, put d1=fstv(d), d2=sndv(d), and let η1,η2 be the recorded component evidence. Under a realizing substitution (σ^,σ), first apply (h) to η1 at α. This gives b1:=Bn(d1)[σ^]withΓσα,ση1b1σd1. Only now is the target fiber selected. Family naturality identifies σ(βidΨ,η1)=βσ,ση1, and the type part of (h) gives the explicit fiber conversion ΓQn(F(d1))[σ^]Qm((σF)(σd1)) type. Transport ση2 across that equality and apply (h) to obtain b2σd2 in precisely this fiber. Rule nf-pair applies after equation 111.7; Σ-η and the two projection equations give the indexed judgment. The same domain-then-fiber calculation proves nf-ty-sg and nf-cd-sg. This is the required dependent transport: the second component is never quoted at an unidentified or unconverted fiber.

For identity, the carrier induction hypothesis gives its substituted quotation. The clique in reflexivity evidence supplies carrier membership for both endpoints and the reflexivity witness. Apply (h) to all three strict carrier witnesses; substitution of the two stored endpoint equations puts their target quotations in the one required identity type. nf-ty-id, nf-cd-id, and nf-refl apply. Neutral identity evidence uses the neutral-graph induction above.

For a vector generator, apply the code part of (h) to its strict code premise and the element part to its length evidence at N^. These are the two substituted premises of nf-ty-vec and nf-cd-vec. At zero, substitution fixes vnil. At successor evidence ζ:(a,a)Elt(γi),η2:(xs,xs)Elt(δν), transport σζ through lemma 111.62(4),(6), apply (h) to the head at the strict semantic embedding of γi, and apply (h) to η2 at the shorter vector generator. Together with the predecessor quotation, nf-vcons gives the substituted result and its index equation. At a neutral length, use the neutral-graph induction. Zero, successor, and neutral are all cases; the successor calls decrease the recorded shorter generator and membership evidence.

For a universe, (e) uses nf-ty-univ; the element part of (h) is the simultaneous code part at the smaller-level code derivation stored as universe membership. Code generators use, in order, nf-cd-K, nf-cd-univ, nf-cd-pi, nf-cd-sg, nf-cd-id, and nf-cd-vec, with their raw substitution equations supplied by the strict premise instances of (h). A code lift invokes (h) at its smaller premise and then nf-cd-lift. A neutral code has endpoint N=upU^i(k) fixed in definition 111.58; its element annotations are N itself, and the neutral-graph induction supplies its substitution equation. Peeling invokes the strict semantic-type premise and changes neither quotation nor element evidence. These cases prove (e)–(h) for every generator and close the simultaneous induction.

Claim (d), uniformly. Choose witnesses for either erased judgment and transport them along AB using lemma 111.66; its converse supplies the reverse implication. The quoted types agree by lemma 111.63(1), so the standing typing premise is preserved by Conv. ◻

Lemma 111.70 — Quotation lands in normal syntax

Let Δ be a context and n=|Δ|. If AT and ΔAQn(A) type for some ΔA type, then ΔQn(A)nftype; if moreover ACi and ΔcQnc(A):Ui for some Δc:Ui, then ΔQnc(A)nfUi.

Proof of Lemma 111.70 — Quotation lands in normal syntax

Proof. Apply lemma 111.69(e) for the type claim and lemma 111.69(f) for the code claim. They were proved in the same well-founded induction as escape and element quotation, so this corollary introduces no reverse dependency. ◻

Exercise 49.15

★★★ Following definition 111.58, define the partial equivalence relation interpreting U0 for the fragment with 2^ and Π^ alone, as an inductive definition of related pairs of codes carrying, by recursion on that definition, the relation on their elements. Where does the ambiguity of remark 49.10 threaten, and what rules it out in your definition?

The fundamental lemma

Everything so far is a definition. The single theorem that turns the definitions into a normalizer is the statement that every derivable judgment of Timpl is valid: its type has a semantic type, its term has an element, judgmentally equal inputs have related outputs, and the syntax stays tied to the semantics by the Kripke relation of definition 111.65. The invariant on environments has to carry all four of those, and it does so in two separate notions, for a reason the definition states.

Definition 111.71 — Related environments and valid pairs

Let Γ be the context x1:A1,,xm:Am, and write ρ<j for the length-(j1) prefix of an environment ρ.

Fix a semantic support telescope Ψ, independently of any syntactic target context. Two Ψ-admissible environments of length m are related over Γ at Ψ, written ρΨρ:Γ, when they carry, for every jm, ranked witnesses αj:[[Aj]]ρ<j[[Aj]]ρ<j@Ψ,ζj:(ρ(j),ρ(j))EltΨ(αj). Formation of the displayed membership judgment supplies the admissibility of both endpoints and of ζj; αj is Ψ-admissible by its own formation. Thus the notation records a common finite initial telescope and not merely an erased binary relation. No theorem reconstructs this index from an erased pair of environments. Instead, the semantic half of the fundamental lemma quantifies over Ψ and over the displayed ranked witnesses at Ψ; each environment extension preserves that same formation index, and only an explicit typed substitution changes it. For a typed relational substitution σ:ΨΦ, componentwise action gives σρΦσρ:Γ; the witnesses are σαj and σζj.

Let Δ be a context with n=|Δ|. A pair (γ,ρ) is valid over Γ in Δ, written Δ(γ,ρ):Γ, when γ assigns to each xj a term with Δγ(xj):Aj[γ], when ρΨΔρ:Γ for the semantic classifier telescope ΨΔ of Δ, and when for every jm Δαj,ζjγ(xj)ρ(j):[[Aj]]ρ<j.

The two notions must be kept apart, and the reason is worth stating, because collapsing them is the natural mistake. An element of Elt(A) need not be the value of any term: nothing in definition 111.58 restricts the relation to definable values. A single invariant carrying both a value and a syntactic witness for it could therefore not be extended by an arbitrary related pair (d,e), and that extension is exactly what the formation and introduction rules of Π and Σ require, since their semantic clauses quantify over all related arguments. Conversely, the syntactic half quantifies over every future argument that comes with a Kripke witness. Fresh reflection supplies the identity environment, while lemma 111.69(h) extends quotation by an arbitrary such argument. The fundamental lemma below therefore has two halves with two different environment notions, and each rule is checked against both.

Lemma 111.72 — Evaluation, weakening, and substitution

Let t be a raw expression with free variables among Γ=(x1,,xm) and let ρ be an environment.

  1. If xm is not free in t, then [[t]](ρ,d)=[[t]]ρ for every d.

  2. For a substitution γ=(a1,,am), [[t[γ]]]ρ=[[t]]([[a1]]ρ,,[[am]]ρ). In particular [[t[a/x]]]ρ=[[t]](ρ,[[a]]ρ).

  3. If σ:ΨΦ and ρ is Ψ-admissible, then [[t]](σρ)=σ([[t]]ρ). Beneath r instantiated source binders, the equation uses the iterated arbitrary extension (σ,e1,,er) of equation 111.2; beneath a fresh target binder it uses the canonical lift σ of equation 111.1. It is natural in every further typed substitution τ:ΦΞ.

Proof of Lemma 111.72 — Evaluation, weakening, and substitution

Proof. Structural induction on t, simultaneously for all three clauses. A variable is lookup: for (1) in the unchanged prefix, for (2) the j-th component [[aj]]ρ by definition. Every non-binding constructor of convention 111.16 evaluates to a value built from the values of its immediate subexpressions by an operation of definition 111.44; the induction hypotheses equate those values, and graph determinism equates the outputs. Every binding constructor evaluates to a finite raw closure. Choosing the bound variable outside dom(γ) and the free variables of its images, the induction hypothesis for b at the extended environment shows that the two closure execution graphs agree on every tuple of arguments. Hence the closures are equal in the contextual quotient of definition 49.36; multi-binder instantiation uses (σ,e1,,er) and repeated equation 111.2; only a new target declaration uses equation 111.1. Naturality is associativity of composition and lemma 111.48(1). The Lift clause is the unary operation lift^, and the symbolic level is unaffected by substitution because levels are external (convention 29.3). ◻

Lemma 111.73 — Semantic lifting

If CiC then lift^i(C)i+1lift^i(C), and the two element relations agree with Elt(CiC).

Proof of Lemma 111.73 — Semantic lifting

Proof. Induction on the derivation of CiC. On 1^,2^,N^ the operation is the identity and the same generator applies at level i+1, whose element clause does not mention the level. On U^j with ji the operation is the identity and ji+1, so the generator applies and the element relation is j either way. On Π^ and Σ^ the operation lifts the domain and every codomain, and the induction hypothesis gives the corresponding derivations at level i+1 with the same element relations, whence the displayed element clauses agree. On Id^ the operation lifts the carrier only, and the endpoints stay related by the induction hypothesis. On the three stuck heads the operation returns Lift^i(), and the lift generator of definition 111.58 applies with Elt unchanged by definition. ◻

Lemma 111.74 — Fundamental lemma for T_ impl

Each clause has two independently quantified halves. Its semantic half is quantified over every finite semantic support telescope Ψ and every ρΨρ:Γ; its output includes the displayed ranked Ψ-admissible witness. Its syntactic half is quantified over every Δ(γ,ρ):Γ, with n=|Δ| and support ΨΔ.

  1. If ΓA type, then there is αA:[[A]]ρ[[A]]ρ@Ψ, and ΔA[γ]Qn([[A]]ρ) type.

  2. If ΓAB type, then there is αA,B:[[A]]ρ[[B]]ρ@Ψ, and ΔA[γ]B[γ] type.

  3. If Γa:A, then there is ζa:([[a]]ρ,[[a]]ρ)EltΨ(αA), where αA is the witness from (a), and Δa[γ][[a]]ρ:[[A]]ρ.

  4. If Γab:A, then there is ζa,b:([[a]]ρ,[[b]]ρ)EltΨ(αA), and both Δa[γ][[a]]ρ:[[A]]ρ and Δb[γ][[b]]ρ:[[A]]ρ.

Proof of Lemma 111.74 — Fundamental lemma for T_ impl

Proof. Simultaneous rule induction on the four judgment forms (remark 26.23); each case discharges both halves. A subsidiary induction on the element derivation is used in the N and Vec elimination cases. In a semantic call, fix the support Ψ carried by ρΨρ; in a syntactic call, independently put n=|Δ| and use ΨΔ. No semantic premise is indexed by n merely because the other half happens to mention Δ. All constructor and closure clauses preserve Ψ-admissibility by lemma 111.48; every output membership judgment contains the two endpoint-admissibility premises of definition 111.58, and all output derivations and membership witnesses carry the assigned ranks. Thus every induction hypothesis used below has a common support and ranked witnesses. Furthermore, lemma 111.62(2) is used silently to speak of the element relation of a pair of related types. Lemma 111.69(d) transports the Kripke relation along and is likewise used silently.

Two extension principles are used repeatedly and are recorded once. Semantic extension: if ρΨρ:Γ, α:[[A]]ρ[[A]]ρ@Ψ and ζ:(d,e)EltΨ(α), then (ρ,d)Ψ(ρ,e):Γ,x:A. The final declaration uses α and ζ; the formation premises of ζ give d,eDΨ, so the two extended environments satisfy the admissibility clause of definition 111.71. Nothing syntactic is required, and d,e are arbitrary among values admissible at Ψ. Syntactic extension: if Δ(γ,ρ):Γ and ΔA[γ]Qn([[A]]ρ) type, then, writing Δ:=Δ,xn:A[γ] and ω:ΔΔ, and v:=ω[[A]]ρ(xn), Δ(ωγ,xn),(ωρ,v):Γ,x:A. Here ΔxnneA[γ] by ne-var, and lemma 111.55 gives xnΨΔnexn at the explicit extended classifier telescope. World equivariance turns the weakened type equation into A[γ]Qn+1(ω[[A]]ρ), so lemma 111.69(b) supplies the Kripke component, while lemma 111.63(4) supplies (v,v) in the element relation.

One half is uniform and is disposed of once: the syntactic half of clause (b), namely ΔA[γ]B[γ] type, is Subst-Eq-Ty applied to the premise ΓAB type and the substitution γ, in every case. The cases below therefore treat only the semantic half of (b).

Structural rules. Var and Assum. Both halves are the corresponding clauses of definition 111.71 at the selected declaration, together with xj[γ]=γ(xj) and [[xj]]ρ=ρ(j).

Wk, Exch, Rename. These change the ambient context without changing the expression. A related environment, respectively a valid pair, for the larger context restricts to one for the smaller by deleting, permuting, or renaming the corresponding components; every clause of definition 111.71 is preserved componentwise, and lemma 111.72(1) identifies the two evaluations.

Subst and Subst-Eq-Ty, Subst-Eq-Tm. Given Γa:A and a judgment in Γ,x:A,Θ, the semantic half of induction hypothesis (c) for a extends ρΨρ by ([[a]]ρ,[[a]]ρ), and its syntactic half extends (γ,ρ) by (a[γ],[[a]]ρ). Applying the induction hypothesis at the longer context and rewriting with lemma 111.72(2) gives the claim for the substituted judgment.

Ctx-Conv. A related environment or valid pair for Γ,x:A,Θ is one for Γ,x:A,Θ when ΓAA type: the type component transports by induction hypothesis (b), the element component by lemma 111.62(2), and the Kripke component by lemma 111.69(d).

Conv and Conv-Eq. Induction hypothesis (b) gives [[A]]ρ[[B]]ρ@Ψ; the element relations coincide by lemma 111.62(2), and the Kripke relation transports by lemma 111.69(d).

The equality rules. Six rules are treated together: Ty-Refl, Ty-Sym, Ty-Trans, Tm-Refl, Tm-Sym and Tm-Trans. The relation ρΨρ:Γ is symmetric and transitive, because and every element relation are (lemma 111.62(1)); so induction hypothesis (d) at the exchanged environments gives symmetry, and composing two instances with the middle term evaluated at a common ρ gives transitivity. On the syntactic side both are symmetry and transitivity of judgmental equality. Reflexivity is (a) and (c), and the presupposition rules follow from (a) and (c) directly.

Π. Π-form and Π-form-eq. Semantic half: induction hypothesis (a) for A gives α:[[A]]ρ[[A]]ρ@Ψ. For every relational substitution σ=(σ0,σ1;q):ΨΦ and every ζ:(d,e)EltΦ(σα), lemma 111.72(3) identifies σ0[[A]]ρ with [[A]](σ0ρ) and likewise on the right. Hence (σ0ρ,d)Φ(σ1ρ,e) is a related environment over Γ,x:A, and induction hypothesis (a) for B gives βσ,ζ:[[B]](σ0ρ,d)[[B]](σ1ρ,e)@Φ. Under a further relational τ, evaluation-substitution and the induction hypothesis identify this derivation with βτσ,τζ, proving equation 111.3. This is the step for which the semantic half must not carry a syntactic witness: d and e range over the whole target-world element relation. The Π^ generator then applies with the pair (ϵ,ϱ) copied unchanged from the syntax; the metadata premise of remark 111.17 is exactly what makes the generator applicable, and a mismatched pair produces no generator at all. Syntactic half: induction hypothesis (a) for A gives ΔA[γ]Qn([[A]]ρ) type; syntactic extension and induction hypothesis (a) for B give ΔB[γ+]Qn+1([[B]](ρ,v)) type, and Π-form-eq assembles the two into the required equation, whose right-hand side is Qn of the semantic product.

Π-intro and λ-eq. Let Γ,x:Ab:B. For the semantic half, fix an arbitrary relational σ=(σ0,σ1;q):ΨΦ and ζ:(d,e)EltΦ(σ[[A]]ρ). Its formation gives d,eDΦ. Apply induction hypothesis (c) at the related environment (σ0ρ,d)Φ(σ1ρ,e). Since (σ0[[λϵ,ϱ(x:A).b]]ρ)ϵ,ϱd=[[b]](σ0ρ,d) by definition 111.44, lemma 111.48, the required left output is [[b]](σ0ρ,d); the identical calculation with σ1,ρ,e gives the right output. The required product membership witness is therefore that induction hypothesis. Its naturality in a further substitution is the evaluation-substitution equation, so the universal product evidence is fully supplied. For the Kripke half, let ω:ΔΔ and Δce:ω[[A]]ρ. Extend the transported pair (ωγ,ωρ) by (c,e). It is a valid pair over Γ,x:A: its Kripke component is the hypothesis, and its element component (e,e)EltΨΔ(ω[[A]]ρ) is the transported domain membership supplied by lemma 111.64. Induction hypothesis (c) then gives Δb[ωγ,c/x][[b]](ωρ,e); rule Π-β gives Δω(λϵ,ϱ(x:A[γ]).b[γ+]))ϵ,ϱcb[ωγ,c/x]:, and lemma 111.69(c) transports the relation along it.

Π-elim and app-eq. Induction hypothesis (c) for f and for a, the element clause at Π^, and the Kripke clause at Π^ taken at Δ=Δ give both halves at the semantic type [[B]](ρ,[[a]]ρ), which is [[B[a/x]]]ρ by lemma 111.72(2). This is the case that defeated the induction on derivations in section 111.6; it goes through here because the induction hypothesis for f is a statement about all related arguments, not about one syntactic subterm.

Π-β. The left side evaluates to [[b]](ρ,[[a]]ρ) and the right side to [[b[a/x]]]ρ, which is [[b]](ρ,[[a]]ρ); the two are related by induction hypothesis (c) at the extended pair. The two Kripke statements are the ones just proved for the two sides.

Π-η. Here the two values are not equal: [[f]]ρ may be up(k) while [[λϵ,ϱ(x:A).fϵ,ϱx]]ρ is a lam value. They are nevertheless related, and this is the clause for which the element relation at Π^ was made extensional. Fix arbitrary σ=(σ0,σ1;q):ΨΦ and ζ:(d,e)EltΦ(σ[[A]]ρ). Then σ0([[f]]ρ)ϵ,ϱdandσ1([[λϵ,ϱ(x:A).fϵ,ϱx]]ρ)ϵ,ϱe=σ1([[f]]ρ)ϵ,ϱe, the equality by definition 111.44 and lemma 111.72(1), and the two are related by induction hypothesis (c) for f at the substituted related environments. This construction is natural in a further target substitution by lemma 111.48; hence it is product evidence, not merely base-world pointwise evidence. On the Kripke side, Π-β and lemma 111.69(c) again transport.

Σ. Σ-form. Let α:[[A]]ρ[[A]]ρ@Ψ. For every relational σ=(σ0,σ1;q):ΨΦ and ζ:(d,e)EltΦ(σα), semantic extension and the induction hypothesis for B give βσ,ζ:[[B]](σ0ρ,d)[[B]](σ1ρ,e)@Φ. Evaluation-substitution proves τβσ,ζ=βτσ,τζ, so these are exactly the domain and natural dependent-family premises of the Σ^ generator. Syntactic formation uses the same construction at the self-related environment and the type-quotation clause of lemma 111.69(e).

Σ-intro and pair-eq. Put a0=[[a]]ρ, a1=[[a]]ρ. The induction hypothesis for a supplies η1:(a0,a1)EltΨ(α). Only after this first-component witness is fixed do we extend the environments and apply the induction hypothesis for b, obtaining η2:([[b]](ρ,a0),[[b]](ρ,a1))EltΨ(βidΨ,η1). The pair (η1,η2) is precisely the dependent-sum element evidence. At a valid syntactic environment the two self-witnesses give Δα,η1pr1((a[γ],b[γ]))a0,ΔβidΨΔ,η1,η2pr2((a[γ],b[γ]))[[b]](ρ,a0). The first uses Σ-β1; that equation selects the fiber βidΨΔ,η1 in which the second judgment lives, and then Σ-β2 supplies the second equation. Thus the dependent transport is determined before the second component is checked.

Σ-elim1, Σ-elim2, and projection congruence. If the induction hypothesis for p supplies sum evidence (η1,η2), the first projection uses η1 at α. Put p1=fstv([[p]]ρ). The second projection uses η2 at βidΨ,η1, and lemma 111.72(2) identifies that semantic fiber with [[B[pr1p/x]]]ρ. The two Kripke premises in definition 111.65 have exactly these indices. Projection congruence transports η1 first and then the selected η2. The two β-rules are literal equalities of values together with the two indexed judgments displayed above.

Σ-η. As for Π: the two values [[p]]ρ and pair(fstv[[p]]ρ,sndv[[p]]ρ) need not be equal, but their semantic projections are, so they are related by the element clause at Σ^. More explicitly, the first projection uses the stored η1 and thereby fixes p1; the second uses the stored judgment η2:(sndv[[p]]ρ,sndv[[p]]ρ)EltΨ(βidΨ,η1). On the syntactic side the Kripke clause at Σ^ uses these two indexed witnesses, and Σ-β1,2 identify the projections of the reconstructed pair with the projections of p[γ], so lemma 111.69(c) transports the relation from one to the other.

1. 1-form, 1-intro, 1-η. The generator 1^ has EltΨ=DΨ×DΨ. Evaluation at related Ψ-admissible environments produces Ψ-admissible values by lemma 111.48, so the two endpoint formation premises construct the Unit membership evidence. The Kripke clause at 1^ imposes only the typing that the judgment supplies. 1-η is therefore valid without inspecting either value. This is the only former whose element relation deliberately relates every pair admissible at the displayed support; that coarseness is the semantic content of 1-η and is the reason section 111.6 showed why it cannot be implemented by rewriting.

2. Formation, 2-intro1,2. The generator 2^ applies, and tt^, ff^ are related to themselves; the Kripke clauses are reflexivity of judgmental equality.

2-elim and its congruence. Induction hypothesis (c) for the scrutinee b puts ([[b]]ρ,[[b]]ρ) in Elt(2^), so exactly one of three cases holds. If both are tt^, then ifv selects [[ct]]ρ and [[ct]]ρ, related by induction hypothesis (c) at [[C]](ρ,tt^)=[[C[tt/x]]]ρ, which is [[C[b/x]]]ρ because [[b]]ρ=tt^. On the syntactic side the Kripke clause for b gives Δb[γ]tt:2, so the eliminator congruence and 2-comp1 give ind2(x.C[γ+];ct[γ],cf[γ],b[γ])ct[γ], and lemma 111.69(c) transports. If both values are ff^, then ifv selects the two interpretations of cf. Induction hypothesis (c) relates them in the fiber [[C]](ρ,ff^)=[[C[ff/x]]]ρ=[[C[b/x]]]ρ. The Kripke clause for b gives Δb[γ]ff:2; eliminator congruence and 2-comp2 therefore give ind2(x.C[γ+];ct[γ],cf[γ],b[γ])cf[γ], after which lemma 111.69(c) transports. If both values are related neutrals up(k), up(k), then ifv returns two ind2^ nodes; they are Ψne because their readbacks agree after every typed future weakening from Ψ, by lemma 111.63(1) on the quoted motive and (3) on the two reified branches, and by hypothesis on the principal argument. The Kripke half uses ne-ind-bool: its motive and branch premises are normal by lemma 111.70 and lemma 111.69(a), and the eliminator congruence identifies ind2(x.C[γ+];,b[γ]) with the readback of the neutral node.

2-comp1,2. Literal equality of values, as computed above, together with the two Kripke statements.

N. Formation, N-intro1,2. As for 2, with suc^ applied to the induction hypothesis for the predecessor.

N-elim and its congruence. Induction hypothesis (c) puts ([[m]]ρ,[[m]]ρ) in Elt(N^), an inductively generated relation; induct on that derivation. At (0^,0^), recv selects the base branch and N-comp1 matches it syntactically. At (suc^(d),suc^(e)) over a smaller derivation, recv returns [[cs]]ρdrecv(;d); induction hypothesis (c) for cs at the Π-type StepN(C) of definition 28.21—which in Timpl carries the pair (exp,runtime), as recv does—applied twice, once at the related predecessors, once at the pair supplied by the subsidiary induction hypothesis—gives the element claim, and N-comp2 together with the Kripke clause at Π^ gives the syntactic one. At related neutrals, the argument is the neutral case of 2 with ne-ind-nat in place of ne-ind-bool and with the step branch reified at the semantic value of StepN.

Intensional identity. Id-form, Id-form-eq. The Id^ generator, from induction hypothesis (a) for A and (c) for the two endpoints.

Id-intro. Evaluation gives [[refla]]ρ=refl^([[a]]ρ), and the element clause requires the six values contributed by the two equal endpoints and the two witnesses to form one Elt([[A]]ρ)-clique. They are just copies of [[a]]ρ and [[a]]ρ. Induction hypothesis (c) supplies the cross pair; symmetry and transitivity from lemma 111.62 supply all ordered pairs in the clique. On the Kripke side, refla[γ] is the required witness, and the two endpoint equations demanded by definition 111.65 hold because [[A]]ρ([[a]]ρ) is judgmentally a[γ] by lemma 111.69(a).

Id-elim, Id-elim-eq, Id-comp. Induction hypothesis (c) for the eliminated proof q gives two cases. If both values are refl^(d), refl^(e) with (d,e) related, then jv returns [[c]](ρ,d) and [[c]](ρ,e), related by induction hypothesis (c) for c at the extended pair. Syntactically, the Kripke clause supplies b with Δq[γ]reflb: and, by its two endpoint equations, Δa[γ]b:A[γ] and Δb[γ]b:A[γ] for the two annotations; so Id-elim-eq replaces q[γ] by reflb and both annotations by b, and Id-comp then contracts the result to c[γ,b/z]. Those two endpoint equations are exactly why definition 111.65 stores them: without them Id-comp is not applicable, since its conclusion is stated at annotations equal to the refl argument. If both values are related neutrals, the two J^ nodes are Ψne by lemma 111.63 on the quoted motive, the quoted carrier, the two reified endpoints and the reified branch, and ne-J makes the syntactic eliminator neutral.

Universes and lifts. U-Form. [[U]]ρ=U^i with i=, related to itself. Quotation returns U, which is schema-equal to U by the symbolic normalization theorem lemma 111.19; no parameter assignment is chosen.

U-Hier. For ji, U^jiU^j is a generator, so U^jElt(U^i); both quotations return Uj. The strictness of the hierarchy is exactly the side condition ji on that generator: no generator places upU^j(k) in Ci for ij.

U-El, U-El-Eq. Induction hypothesis (c) at Ui gives [[A]]ρCi and, by the Kripke clause at U^i, the type equation ΔA[γ]Qn([[A]]ρ) type. Lemma 111.62(4) turns the code relation into a type relation with the same elements, which is claim (a); U-El-Eq is the same step from (d) to (b).

U-Pi, U-Sig, U-Unit, U-Bool, U-Nat, Id-form-U, Vec-form, and their congruences. Each is the corresponding generator of definition 111.58 at the level named in the rule, applied to the induction hypotheses for the components at that same level. On the Kripke side, the clause at U^i has two equations; the first is proved by the code congruence of the rule together with the induction hypotheses at Ui, the second by the type congruence together with claim (a). Vec-form is the case where the two equations genuinely differ, because Qnc retains a lift in the element code that Qn would delete (remark 111.21).

Lift-U, Lift-Cong. Lemma 111.73 gives lift^i([[A]]ρ)Ci+1 with the same elements, and the Kripke code equation is Qnc(lift^i([[A]]ρ)), which the five clauses of lift^ match against the five contraction instances by lemma 111.23(3).

Lift-El. Claim (b) at ΓLiftAA type is lift^i([[A]]ρ)[[A]]ρ, which is lemma 111.62(5) followed by transitivity. The peeling generators of definition 111.59 exist for exactly this rule.

Lift-Pi, Lift-Sig, Lift-Id, Lift-Unit, Lift-Bool, Lift-Nat, Lift-Hier. Each is a literal equality of values: lift^i is defined by exactly those seven clauses, and lemma 111.72 shows that the right-hand side evaluates to the same value. For example, writing P:=x:Aϵ,ϱB and P:=x:LiftAϵ,ϱLiftB, [[P]]ρ=Π^ϵ,ϱ(lift^i[[A]]ρ,ρ;x.LiftB)=Π^ϵ,ϱ(lift^i[[A]]ρ,liftcli(ρ;x.B))=lift^i([[P]]ρ). The middle equality is equality of closure-execution graphs, hence equality in the contextual quotient of definition 49.36. There is no clause for Vec, and none is needed, because the signature has no equation there.

Vectors. Vec-form. The universe induction hypothesis for the element code gives γi:CiC; the induction hypothesis for the length gives ν:(dm,dm)Elt(ni). These two witnesses generate Vec^(C,dm)iVec^(C,dm). Its semantic embedding is obtained by lemma 111.62(4), with the head membership map of part (6). The syntactic code equation retains the element code through Qc and quotes the index through element quotation; these are exactly the two premises of Vec-form.

The two constructor rules. At zero length, the vector generator contains (vnil^,vnil^) and the Kripke clause stores both m0 and vnilvnil. At successor length, induction gives ζ:(a0,a1)Elt(γi),ηxs:(xs0,xs1)Elt(δν), where ν is predecessor evidence and δν is the shorter vector generator. If the right element-code premise is recorded at level j, transport ζ by trγi,γji,j before forming the right constructor. The vector-successor membership constructor then yields (vcons^(dm,a0,xs0),vcons^(dm,a1,xs1))Elt(δsuc(ν)). The syntactic clause stores the reified predecessor, head, and tail equations; Vec-intros identifies its result index with suc(m).

Vec-elim and its congruence. Induction hypothesis (c) for the index m and for the vector ys gives related values; induct on the derivation of the length relation, a derivation in the inductively generated relation Elt(N^).

If the vector values are related neutrals upV(k), upV(k), the first clause of vrv applies on both sides and returns two vind^ nodes. Their stored fields are related: the motives and the two branches by the induction hypotheses, the stored vector types V,V by induction hypothesis (a) for the type of ys, the index values by induction hypothesis (c) for m. Hence, after every typed future weakening, their readbacks agree at the exact target-support depth by lemma 111.63(1)–(3), which gives the required self-related and cross-related neutral evidence, not merely equality at the ambient depth. Syntactically, ne-vind makes the eliminator neutral: its element-code premise is lemma 111.70, its motive and branch premises are lemma 111.69(a) and lemma 111.70, its index premise is lemma 111.69(a) at N^, and its principal premise is the Kripke clause for ys.

Otherwise the vector values are constructors, and the length derivation decides which. At (0^,0^) they are vnil^, the second clause returns the base branch, and the Vec-elim congruence followed by Vec-comp1 performs the same replacement syntactically, using the Kripke equations Δm[γ]0:N and Δys[γ]vnil:. At (suc^(d),suc^(e)) they are vcons^ nodes, the third clause applies the four-argument map G to the predecessor pair (d,e), the transported head pair trγi,γji,j(ζ), the tail pair ηxs, and the recursive pair supplied by the subsidiary induction hypothesis at δν. Applying the semantic induction hypothesis for the successor method in that order selects the dependent result fiber F(suc^(d),vcons^(d,a,xs)) on the left and its related fiber on the right. Syntactically, Vec-comp2 performs exactly those four substitutions [m/n,c/a,ys/xs,r/q], its recursive occurrence r matching the recursive semantic call. The remaining combination—a neutral index with a constructor vector—cannot occur, because the element relation of definition 111.58 at a vector type of related neutral length contains only related neutrals; that is why vrv needs no clause for it and why definition 49.14 has no neutral rule for it.

Vec-comp1,2. The two computations displayed above are literal equalities of values.

Every rule of Timpl named in convention 111.16 has now been treated. No case was deferred, and the three cases that are not literal equalities of values—Π-η, Σ-η, 1-η—are precisely the three for which the element relations were made extensional. ◻

Lemma 111.75 — The identity environment is valid

For every derivable context Γ ctx, the identity environment ρΓ of definition 49.37 satisfies ρΓΨΓρΓ:Γ, and Γ(ι,ρΓ):Γ where ι is the substitution fixing every variable.

Proof of Lemma 111.75 — The identity environment is valid

Proof. Induction on the length of Γ. The empty case is the empty pair. Suppose the claim for Γ and let ΓA type, so that Γ,x:A is derivable. By lemma 111.74(a) at the induction hypothesis, A:=[[A]]ρΓ is a semantic type and ΓAQn(A) type with n=|Γ|. Let ω:ΓΓ,x:A. World equivariance moves the equation to Γ,x:A, where ne-var gives Γ,x:AxneA and hence, after conversion, Γ,x:AxneQn+1(ωA). The fresh level is the final declaration of ΨΓ,x:A. Hence xnΨΓ,x:Anexn by lemma 111.55, and lemma 111.69(b) gives Γ,x:AxωA(xn):ωA. Moreover, lemma 111.63(4) gives (ωA(xn),ωA(xn))EltΨΓ,x:A(ωA). This pair is both the element component of ρΓ,x:A and the standing requirement of definition 111.65. The earlier components are inherited from the induction hypothesis by lemma 111.69(c) at ω, using reflexivity for the target conversion. ◻

Normalization, canonicity, and the kernel’s conversion interface

The three targets of section 111.4 are now assembled from the fundamental lemma, in the order Target N, Target C, Target D, each followed immediately by its proof.

Theorem 111.76 — Normalization for T_ impl

Timpl satisfies the package () of convention 111.28. More precisely, for every derivable context Γ ctx, every ΓA type, and every Γa:A, the indexed normalizers of definition 49.37 are idempotent: nfΓA(nfΓA(a))=nfΓA(a),nfΓ(nfΓ(A))=nfΓ(A).

Proof of Theorem 111.76 — Normalization for T_ impl

Proof. Let Γa:A with n=|Γ|. By lemma 111.75 the pair (ι,ρΓ) is valid, where ι fixes every variable, so the syntactic half of lemma 111.74(c) gives Γa[[a]]ρΓ:A,A:=[[A]]ρΓ, using a[ι]=a. Lemma 111.69(a) makes nfΓA(a)=An([[a]]ρΓ) a normal form of type Qn(A) with ΓanfΓA(a):Qn(A), and lemma 111.74(a) gives ΓAQn(A) type, so Conv moves the equation to A and lemma 111.70 makes nfΓ(A)=Qn(A) a normal type. That is clause (1) and clause (2) of ().

For clause (3), let Γab:A. The semantic half of lemma 111.74(d) at the related environments ρΓρΓ gives ([[a]]ρΓ,[[b]]ρΓ)Elt(A), and lemma 111.63(3) turns that into nfΓA(a)=nfΓA(b) as raw expressions. Conversely, if the two normal forms are α-equal, then clause (2) and transitivity give Γab:A. For types, run the same three sentences with clause (d) replaced by lemma 111.74(b), Elt(A) by , and lemma 111.63(3) by lemma 111.63(1). Computability of nf is remark 49.35, whose one open point—totality on well-typed input—has just been proved: along a valid pair every semantic operation invoked has a unique output, and every readback invoked is defined by lemma 111.63.

Idempotence follows from (2) and (3): ΓanfΓA(a):A, so applying (3) to that equation gives nfΓA(nfΓA(a))=nfΓA(a), and likewise for types. ◻

Idempotence says only that renormalizing changes nothing. The sharper statement is that the normal forms are exactly the fixed points.

Lemma 111.77 — Stability

Let Δ be a derivable context, n=|Δ|, and write [[]] for [[]]ρΔ.

  1. If ΔAnftype then Qn([[A]])=A.

  2. If ΔcnfU then Qnc([[c]])=c.

  3. If ΔvnfA then [[A]]n([[v]])=v.

  4. If ΔuneA then [[u]]=[[A]](k) for a neutral value k with Rn(k)=u.

Consequently nfΔA(v)=v for normal v and nfΔ(A)=A for normal A, so each judgmental-equality class contains exactly one normal form.

Proof of Lemma 111.77 — Stability

Proof. Simultaneous induction on the four derivations of definition 49.14. Each is well typed by lemma 111.26(2), so lemma 111.74 applies to it and every semantic type mentioned is a semantic type. Two facts are used throughout: ρΔ,x:A=(ρΔ,vn[[A]]) by definition 49.37, and [[Aj]]ρ<j=[[Aj]]ρΔ by lemma 111.72(1).

(d), ne-var: [[xj]]=ρΔ(j)=[[Aj]](xj) and Rn(xj)=xj.

(d), ne-app: by the induction hypothesis [[u]]=Π^ϵ,ϱ(A0,F)(k), which definition 49.37 unfolds to etaϵ,ϱ(k;A0;F). Applying it to [[v]] gives F([[v]])(app(k;A0;[[v]])), and F([[v]])=[[B[v/x]]] by lemma 111.72(2). Its readback is Rn(k)ϵ,ϱA0n([[v]]), which the induction hypotheses (d) and (c) turn into uϵ,ϱv.

(d), ne-fst, ne-snd: reflection at Σ^ is a pair of two reflections, so the semantic projections return them, and Rn prefixes pr1 or pr2.

(d), ne-ind-bool, ne-ind-nat, ne-J, ne-vind: the induction hypothesis makes the principal argument upB(k), so the corresponding clause of definition 111.44 builds a stuck node whose readback rebuilds the syntactic eliminator. Its motive is quoted at the extended level and equals the stored motive by induction hypothesis (a); its minor arguments are reified at the semantic types of their declared classifiers—for 2 these are F(tt^) and F(ff^), equal to [[C[tt/x]]] and [[C[ff/x]]] by lemma 111.72(2)—and equal the stored arguments by induction hypothesis (c). For ne-vind the element code is recovered from the semantic vector type stored in upB(k), which is [[Vec(c,w)]]=Vec^([[c]],[[w]]), and induction hypothesis (b) returns c.

(c), nf-lam: [[λϵ,ϱ(x:A).v]]=lamϵ,ϱ(ρΔ;x.v), and reification emits λϵ,ϱ(xn:Qn([[A]])).F(v)n+1([[v]](ρΔ,v)) with v=vn[[A]]. The domain is A by induction hypothesis (a)—which is available exactly because nf-lam carries the premise ΔAnftype—and the body is v by induction hypothesis (c) in Δ,x:A, whose identity environment is (ρΔ,v).

(c), nf-pair: the semantic projections of a pair are its components, and the two induction hypotheses return v and w.

(c), nf-star, nf-true, nf-false, nf-zero, nf-suc, nf-refl, nf-vnil, nf-vcons: reification emits the same constructor and reifies each stored field at the semantic type of its declared classifier, so the induction hypotheses return the stored fields.

(c), nf-ne: by (d), [[u]]=[[A]](k), and at a positive head reflection is up[[A]](k), whose reification is Rn(k)=u.

(a) and (b): each rule of the two normal families is matched by the clause of definition 49.37 for the corresponding value head. For nf-ty-vec the code is requoted by Qnc and the length reified at N^, returning c and v by (b) and (c); for nf-ty-ne the value is upU^(k) by (d) and Qn returns Rn(k)=u. For nf-cd-lift, induction hypothesis (b) shows that [[c]] has one of the three stuck heads—a neutral code, a Vec^, or a Lift^—so lift^ wraps rather than computes, and Qnc emits Lift(c).

The final claim combines (a) and (c) with the definition of nf; uniqueness of the normal form in an equality class then follows from theorem 111.76(3). ◻

Remark 49.38 — Correctness architecture

It is worth separating the three properties, because they are proved by three different mechanisms and only the first two are usually named. Soundness, Γanf(a):A, comes from the Kripke relation between syntax and values and its escape lemma (lemma 111.69(a)); nothing about partial equivalence relations enters it. Completeness, abnf(a)=nf(b), comes from the partial equivalence relations on values and the reification lemma (lemma 111.63); nothing about syntax enters it, and it is the direction that fails for a naive value domain in which η is not built into reification. Stability, nf(v)=v, comes from neither: it is the induction of lemma 111.77 over the normal and neutral rules. A development that proves only the first two has a normalizer; a development that proves all three has canonical representatives.

Theorem 49.18 — Canonicity and canonical forms

In Timpl:

  1. every closed b:2 is judgmentally equal to exactly one of tt,ff;

  2. every closed n:N is judgmentally equal to sucm(0) for exactly one mN;

  3. every closed p:IdA(a,b) satisfies ab:A and prefla:IdA(a,b);

  4. every closed xs:Vec(c,n) with nsucm(0):N is judgmentally equal to an m-fold vcons chain ending in vnil;

  5. every Γf:x:Aϵ,ϱB is judgmentally equal to λϵ,ϱ(x:A).fϵ,ϱx, every Γp:x:AB to (pr1(p),pr2(p)), and every Γt:1 to , in an arbitrary context Γ.

Proof of Theorem 49.18 — Canonicity and canonical forms

Proof. Item (5) is Π-η, Σ-η, and 1-η read as they stand; it is recorded beside the others because it is the exact sense in which a negative former has canonical forms, and because it is the only one of the five that does not need the empty context.

For the other four, work in the empty context, where ρ is the empty environment and, by lemma 111.26(3), no expression is neutral. Consequently no clause of definition 111.65 that requires R0(k)ne can hold: its premise is a neutral judgment in the empty context.

(1) Let b:2. The syntactic half of lemma 111.74(c), at the valid pair of lemma 111.75 for the empty context, gives b[[b]]ρ:2^, and the neutral case is excluded, so btt:2 or bff:2. They are not both derivable: otherwise ttff, and theorem 111.76(3) would give nf(tt)=nf(ff), that is tt=ff as raw expressions. (Proposition 49.3 proves the same separation by a two-point model and without the present construction.)

(2) Run the argument of (1) with 2^ replaced by N^ and its two constructor cases by the two generators 0^ and suc^, adding an induction on the derivation that [[n]]ρ is related to itself: the neutral case is excluded, so the value is suc^m(0^) for some mN, and the Kripke clauses compose m successor equations into nsucm(0):N. Uniqueness of m again follows from clause (3) of (), since distinct numerals are distinct raw expressions.

(3) Let p:IdA(a,b). The neutral case at Id^ is excluded, so [[p]]ρ=refl^(d) and there is c with preflc:IdA(a,b) together with the two stored endpoint equations of definition 111.65, which after lemma 111.74(a) and Conv read ac:A and bc:A. Symmetry and transitivity give ab:A, and the Id-intro congruence along ca:A then identifies reflc with refla at IdA(a,b).

(4) Let xs:Vec(c,n) with nsucm(0):N. By (2) the length value is suc^m(0^); induct on m. At m=0 the neutral case is excluded and the clause gives xsvnil:. At m+1 it gives xsvcons(sucm(0),b1,b2): with b2 a closed vector of length sucm(0), to which the induction hypothesis applies. ◻

Corollary 49.20 — Decidability

Given derivations of the inputs as in remark 48.7, the judgments ΓAB type and Γab:A are decidable in Timpl; equivalently, Timpl has an effective conversion invariant in the sense of definition 48.8.

Proof of Corollary 49.20 — Decidability

Proof. Given derivations of Γa:A and Γb:A, compute nfΓA(a) and nfΓA(b) and compare them for α-equality. Both computations terminate by theorem 111.76; the outputs are finite binding trees whose only non-syntactic data are external level expressions, and α-equality of such trees is decidable by convention 26.8 together with lemma 111.19(2) for the level indices. Soundness and completeness of the test are clauses (2) and (3) of (). Types are decided in the same way. Proposition 48.9 converts the decision procedure into an effective conversion invariant, and conversely the encoded normal form is one directly. ◻

The kernel of chapter 48 asked for six operations, not two, and asked for them at the full signature. All six are now definable.

Theorem 111.81 — The Timpl conversion interface

At Timpl the six operations hypothesized in definition 48.16 exist and are total computable: ΓAB type,Γab:A,unPiMeta(Γ,C),unSg(Γ,C),unId(Γ,C),unUniv(Γ,C). The two conversion queries are sound and complete for judgmental equality. Each inversion operation returns the constructor arguments together with a judgmental equality to C, coherently with every other presentation of C in the sense of definition 48.10, or correctly reports that no such presentation exists.

Proof of Theorem 111.81 — The Timpl conversion interface

Proof. The two conversion queries are the decision procedure of corollary 49.20.

For unPiMeta(Γ,C), compute V:=nfΓ(C). If V=x:A0ϵ,ϱB0, return (ϵ,ϱ,A0,x.B0) together with ΓCx:A0ϵ,ϱB0 type, which is clause (2) of (). Otherwise report failure. Failure is correct: if ΓCx:Aϵ,ϱB type held, clause (3) would give V=nfΓ(x:Aϵ,ϱB), and that normal type has a Π head, because [[x:Aϵ,ϱB]]ρΓ=Π^ϵ,ϱ(,) and Qn of a Π^ value is a Π-type carrying the same two bits.

Coherence is Π-injectivity, which the same two clauses supply. Suppose ΓCx:Aϵ,ϱB type and ΓCx:Aϵ,ϱB type. Clause (3) makes the two normal types the same raw expression; in particular (ϵ,ϱ)=(ϵ,ϱ), and the two displayed domains have the same normal form, so clause (2) and transitivity give ΓAA type. Context conversion along that equality puts B in Γ,x:A, where the two codomains again have the same normal form, whence Γ,x:ABBA type. This is exactly definition 48.10.

unSg and unId repeat the argument with the heads Σ^ and Id^, whose quotations are Σ-types and identity types; for unId the two endpoints returned are the reified ones, and coherence follows because clause (3) identifies them as raw expressions. For unUniv(Γ,C), compute V; if V=Ui return i, else fail. Correctness of the returned level uses lemma 111.19(2): two level expressions name the same universe exactly when their normal forms agree, so the returned i is unique. Failure is correct by the same head argument, and unUniv is an executable operation rather than an unbounded search for i. ◻

Corollary 111.82 — The kernel is unconditional

Every theorem of chapter 48 whose statement is conditional on totality of the six operations of definition 48.16 holds unconditionally at Timpl; in particular the determinism, soundness, and completeness statements proposition 48.17, theorem 48.19, theorem 48.20, and the termination conclusion of proposition 110.17, hold with actual algorithms in place of every assumed oracle. Consequently bidirectional type-checking for Timpl is decidable, and demands (D1), (D2), and (D4) of remark 48.14 are met at that signature.

Proof of Corollary 111.82 — The kernel is unconditional

Proof. Theorem 111.81 constructs the six operations with exactly the modes, presuppositions, soundness, completeness, and universal-coherence properties assumed in definition 48.16. Discharging a hypothesis of a conditional theorem yields its conclusion. (D1) is corollary 49.20 through proposition 48.9; (D2) is the inversion half of theorem 111.81; (D4) is theorem 49.18. ◻

Remark 49.22 — Injectivity and inversion discharged

Π-head injectivity for Timpl is proved inside theorem 111.81 and is not assumed anywhere. Two boundaries remain visible in that proof. First, injectivity is a consequence of completeness of nf, not of any confluence or subject-reduction property: lemma 111.23 is never used for it. Second, the inversion operations invert normal-form heads, and for Vec that head stores a code rather than a type. An operation unVec—which chapter 48 does not require—would therefore distinguish Vec(A,n) from Vec(LiftA,n), and correctly so: by remark 111.21 those two are not judgmentally equal types. It is the deleted lift of Lift(Vec(A,n)), not the one inside a Vec, that a type-level inversion may discard.

Example 111.84 — The two lifts of a vector type

Let Γ:=(X:U0, n:N), so |Γ|=2 and [[X]]ρΓ=X:=upU^0(x0), [[n]]ρΓ=ν:=upN^(x1). Evaluating and quoting the two expressions of remark 111.21 as types gives nfΓ(Lift0(Vec(X,n)))=Q2(Lift^0(Vec^(X,ν)))=Vec(X,n),nfΓ(Vec(Lift0X,n))=Q2(Vec^(Lift^0(X),ν))=Vec(Lift0X,n), because Q2 deletes an outer lift and Q2c, which the vector clause uses on the element, keeps one. Quoting the same two expressions as codes at U1 gives Lift0(Vec(X,n)) and Vec(Lift0X,n). So the kernel accepts ΓLift0(Vec(X,n))Vec(X,n) type and rejects both ΓVec(Lift0X,n)Vec(X,n) type and ΓLift0(Vec(X,n))Vec(Lift0X,n):U1. All three answers are correct for the signature as definition 29.10 leaves it.

Remark 49.39 — The demands of ch:trusted-kernels, discharged

The theorem package () is proved for Timpl and for nothing larger. Four boundaries are worth naming exactly, because later chapters inherit them.

Inside. All eight former families of convention 111.16 are covered by one simultaneous construction: Π with its two metadata bits, Σ, 1, 2, N, intensional identity with J, the strict Russell universes with their lifts, and the vector family with vind. They had to be treated simultaneously: the element relation of each former is defined in terms of the element relations of the others, and the recursion is founded on the paired-level multiset and Hessenberg rank sum of lemma 111.62, not on any one former. Discharging them one at a time would not have been possible.

Outside: W and coinduction. Timpl contains no W-type and no coinductive former. Adding W would require an additional ordinal component in the induction measure—a rank on semantic subtrees—and a new element clause inductive in those subtrees; adding a coinductive former would require the dual and a productivity condition. Neither is carried out here, so no statement of this chapter applies to Timpl-co.

Outside: a neighbouring signature. Theorem 49.17 remains confined to TCoq and is used for nothing above; the proofs of theorem 111.76, theorem 49.18, corollary 49.20, theorem 111.81 cite only results of this book. In particular the universe and identity cases of lemma 111.74 are proved locally.

Outside: extensional type theory, and conservativity. The construction uses Id-comp at refl and nothing stronger; adding equality reflection destroys the theorem at its root, by theorem 35.49, corollary 48.48. In the other direction, () is what convention 110.16 named as the missing ingredient for conservativity of Timpl over the proof fragment Tel, but it is not by itself that conservativity: one would still have to show that the normal form of a Tel judgment mentions no 2, no vector, and no metadata bit, a subformula argument that this chapter does not carry out.

Remark 111.86 — Specification versus kernel conversion

Normalize-and-compare is the executable specification supplied by corollary 49.20, not the usual production strategy. Kernels weak-head normalize both sides in the sense of definition 111.22, compare the exposed heads, recurse only into the necessary components, and unfold stored definitions lazily. Theorem 111.76(3) proves that any such sound and complete head-directed comparison decides the same relation, and lemma 111.23(3)–(4) is what makes a head-directed strategy sound and deterministic in the first place. Avoiding the construction of full normal forms is essential for large terms with expensive computations.

Remark 49.21 — The extensional contrast

By theorem 35.49, corollary 48.48, judgmental equality in extensional type theory is undecidable and ETT admits no effective conversion invariant. The latter corollary already discharges the recursive-signature hypotheses of proposition 48.9. The culprit is equality reflection (definition 35.1): a derivation of a judgmental equality may bury an arbitrary proof of an identity, so equality of terms inherits the full strength of provability (theorem 35.9, [Hof95]). This is the precise cost of ETT recorded in chapter 35, and it is the exact complement of corollary 49.20: the two signatures differ by one rule.

Example 111.88 — Two Boolean functions that agree pointwise

Work in the empty context and put f:=λϵ,ϱ(x:2).x and g:=λϵ,ϱ(x:2).ind2(y.2;ff,tt,ind2(y.2;ff,tt,x)). Evaluating and reifying at 22 introduces one reflected variable, v:=up2^(x0). For f the semantic function returns v, so nf22(f)=λϵ,ϱ(x0:2).x0. For g the inner ifv is stuck on v and returns up2^(k1) with k1=ind2^(;y.2;ff^;tt^;x0); the outer one is stuck on that and returns up2^(k2) with k2=ind2^(;y.2;ff^;tt^;k1). Hence nf22(g)=λϵ,ϱ(x0:2).ind2(x1.2;ff,tt,ind2(x1.2;ff,tt,x0)), a different raw expression. By theorem 111.76(3), fg:22 is therefore not derivable, although fttgtt and fffgff by theorem 49.18(1) and two Boolean computations. The clause that separates them is the reflected variable of definition 49.37: it is the one argument at which the two functions cannot be compared by computation.

Remark 111.89 — Function extensionality is still independent

Example 111.88 exhibits two pointwise-equal Boolean functions that are not judgmentally equal, which is what makes a function extensionality axiom meaningful. It is not a proof that the axiom is independent. The expected independence statement says that there is no closed term of type A:U0B:AU0FunextA,B in the intensional theory of chapter 26chapter 30. That theory is not Timpl: it contains 0, binary sums, and W-types, each of which would need its own generator in definition 111.58 and its own case in lemma 111.74. So theorem 111.76 does not apply to it, and neither does theorem 49.17, whose signature is TCoq. Streicher’s modified-realizability separation and Hofmann’s account establish closely related formulations [Str93] [Hof95], but an exact signature translation to the book’s strict Russell hierarchy remains open.

A normalization theorem at a neighbouring signature

A cumulative Russell hierarchy also admits a normalization-model argument. The signature must remain explicit because its universe equations participate in the construction.

Convention 111.90 — The signature T_ Coq

Write TCoq for the signature of [Coq19]: the structural operations of a category with families [Coq19], dependent products with η [Coq19], a cumulative universe hierarchy Un satisfying the Russell identification Typen(Γ)=Elem(Γ,Un) [Coq19], and booleans N2 with the curried dependent recursor brec(C,c0,c1) in Elem(Γ,ΠN2C) [Coq19].

TCoq is not any calculus of this book, and four differences are load-bearing rather than cosmetic. Its universes are cumulative, whereas the hierarchy of definition 29.1 is strict and reaches higher levels only through the explicit lifts of definition 29.10; its Boolean recursor is ternary and returns a function, whereas ind2(x.C;ct,cf,b) is quaternary and consumes its scrutinee; the displayed Russell identification makes a type be an element of Un, whereas this book keeps ΓA type and Γa:Ui separate judgments related by U-El; and TCoq has no Σ, no 1, no N, no identity type and no indexed family. Its §7 records that the argument is expected to extend to dependent sums with surjective pairing and to W [Coq19]; that is an author’s remark about a future construction, not a theorem, and nothing here treats it as one.

Remark 111.91 — Why the universe cannot be deleted

It is tempting to read the Π and N2 clauses of the source as a self-contained sublist and to obtain a universe-free normalization theorem by striking the universe clauses. The construction does not have that shape.

In the reducibility model the type sort of the constructed model is its element sort at the universe: Elem((Γ,Γ),Un)=Typen(Γ,Γ) [Coq19]. In the normalization model a type at level n is a pair consisting of a type A together with a component in Un(A), and an element of Un(T) is a quadruple one of whose components is a normal form of T at Un [Coq19]. So Un is not one clause beside the others: it is the fibre in which every type datum lives, and the level n indexing it is the stratification on which the whole assignment recurses.

Deleting the universe operations therefore removes two different things at once—the carrier of every type datum, and the measure that makes the definition well founded. Replacing the universe-code component by a normal-type judgment does not repair this: it changes what the fibre is, so the closure and stability verifications must be redone for the new fibre, and the recursion must be re-founded on a new measure. That is a different construction with its own fundamental lemma. The construction of section 49.5section 111.9 is such a different construction, carried out from scratch for convention 111.16; it is not the neighbouring construction with its universe clause deleted.

Theorem 49.17 — Normalization

Let ICoq be the initial model of TCoq. For every context Γ of ICoq, type A over Γ, and elements a,b:A, it is decidable whether a=b. The decision procedure normalizes a and b to typed normal forms and compares those forms syntactically.

The conclusion is confined to TCoq. It proves nothing about TΠ2, nothing about the checker fragment Tel of definition 48.16, and nothing about Timpl; in particular it supplies no normalization structure in the sense of definition 49.16 for any of the three, and the Π/2 part of TCoq may not be split off to obtain one (remark 111.91). Nothing in section 49.5section 111.10 cites it.

Proof of Theorem 49.17 — Normalization

Proof. We construct a normalization model over ICoq and then use initiality to obtain the normalization function. The construction has four stages.

Stage 1: typed normal syntax. Let C be the category whose objects are telescopes and whose morphisms are renamings represented by lists of variables. For a telescope Δ and a type T over Δ, write NormΔ(T)andNeutΔ(T) for the sets of typed normal and neutral expressions, and write evT for their evaluation into ICoq. Renaming acts on both sets by recursion on normal and neutral syntax. The variable, application, Boolean-recursion, lambda, and normal-product constructors commute with this action, so these sets and evaluation maps form presheaves on C. In particular, normal products are freely generated: pi(T0,F0)=pi(T1,F1)T0=T1  and  F0=F1. The second equality is equality of the renamed bodies in the extended telescope. This injectivity is the syntactic fact used by the final comparison procedure.

Stage 2: the universe fibre. For an element T:Un in the presheaf model, define Un(T) to consist of quadruples qT=(T,T0,αT,βT) with the following data, natural in renamings: T(u)a set of realizers for every u:T,T0Norm(Un)with evUn(T0)=T,αT(u,ν)Norm(T)with evT(αT(u,ν))=u,βT(k)T(evT(k))for every kNeut(T). Thus αT reifies a realized element and βT reflects a neutral element. The normal universe code is part of the datum rather than a consequence of it; this is the reason for remark 111.91.

Form the displayed normalization model whose contexts are pairs (Γ,Γ), where Γ is a renaming-stable family over the environments of Γ. A type is a pair (A,A) with A(ρ,ρ)Un(Aρ), and an element is a pair (a,a) with a(ρ,ρ)(A(ρ,ρ))(aρ). Context extension and substitution use dependent sum and reindexing of these families. The projection that forgets all primed components therefore preserves the category-with-families operations.

Stage 3: closure under the signature. The universe Un is realized by Un=(Un,Un,αUn,βUn). Here αUn(T,qT) returns the component T0 of equation 111.14 below, and reflection of a neutral K:Un produces βUn(K)=(K,K,αK,βK), where K(u) is the set of neutral normal witnesses over u, αK includes such a witness into normal syntax, and βK regards a neutral as such a witness. In the notation of equation 111.14, the relevant component is αUn(T,(T,T0,αT,βT))=T0. These definitions satisfy equation 111.10 by the evaluation rule for a neutral universe code.

For booleans, let N2(t) contain a normal Boolean over t: it is either 0, 1, or a neutral Boolean. Reification is the inclusion into normal syntax, and reflection sends a neutral to its neutral alternative. To check the recursor, let qC(t,ν) be the normalization datum for its motive and let ξ0,ξ1 realize its two branches c0,c1. The result realizer is ξ0 when ν=0 and ξ1 when ν=1. When ν is a neutral k, put g(x):=(qC(ev(x),βN2(x)))0,krec:=brec(lamN2(xg(x)),αC(0,0)(c0,ξ0),αC(1,1)(c1,ξ1))(k). Reflect krec with the β-component of qC(t,k). Evaluation of the three clauses gives the two Boolean computations and the stuck recursor, respectively.

It remains to give the product clause. Suppose qA=(A,A0,αA,βA)Un(A) and, for every a:A and νA(a), qB(a,ν)=(B(a,ν),B0(a,ν),αB(a,ν),βB(a,ν))Un(B(a)). For w:Π(a:A).B(a) and a variable x, abbreviate ax:=ev(x) and νx:=βA(x). Set C(w):=a:AνA(a)B(a,ν)(app(w,a)),βC(k)(a,ν):=βB(a,ν)(app(k,αA(a,ν))),hw,ξ(x):=αB(ax,νx)(app(w,ax),ξ(ax,νx)),αC(w,ξ):=lamA0(xhw,ξ(x)),C0:=pi(A0,xB0(ax,νx)). In the last three lines x is the newest variable of the extended telescope, and every operation is renamed along that extension. Evaluation of the last line gives Π(a:A).B(a). Evaluation of βC gives the application of k because reflection preserves evaluation. Evaluation of αC gives w because the body evaluates pointwise to app(w,a) and product η identifies the resulting lambda with w. Hence (C,C0,αC,βC) belongs to Un(Π(a:A).B(a)). Equation 111.12, Equation 111.13, Equation 111.15, together with the pointwise structural clauses, equip the displayed model with every operation of TCoq and preserve all of its equations.

Stage 4: normalization and decision. Initiality gives a unique morphism s:ICoqICoq into the displayed model. Its composite with the forgetful projection is the identity morphism by initiality. Consequently, for every a:A, the second component a of s(a) has the type required in equation 111.11. Define nfA(a):=αA(a,a). By equation 111.10, evA(nfA(a))=a. If a=b, functoriality of s and of reification gives nfA(a)=nfA(b). Conversely, equality of the normal forms implies a=evA(nfA(a))=evA(nfA(b))=b. Typed normal syntax has decidable equality by structural recursion; the product case uses equation 111.8. Comparing nfA(a) and nfA(b) therefore decides whether a=b, as required. ◻

Remark 111.93 — What Abel's construction supplies, and at which signature

The untyped value domain of definition 49.36, the type-directed reflection and reification of definition 49.37, and the division of labour between a partial equivalence relation for completeness and a Kripke relation for soundness are Abel’s: the untyped domain is [Abe13], type-directed reflection and reification are [Abe13], the partial equivalence relations are [Abe13], and the Kripke relation to syntax is [Abe13]. The theorems there are proved for the language PTT of [Abe13]: untyped de Bruijn expressions with explicit substitutions over six constants—natural numbers, zero, successor, primitive recursion, the dependent function type, and the universes Setk—presented as a type-assignment system with a subsumption rule and cumulative universes SetkSetl for kl. PTT therefore has Π, N and universes and nothing else: no Σ, no 1, no 2, no identity type, no indexed family, no strict lifts and no binder metadata; and its subsumption rule is a rule that convention 111.16 does not have. What is borrowed above is the architecture, clause by clause; what is proved above is proved here. The same source’s [Abe13] records injectivity of the dependent function type for PTT, which is the analogue of the Π clause of theorem 111.81 at that smaller signature.

Remark 111.94 — The gluing reading

Definition 111.65 pairs a term with a value and requires them to agree after readback; definition 111.71 does the same for substitutions and environments. Angiuli and Gratzer present exactly this pairing as a gluing construction and package its conclusion as a normalization structure [AG26], which is the form used in definition 49.16. Their development is for extensional type theory and supplies no theorem used above; the normalization-structure packaging is only a definition.

Remark 111.95 — Boundary of the intrinsic NbE source

Altenkirch and Kaposi prove normalization, completeness, stability, and decidability of definitional equality by an internal, proof-relevant logical predicate [AK17]. Their object theory is the intrinsically typed quotient inductive–inductive syntax of [AK17]: explicit substitutions, dependent functions with η, one uninterpreted type U, and a family sending a term of that type to a type, El:TmΓUTyΓ. It has no Σ, 1, 2, N, identity type, vector family, strict lift, or binder metadata. The construction is internal to a metatheory supporting the quotient inductive–inductive presentation and extensional principles. It does not normalize types: normal terms remain indexed by types that need not be normal [AK17]. Thus it does not supply the normal-type component of convention 111.28. Its separate injectivity development [AK17] is the analogue of the Π-head argument in theorem 111.81, but only for its own signature. Consequently it supplies architectural evidence for definition 111.71, lemma 111.74. The proofs above are independent of its result; transferring that result to Timpl would still require exactly the missing former and metatheory translations just listed.

Bibliographic notes

Computability predicates originate with Tait’s normalization proof for Gödel’s System T; Girard’s candidates extend the method to impredicative polymorphism [GLT89]. Martin-Löf’s semantic normalization and decidability arguments [ML98, ML75] anticipate normalization by evaluation. Section 49.4 uses the Kripke presentation descending from Catarina Coquand’s formalization; Abel supplies the architecture for section 49.5section 111.9 at the smaller signature recorded in remark 111.93 [Abe13]. Altenkirch and Kaposi’s intrinsic presheaf construction supplies the source-bounded comparison in remark 111.95, including its explicit substitution signature and its limits relative to Timpl [AK17]. The proof-relevant algebraic construction in section 49.2, convention 111.90 follows Coquand [Coq19]; Angiuli and Gratzer package the corresponding Artin gluing as the normalization structure of definition 49.16 [AG26]. Streicher gives an early semantic analysis of intensionality [Str93], while Hofmann proves the extensional-equality boundary used in remark 49.21 [Hof95]. Synthetic Tait computability and its cubical and modal applications are developed in [Ste21, SA21, Gra23]; an operational cubical canonicity proof is [Ang19]. The rule-induction discipline is that of [Har16].

Suggested first pass.

Begin with exercise 111.16, then complete exercise 111.17.

Exercise 111.16

★★☆ In the respective contexts, normalize f:22f:22,x:2ind2(y.2;tt,ff,x):2, and p:(22)2p:(22)2. In the middle term the motive is the constant family y.2, the true branch is tt, the false branch is ff, and the principal argument is the neutral variable x; hence no computation rule fires. For each result, trace reflection and reification and identify the type index that prevents an untyped readback clause.

Exercise 111.17

★★★ Practical project.nbe-pi-bool Before implementing the evaluator, carry out on paper the following exact case table and record every evaluation, reflection, and reification call: Π—a lambda and application of a neutral function; Σ—a pair and both projections of a neutral pair; 1 and η-readback (there is no Unit eliminator in the signature); 2—both constructors and elimination of a neutral Boolean; N—zero, successor, and elimination of a neutral natural; identity—reflexivity and J on a neutral proof; vectors—nil, cons, and vind on a neutral vector; universes and strict lift—quotation of a universe code, a neutral code, and a lifted code (these are quotation cases, not term eliminators). Also write one ill-typed readback request and the invariant that rejects it.

Implement in Agda or Kappa a fuel-bounded executable slice of the normalizer of definition 111.45, definition 49.37 and a partial normal-form shape rechecker, covering every entry of the preceding case table; for Π preserve its two binder bits, for identity include J, for vectors include vind, and for strict universes include Lift. Each test supplies the semantic readback type as trusted input: the slice neither infers that type nor checks universe formation. Its invariant is only that reification is called at the supplied semantic type, that every stored annotation in the output is requoted rather than copied, and that the separate rechecker accepts the outer grammar of the resulting normal form. It is not the independent bidirectional rechecker of chapter 48. The program must produce: the η-long normal form of a variable at each negative former; the stuck normal form of each eliminator on a neutral principal argument; a normal Π-type whose two bits are preserved; the accepted type equation and the rejected code equation of example 111.84; the J and vind computations on refl and on vcons; and one accepted and one rejected conversion. Mutation test: replace one semantic clause by another that still type-checks—for instance, let reification at a Σ value return its first projection twice—and exhibit the named oracle that then fails. State explicitly that the executable slice is finite and that running it proves none of theorem 111.76, theorem 49.18, corollary 49.20.

Search the book

Type to search the local edition.