Chapter 110Core route

Trusted Kernels and Bidirectional Checking

Consider the input $((λ x . x) : N \to N) 0 : N .$ It is not a derivation. It is a finite string containing two claims: that the abstraction has function type, and that the application has type $N$ . A trusted kernel is the final checker that either constructs derivations of those claims or rejects the string. To accept it, the kernel checks the abstraction against $N \to N$ , synthesizes the same type for the annotated term, checks the argument, and finally compares the computed result type with $N$ .

The calculation exposes two algorithmic obligations. The checker must decide judgmental equality, and it must recover the arguments of a type constructor when an elimination rule demands them. The rest of the chapter makes those two obligations explicit in the kernel interface.

Proof assistants, judgmentally

Here a proof assistant is a partial function from unchecked syntax to derivations.

Remark 48.1 — Proof assistants are type-checkers ¶

Stripped of definitions, implicit arguments, tactics, and libraries, a proof assistant in the style of Agda, Rocq, or Lean is a type-checker. Its kernel checks context formation, declarations, types, terms, and equalities; the closed query $\cdot ⊢ a : A$ is only the simplest case. Surface features produce such kernel queries, but do not change their mathematical content. We study the trusted checking problem, not tactics or unification.

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

Production kernels optimize conversion and may use different universe or lift mechanisms. Whatever the representation, every accepted surface term must elaborate to a kernel term that a small trusted checker can recheck. The core used here is therefore a mathematical design point, not a literal description of Agda, Lean, or Rocq.

The five judgment forms of definition 26.13 classify well-formed objects, whereas a type-checker receives arbitrary syntax. Its input is therefore presyntax, syntax carrying no well-formedness guarantee, and its task is to produce a derivation—the process called elaboration.

Definition 48.2 — Presyntax ¶

A preexpression is a binding tree with no well-formedness requirement. We write $τ$ when it is offered as a type and $e$ when it is offered as a term. In the annotated language the relevant constructors are $\begin{array}{r} Pi (τ_{0}; x . τ_{1}), lam (τ_{0}; x . τ_{1}; x . e), app (τ_{0}; x . τ_{1}; e_{0}; e_{1}) . \end{array}$ In $Pi (τ_{0}; x . τ_{1})$ , $x$ binds in $τ_{1}$ ; in $lam (τ_{0}; x . τ_{1}; x . e)$ it also binds in $e$ . Base types and their constructors are preexpressions without annotations. Erasure retains the domain field of an abstraction as the kernel annotation of convention 27.1, and deletes the stored codomain and elimination annotations.

Referenced from 3 locations

Trusted Kernels and Bidirectional Checking

Definition 48.3 — Elaboration judgments ¶

The judgment $Γ ⊢ τ \Leftarrow type ⇝ A$ returns a well-formed type $A$ . The judgment $Γ ⊢ e : A ⇝ a$ checks $e$ at $A$ and returns a kernel term $a : A$ . Both presuppose $Γ ctx$ . The head constructor selects at most one rule, so the judgments define partial functions $elabTy$ and $elabTm$ .

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

Here are the rules needed for the opening calculation. The base rules are $Γ ⊢ N \Leftarrow type ⇝ N$ and $Γ ⊢ 0 : N ⇝ 0$ .

Γ ⊢ τ_{0} \Leftarrow type ⇝ A

Γ, x : A ⊢ τ_{1} \Leftarrow type ⇝ B

Γ ⊢ Pi (τ_{0}; x . τ_{1}) \Leftarrow type ⇝ \prod_{x : A} B

Pre-Pi

(x : A) \in Γ

Γ ⊢ C \equiv A type

Γ ⊢ x : C ⇝ x

Pre-Var

Γ ⊢ τ_{0} type ⇝ A

Γ, x : A ⊢ τ_{1} type ⇝ B

Γ, x : A ⊢ e : B ⇝ b

Γ ⊢ C \equiv \prod_{x : A} B type

Γ ⊢ lam (τ_{0}; x . τ_{1}; x . e) : C ⇝ λ (x : A) . b

Pre-Lam

Γ ⊢ τ_{0} type ⇝ A

Γ, x : A ⊢ τ_{1} type ⇝ B

Γ ⊢ e_{0} : \prod_{x : A} B ⇝ f

Γ ⊢ e_{1} : A ⇝ a

Γ ⊢ C \equiv B [a / x] type

Γ ⊢ app (τ_{0}; x . τ_{1}; e_{0}; e_{1}) : C ⇝ f a

Pre-App

Example 110.4 — The first complete elaboration ¶

Put $I : = lam (N; x . N; x . x)$ . The premises $\begin{aligned} \cdot ⊢ N \Leftarrow type ⇝ N, & x : N ⊢ N \Leftarrow type ⇝ N, x : N ⊢ x : N ⇝ x, \\ \cdot ⊢ N \to N \equiv N \to N type \end{aligned}$ give $\cdot ⊢ I : N \to N ⇝ λ (x : N) . x$ by Pre-Lam. Together with $\cdot ⊢ 0 : N ⇝ 0$ and $\cdot ⊢ N \equiv N type$ , rule Pre-App gives $\cdot ⊢ app (N; x . N; I; 0) : N ⇝ (λ (x : N) . x) 0 .$ The variable and zero leaves produce the kernel subterms; the two reflexive equality checks discharge the claimed function and result types.

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

Remark 48.5 — Where type-checking happens ¶

In Pre-Lam the recursive calls merely translate presyntax; the checking is the final premise $Γ ⊢ C \equiv \prod_{x : A} B type$ —a full judgment of the object theory, not a syntactic comparison. With universes and large elimination (definition 29.1) the expected type $C$ may be an arbitrary computation, e.g. $C : = {rec}_{2} (U_{0}; \prod_{x : N} N; 2; b)$ for non-normal $b : 2$ , and deciding $C \equiv \prod_{x : A} B$ requires evaluating $b$ . An elaborator therefore contains, as a subroutine, a decision procedure for judgmental equality; whether one exists is a property of the theory, not of the implementation (section 48.2).

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

The untrusted elaborator may construct annotations by any method. The trusted rechecker traverses those annotations independently and accepts only when it reconstructs the claimed type and kernel term. This two-phase boundary goes back to de Bruijn’s Automath; the LCF architecture instead makes theorems values of an abstract type.

The projection example marks the same boundary in the fused calculus: projection from an unannotated pair is not synthesizable, and an expected type for the projection does not repair the missing synthesis premise. The elaboration rule must put an annotation on the pair itself or construct another synthesis-directed form.

Exercise 48.1 ¶

★★☆ Extend definition 48.2 by the four constructors $Sg$ , $pair$ , $fst$ , and $snd$ , with the same stored domain and codomain annotations as their $Π$ analogues. Then write Pre-Sg, Pre-Pair, Pre-Fst, and Pre-Snd. Include a result-type equality premise in each term rule whose expected type is $C$ ; Pre-Sg, like Pre-Pi, is a type-elaboration rule and has no such premise. Verify that each constructor selects exactly one rule.

Referenced from 3 locations

Lemma 48.6 — Effective enumeration of derivations ¶

For a fixed recursive signature, derivations of each of the five judgments are recursively enumerable. Consequently derivability, including $Γ ⊢ A \equiv B type$ and $Γ ⊢ a \equiv b : A$ , is semidecidable.

Referenced from 3 locations

Trusted Kernels and Bidirectional Checking

Proof of Lemma 48.6 — Effective enumeration of derivations

Proof. Encode variables, binding trees, finite contexts, rule names, and finite trees by natural numbers. Enumerate finite labeled trees. For each tree, check bottom-up that every node is an instance of its displayed rule: finite lists and freshness are elementary, while raw substitution and alpha-equivalence are decidable by convention 2.3, definition 26.6, definition 26.10. Output precisely the accepted trees. To semidecide a fixed judgment, run the enumeration until a tree with that root appears. If the judgment is derivable this happens after finitely many steps; otherwise the search continues. ◻

The metatheoretic demands

Equality checking and constructor inversion are algorithmic requirements; consistency and canonicity describe the judgments they accept. Their computability claims take finite derivation trees as inputs.

Remark 48.7 — Encoding ¶

Computability-theoretic statements use ordinary deterministic Turing machines and a fixed effective Gödel coding of binding trees, contexts, rule names, and finite derivation trees by $N$ . A relation is decidable when a total machine computes its characteristic function; it is semidecidable when a machine halts and accepts exactly its positive instances. A type $A$ with $Γ ⊢ A type$ is presented by a derivation tree of that judgment, and likewise for terms. Thus “equality of types is decidable” means that, given derivations of $Γ ⊢ A type$ and $Γ ⊢ B type$ , a total machine decides whether $Γ ⊢ A \equiv B type$ . These are external metatheoretic claims, not object-language judgments.

Referenced from 4 locations

Definition 48.8 — Normalization structure ¶

An effective conversion invariant consists of computable functions $nfTy$ and $nfTm$ on derivations. They return natural numbers and satisfy $\begin{aligned} nfTy (Γ, A) = nfTy (Γ, B) & ⟺ Γ ⊢ A \equiv B type, \\ nfTm (Γ, a, A) = nfTm (Γ, b, A) & ⟺ Γ ⊢ a \equiv b : A . \end{aligned}$ The inputs include the formation or typing derivations. Such an invariant computes one canonical code for each judgmental-equality class. A normalizer supplies one by encoding its normal form. The converse need not compute a normal term or a reduction sequence, so this definition is strictly weaker than a normalization theorem.

Referenced from 6 locations

Proposition 48.9 ¶

A type theory with a recursive signature and effectively checkable rule instances admits an effective conversion invariant if and only if there is a decision procedure for its judgmental equality of types and of terms.

Referenced from 7 locations

Proof of Proposition 48.9

Proof. ( $\Rightarrow$ ) Compute and compare the two output numerals.

( $\Leftarrow$ ) Enumerate all derivations as $D_{0}, D_{1}, \dots$ using lemma 48.6. Let $nfTy (Γ, A)$ be the least index $i$ such that $D_{i} derives Γ ⊢ A_{i} type and the decider accepts Γ ⊢ A \equiv A_{i} type .$ The input derivation of $A$ itself eventually appears, so the search terminates. Equal types accept the same indices. Their least indices are therefore equal; the common $A_{i}$ proves the converse.

For a term input $Γ ⊢ a : A$ , let $nfTm (Γ, a, A)$ be the least $i$ for which $D_{i}$ derives $Γ ⊢ b_{i} : B_{i}$ , the type decider accepts $A \equiv B_{i}$ , and, after converting $b_{i}$ to $A$ , the term decider accepts $a \equiv b_{i} : A$ . The same termination and least-index argument applies. The hypothesis is an actual computable decider; a bare classical instance of excluded middle contains no such algorithm. ◻

Definition 48.10 — Injective and invertible Π -types ¶

A type theory has injective $Π$ -types if $Γ ⊢ \prod_{x : A} B \equiv \prod_{x : A^{'}} B^{'} type$ implies first $Γ ⊢ A \equiv A^{'} type$ and then $Γ, x : A ⊢ B \equiv B^{'} ↓_{A} type .$ Here $B^{'} ↓_{A}$ is $B^{'}$ regarded in $Γ, x : A$ by context conversion along $A \equiv A^{'}$ . An inversion operation satisfies $unPi (Γ, C) = (A, x . B) ⟹ C \equiv \prod_{x : A} B .$ If also $C \equiv \prod_{x : A^{'}} B^{'}$ , injectivity gives $A \equiv A^{'}$ and, after context conversion, $B \equiv B^{'}$ . Thus the returned head is computed, not chosen. The total operation reports failure exactly when $C$ has no $Π$ -presentation. Replacing the $Π$ head and its two component types by the $Σ$ , identity, universe, or nullary head and its displayed arguments defines the remaining inversion operations.

Referenced from 7 locations

Definition 48.11 — Consistency ¶

A type theory is consistent if there is no closed term $\cdot ⊢ a : 0$ .

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

Consistency excludes a proof of the empty type, but it does not say what a closed datum computes to. A consistent theory could still contain a closed Boolean that is judgmentally equal to neither constructor. The stronger computational condition is therefore separate.

Definition 48.12 — Canonicity ¶

A type theory enjoys canonicity if for every closed term $\cdot ⊢ b : 2$ exactly one of $\cdot ⊢ b \equiv tt : 2$ and $\cdot ⊢ b \equiv ff : 2$ holds.

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

Remark 48.13 ¶

Natural-number canonicity says more than head canonicity: every closed $n : N$ is judgmentally equal to one and only one numeral ${suc}^{k} (0)$ . Boolean canonicity does not by itself establish this natural-number statement for the full base theory. In the Boolean definition, “exactly one” is “at least one” together with the separation $tt ≢ ff$ . Consistency implies that separation by the Boolean large-elimination family of theorem 29.14.

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

Remark 48.14 — The demand list ¶

The four demands are:

an effective conversion invariant, for equality checking;
computably invertible type constructors, for syntax-directed elaboration;
consistency, for reading types as propositions; and
canonicity, for reading closed data as programs.

These are properties of a specified signature. No item follows merely from the words “dependent type theory.”

Referenced from 3 locations

Exercise 48.2 ¶

★★★ Spell out the computability details suppressed in the proof of proposition 48.9: define the enumeration of derivations, verify that the search is a partial recursive function, and verify totality on well-typed inputs, and prove that the term index is independent of a converted choice of classifier.

Referenced from 3 locations

Bidirectional elaboration

The annotated calculation works, but it repeats $N$ four times. We can remove most annotations without asking the impossible question “infer the type of every term.” Instead, information is allowed to flow in both directions.

Remark 48.15 — The bidirectional discipline ¶

For some preterms the term fixes the type: the codomain of the synthesized type of $f$ fixes the type of $f a$ after checking $a$ against its domain. For others it must be supplied from outside: to elaborate $λ x . e$ one must be told the domain. The discipline checks types at introduction forms and synthesizes them at elimination forms, changing direction at a single explicit annotation form.

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

Convention 110.16 — The Timpl kernel signature ¶

The implementation signature $T_{impl}$ , pronounced “Timpl”, is the predicative kernel used by the elaboration and definition-processing pipeline. Its type formers are $Π$ , $Σ$ , $1$ , $2$ , $N$ , intensional identity, the strict Russell universes of definition 29.1, and the vector family and eliminator of definition 78.1. Level expressions are built from external parameters by zero, successor, and maximum. The only recursive programs in the signature are the displayed structural eliminators.

Every core $Π$ -binder, abstraction, and application stores an explicitness bit $ϵ \in {\exp, imp}$ and a relevance bit $ϱ \in {runtime, erased}$ : $\prod_{x : A}^{ϵ, ϱ} B, λ^{ϵ, ϱ} (x : A) . b, f^{ϵ, ϱ} a .$ Formation, introduction, elimination, computation, and uniqueness erase these two bits to the corresponding rules of definition 27.2; a rule is admitted only when all occurrences belonging to one binder carry the same pair $(ϵ, ϱ)$ . Relevance is therefore checked kernel syntax, not a typing or conversion premise: erased arguments remain exact arguments of core terms. The Boolean and vector rules are exactly those of definition 28.7, definition 78.1; the kernel merely copies their explicit level and element/index arguments.

The auxiliary proof fragment $T_{el} \subset T_{impl}$ , used to isolate a smaller named signature, deletes $2$ , vectors, and the two metadata fields. The inclusion runs one way only: every $T_{el}$ derivation is a Timpl derivation, because its rules are a sublist of Timpl’s. Nothing here asserts the converse. In particular a judgment written in $T_{el}$ syntax may in principle have a Timpl derivation that passes through $2$ large elimination. Conservativity of Timpl over $T_{el}$ would require both full-signature normalization and a subformula argument showing that the normal form of a $T_{el}$ judgment mentions no $2$ , no vector, and no metadata bit. The checker, rechecker, and all metatheorems in this chapter range over full Timpl; no constructor is hidden behind the name of the auxiliary fragment.

Referenced from 14 locations

Proposition 110.17 — Exact rule delta from the proof fragment to Timpl ¶

The full Timpl rule set is obtained from $T_{el}$ by exactly three changes: restore $2$ and its dependent eliminator from definition 28.7; restore the level-polymorphic vector family, constructors, and eliminator from definition 78.1; and replace each $Π$ -formation, abstraction, application, beta, and eta rule by its metadata-preserving instance from convention 110.16. No other formation, conversion, or computation rule changes.

The delta newly admits, for example, the fully annotated derivation $A : U_{i}, n : N, a : A, x s : Vec (A, n) ⊢ vcons (n, a, x s) : Vec (A, suc (n)) .$ Here $vcons$ is the surface vector constructor fixed in definition 78.1. The annotated core constructor written later as ${Cons}_{i} [τ; \vec{e}]$ records the universe, element type, and index arguments that elaboration reconstructs for this same constructor. The rules below print these added cases rather than appealing to this delta as an implementation. Their termination conclusion remains conditional on the conversion and inversion oracles hypothesized in definition 48.16 at the full Timpl signature. Nothing in this chapter constructs those oracles, so every generic checker theorem below retains that interface as an explicit hypothesis.

Since that hypothesis is what every checker theorem below rests on, name its content exactly. Totality of $- ⊢ - \Leftrightarrow - type$ , $- ⊢ - \Leftrightarrow - : -$ , $unPiMeta$ , $unSg$ , $unId$ and $unUniv$ at Timpl means one simultaneous construction covering six formers beyond $Π$ and $2$ : the strict Russell universes, $Σ$ , $1$ , $N$ , intensional identity with $J$ , and the vector family. Six separate arguments would not do, because the evidence attached to each former recurs through the others. A total Timpl conversion interface means exactly this simultaneous six-former construction; no smaller collection of unrelated decision procedures satisfies the hypothesis.

Referenced from 5 locations

Proof of Proposition 110.17 — Exact rule delta from the proof fragment to Timpl

Proof. Inspection of the three listed rule families proves the syntactic-delta claim. Applying Vec-intro $_{s}$ to the displayed premises gives the new derivation. The last claim follows from the six operations just listed: each is an explicit premise of a checker clause and none is defined by the finite structural traversal. ◻

Definition 48.16 — Bidirectional elaboration ¶

The algorithm ranges over the full Timpl signature of convention 110.16: $Π$ , $Σ$ , $1$ , $2$ , $N$ , intensional identity, the Russell hierarchy with strict lifts, and $Vec$ . Products, abstractions, and applications retain their explicitness and relevance bits. Vector type syntax writes its level as $Vec [i] (τ, e)$ ; the level and all element, index, and motive arguments remain present in the returned core term.

Its surface expressions are the unannotated raw expressions, with two exceptions. There is an annotation $(e : τ)$ , and the surface reflexivity constructor is $refl (e)$ ; the latter elaborates to the official raw constructor ${refl}_{a}$ . Eliminators retain the motives and binders displayed in definition 28.21, definition 30.1.

The bidirectional elaboration judgments are the three modes that respectively check a type, check a term against an expected type, and synthesize a type together with a kernel term.

Assume total deterministic computable operations $\begin{matrix} Γ ⊢ A \Leftrightarrow B type, Γ ⊢ a \Leftrightarrow b : A, \\ unPiMeta (Γ, C), unSg (Γ, C), unId (Γ, C), unUniv (Γ, C) . \end{matrix}$ Their modes and presuppositions are: $\begin{array}{ccc} query & inputs & output \\ Γ ⊢ τ \Leftarrow type & Γ, τ & A type in Γ \\ Γ ⊢ e \Leftarrow A & Γ, e, A & A -typed kernel term a \\ Γ ⊢ e \Rightarrow & Γ, e & A and a : A \\ Γ ⊢ A \Leftrightarrow B type & Γ, A, B & yes / no \\ Γ ⊢ a \Leftrightarrow b : A & Γ, a, b, A & yes / no \end{array}$ The equality queries presuppose well-formed input types and well-typed terms; the symbol $\Leftrightarrow$ denotes algorithmic conversion, not logical equivalence. The first two oracles are sound and complete for judgmental equality. Each constructor inversion has the universal-coherence property of definition 48.10: it either returns the constructor arguments together with a judgmental equality to $C$ , coherently with every other presentation of $C$ , or reports correctly that none exists. In particular, $unPiMeta (Γ, C) = (ϵ, ϱ, A, x . B)$ verifies the stored bits and returns a display $C \equiv \prod_{x : A}^{ϵ, ϱ} B$ ; and $unUniv (Γ, C) = i$ means $Γ ⊢ C \equiv U_{i} type$ ; unlike an unbounded search for $i$ , this is an executable oracle.

Strict lift is deliberately a code-level former in this surface language: ${Lift}_{i} (e)$ checks against a universe, but does not synthesize as a type head. To use it where type synthesis is required, annotate it at the intended universe and let the synthesized universe element enter type mode.

The three judgments are $Γ ⊢ τ \Leftarrow type ⇝ A, Γ ⊢ e \Leftarrow A ⇝ a, Γ ⊢ e \Rightarrow A ⇝ a .$ Type mode elaborates a surface type, checking mode consumes an expected type, and synthesis mode returns one. The annotation $(e : τ)$ switches a checked term into synthesis. Formation premises recoverable from the rule data are suppressed as in convention 26.14. The exact priority order is printed after the rule cards; a recognized head is never retried through the fallback clause.

Referenced from 17 locations

Remark 110.19 — Status for the named signatures ¶

The assumptions and results do not have the same scope:

Signature	Demands	Status
$T_{Π 2}$	neither D1 nor D2	the direct Tait proof supplies only closed-Boolean canonicity and separation
Coquand’s $T_{Coq}$	D1	a normalization-model construction at a cumulative universe-bearing signature that is none of the calculi in this book
$T_{impl}$	D1–D2	the six total operations are the explicit interface hypotheses of this chapter
ETT with universes	D1; $Π$ part of D2	refuted by theorem 48.40, corollary 48.48

The cumulative construction remains at $T_{Coq}$ and supplies none of the oracles here. The generic checker theorems therefore remain stated relative to their interface at this point; the whole-book signature ledger records any separate construction that instantiates it.

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

The type-checking rules are structural translations. A synthesized universe element provides the only bridge from a term mode to the type mode.

Γ ⊢ τ_{0} \Leftarrow type ⇝ A

Γ, x : A ⊢ τ_{1} \Leftarrow type ⇝ B

Γ ⊢ \prod_{x : τ_{0}}^{ϵ, ϱ} τ_{1} \Leftarrow type ⇝ \prod_{x : A}^{ϵ, ϱ} B

Ty-Pi

Γ ⊢ τ_{0} \Leftarrow type ⇝ A

Γ, x : A ⊢ τ_{1} \Leftarrow type ⇝ B

Γ ⊢ \sum_{x : τ_{0}} τ_{1} \Leftarrow type ⇝ \sum_{x : A} B

Ty-Sg

Γ ⊢ τ \Leftarrow type ⇝ A

Γ ⊢ e_{0} \Leftarrow A ⇝ a

Γ ⊢ e_{1} \Leftarrow A ⇝ b

Γ ⊢ {Id}_{τ} (e_{0}, e_{1}) \Leftarrow type ⇝ {Id}_{A} (a, b)

Ty-Id

Γ ⊢ 1 \Leftarrow type ⇝ 1

Ty-1

Γ ⊢ N \Leftarrow type ⇝ N

Ty-

Γ ⊢ 2 \Leftarrow type ⇝ 2

Ty-

Γ ⊢ τ \Leftarrow U_{i} ⇝ A

Γ ⊢ e \Leftarrow N ⇝ n

Γ ⊢ Vec [i] (τ, e) \Leftarrow type ⇝ Vec (A, n)

Ty-Vec

Γ ⊢ U_{i} \Leftarrow type ⇝ U_{i}

Ty-Univ

Γ ⊢ e \Rightarrow C ⇝ a

unUniv (Γ, C) = i

Γ ⊢ e \Leftarrow type ⇝ a

Ty-El

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

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

(x : A) \in Γ

Γ ⊢ x \Rightarrow A ⇝ x

Syn-Var

Γ ⊢ e_{0} \Rightarrow C ⇝ f

unPiMeta (Γ, C) = (ϵ, ϱ, A, x . B)

Γ ⊢ e_{1} \Leftarrow A ⇝ a

Γ ⊢ e_{0}^{ϵ, ϱ} e_{1} \Rightarrow B [a / x] ⇝ f^{ϵ, ϱ} a

Syn-App

Γ ⊢ e \Rightarrow C ⇝ p

unSg (Γ, C) = (A, x . B)

Γ ⊢ {pr}_{1} (e) \Rightarrow A ⇝ {pr}_{1} (p)

Syn-Fst

Γ ⊢ e \Rightarrow C ⇝ p

unSg (Γ, C) = (A, x . B)

Γ ⊢ {pr}_{2} (e) \Rightarrow B [{pr}_{1} (p) / x] ⇝ {pr}_{2} (p)

Syn-Snd

Γ ⊢ ⋆ \Rightarrow 1 ⇝ ⋆

Syn-★

Γ ⊢ 0 \Rightarrow N ⇝ 0

Syn-Zero

Γ ⊢ e \Leftarrow N ⇝ n

Γ ⊢ suc (e) \Rightarrow N ⇝ suc (n)

Syn-Suc

Γ ⊢ tt \Rightarrow 2 ⇝ tt

Syn-True

Γ ⊢ ff \Rightarrow 2 ⇝ ff

Syn-False

Γ ⊢ τ \Leftarrow type ⇝ A

Γ ⊢ e \Leftarrow A ⇝ a

Γ ⊢ (e : τ) \Rightarrow A ⇝ a

Syn-Ann

Γ ⊢ e \Rightarrow D ⇝ b

Γ ⊢ D \Leftrightarrow 2 type

Γ, k : 2 ⊢ τ \Leftarrow type ⇝ C

Γ ⊢ e_{t} \Leftarrow C [tt / k] ⇝ c_{t}

Γ ⊢ e_{f} \Leftarrow C [ff / k] ⇝ c_{f}

Γ ⊢ {ind}_{2} (k . τ; e_{t}, e_{f}; e) \Rightarrow C [b / k] ⇝ {ind}_{2} (k . C; c_{t}, c_{f}; b)

Syn-BoolInd

Γ ⊢ e \Rightarrow D ⇝ m

Γ ⊢ D \Leftrightarrow N type

Γ, k : N ⊢ τ \Leftarrow type ⇝ C

Γ ⊢ e_{z} \Leftarrow C [0 / k] ⇝ c_{z}

Γ, n : N, y : C [n / k] ⊢ e_{s} \Leftarrow C [suc (n) / k] ⇝ c_{s}

Γ ⊢ {ind}_{N} (k . τ; e_{z}; n . y . e_{s}; e) \Rightarrow C [m / k] ⇝ {ind}_{N} (k . C; c_{z}; n . y . c_{s}; m)

Syn-NatInd

Γ ⊢ q \Rightarrow D ⇝ q^{'}

unId (Γ, D) = (A, a, b)

Γ, x : A, y : A, p : {Id}_{A} (x, y) ⊢ τ \Leftarrow type ⇝ C

Γ, z : A ⊢ e \Leftarrow C [z / x, z / y, {refl}_{z} / p] ⇝ c

Γ ⊢ J (x . y . p . τ; z . e; q) \Rightarrow C [a / x, b / y, q^{'} / p] ⇝ J_{A; a; b} (x . y . p . C; z . c; q^{'})

Syn-J

The vector constructors and eliminator expose every parameter needed by the kernel rule. The bracketed lists below are stored certificate fields, not inferred surface arguments. Write ${Nil}_{i} [τ]$ for the annotated nil form, ${Cons}_{i} [τ; \vec{e}]$ for annotated cons, where $\vec{e} = (e_{n}, e_{a}, e_{x s})$ , and ${Ind}_{i, j}$ for annotated vector elimination. Its stored fields, in order, are $τ_{A}$ , $n . v . τ_{P}$ , $e_{0}$ , $n . a . x s . q . e_{s}$ , $e_{m}$ , and $e_{y s}$ . Put $P_{0} : = P [0 / n, {Nil}_{i} [A] / v]$ and $P_{s} : = P [suc (n) / n, {Cons}_{i} [A; (n, a, x s)] / v]$ . For the eliminator rule also abbreviate $\begin{aligned} Δ_{s} : = & Γ, n : N, a : A, \\ x s : Vec (A, n), q : P [n / n, x s / v] . \end{aligned}$

Γ ⊢ τ \Leftarrow U_{i} ⇝ A

Γ ⊢ {Nil}_{i} [τ] \Rightarrow Vec (A, 0) ⇝ {Nil}_{i} [A]

Syn-VNil

Γ ⊢ τ \Leftarrow U_{i} ⇝ A

Γ ⊢ e_{n} \Leftarrow N ⇝ n

Γ ⊢ e_{a} \Leftarrow A ⇝ a

Γ ⊢ e_{x s} \Leftarrow Vec (A, n) ⇝ x s

Γ ⊢ {Cons}_{i} [τ; \vec{e}] \Rightarrow Vec (A, suc (n)) ⇝ {Cons}_{i} [A; (n, a, x s)]

Syn-VCons

For Syn-VecInd, abbreviate the complete surface and core nodes by $\begin{aligned} E_{V} & : = {Ind}_{i, j} [τ_{A}; n . v . τ_{P}; e_{0}; n . a . x s . q . e_{s}; e_{m}, e_{y s}], \\ a_{V} & : = {Ind}_{i, j} [A; n . v . P; p_{0}; n . a . x s . q . p_{s}; m, y s] . \end{aligned}$

Γ ⊢ τ_{A} \Leftarrow U_{i} ⇝ A

Γ ⊢ e_{m} \Leftarrow N ⇝ m

Γ ⊢ e_{y s} \Leftarrow Vec (A, m) ⇝ y s

Γ, n : N, v : Vec (A, n) ⊢ τ_{P} \Leftarrow U_{j} ⇝ P

Γ ⊢ e_{0} \Leftarrow P_{0} ⇝ p_{0}

Δ_{s} ⊢ e_{s} \Leftarrow P_{s} ⇝ p_{s}

Γ ⊢ E_{V} \Rightarrow P [m / n, y s / v] ⇝ a_{V}

Syn-VecInd

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

unPiMeta (Γ, C) = (ϵ, ϱ, A, x . B)

Γ, x : A ⊢ e \Leftarrow B ⇝ b

Γ ⊢ λ^{ϵ, ϱ} x . e \Leftarrow C ⇝ λ^{ϵ, ϱ} (x : A) . b

Chk-Lam

unSg (Γ, C) = (A, x . B)

Γ ⊢ e_{0} \Leftarrow A ⇝ a

Γ ⊢ e_{1} \Leftarrow B [a / x] ⇝ b

Γ ⊢ (e_{0}, e_{1}) \Leftarrow C ⇝ (a, b)

Chk-Pair

unId (Γ, C) = (A, a, b)

Γ ⊢ e \Leftarrow A ⇝ c

Γ ⊢ c \Leftrightarrow a : A

Γ ⊢ a \Leftrightarrow b : A

Γ ⊢ refl (e) \Leftarrow C ⇝ {refl}_{c}

Chk-Refl

Γ ⊢ e \Rightarrow C^{'} ⇝ a

Γ ⊢ C \Leftrightarrow C^{'} type

Γ ⊢ e \Leftarrow C ⇝ a

Chk-Conv

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

unUniv (Γ, C) = i

Γ ⊢ 1 \Leftarrow C ⇝ 1

Chk-Code-1

unUniv (Γ, C) = i

Γ ⊢ N \Leftarrow C ⇝ N

Chk-Code-

unUniv (Γ, C) = i

Γ ⊢ 2 \Leftarrow C ⇝ 2

Chk-Code-

unUniv (Γ, C) = i j < i

Γ ⊢ U_{j} \Leftarrow C ⇝ U_{j}

Chk-Code-Univ

unUniv (Γ, C) = i

Γ ⊢ τ_{0} \Leftarrow U_{i} ⇝ A

Γ, x : A ⊢ τ_{1} \Leftarrow U_{i} ⇝ B

Γ ⊢ \prod_{x : τ_{0}}^{ϵ, ϱ} τ_{1} \Leftarrow C ⇝ \prod_{x : A}^{ϵ, ϱ} B

Chk-Code-Pi

unUniv (Γ, C) = i

Γ ⊢ τ_{0} \Leftarrow U_{i} ⇝ A

Γ, x : A ⊢ τ_{1} \Leftarrow U_{i} ⇝ B

Γ ⊢ \sum_{x : τ_{0}} τ_{1} \Leftarrow C ⇝ \sum_{x : A} B

Chk-Code-Sg

unUniv (Γ, C) = i

Γ ⊢ τ \Leftarrow U_{i} ⇝ A

Γ ⊢ e_{0} \Leftarrow A ⇝ a

Γ ⊢ e_{1} \Leftarrow A ⇝ b

Γ ⊢ {Id}_{τ} (e_{0}, e_{1}) \Leftarrow C ⇝ {Id}_{A} (a, b)

Chk-Code-Id

unUniv (Γ, C) = i + 1

Γ ⊢ e \Leftarrow U_{i} ⇝ A

Γ ⊢ {Lift}_{i} (e) \Leftarrow C ⇝ {Lift}_{i} A

Chk-Code-Lift

unUniv (Γ, C) = i

Γ ⊢ τ \Leftarrow U_{i} ⇝ A

Γ ⊢ e \Leftarrow N ⇝ n

Γ ⊢ Vec [i] (τ, e) \Leftarrow C ⇝ Vec (A, n)

Chk-Code-Vec

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

The rule cards are executed in the following total priority order. In type mode inspect the head in the order $Π^{ϵ, ϱ}, Σ, Id, 1, 2, N, Vec [i], U_{i}; otherwise try Ty-El.$ In synthesis mode inspect the head in the order $\begin{aligned} x, {app}^{ϵ, ϱ}, fst, snd, ⋆, 0, suc, tt, ff, (- : -), \\ 2 -ind, N -ind, J, {Nil}_{i} [-], {Cons}_{i} [-; -], {Ind}_{i, j} [-] . \end{aligned}$ In checking mode first try, in order, the recognized heads $λ^{ϵ, ϱ}$ , pair, reflexivity, and the universe-code heads $1, N, 2, U, Π^{ϵ, ϱ}, Σ, Id, Lift, Vec$ ; only an unrecognized head reaches Chk-Conv. Within a selected clause, premises run top to bottom. A failed premise rejects the query; there is no backtracking to a later clause.

Proposition 48.17 — Determinism and termination ¶

Read with this priority, every full-Timpl elaboration query has at most one derivation and one output. Assuming the exact oracles of definition 48.16 total, every query terminates.

Referenced from 4 locations

Proof of Proposition 48.17 — Determinism and termination

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

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

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

Remark 110.21 — The de Bruijn criterion ¶

A proof assistant meets the de Bruijn criterion when it can export a proof object that a small, independent program checks against the stated formal rules. For Timpl the trust chain consists of the surface input, then the untrusted elaborator, then the certificate $(Γ, τ_{A}, e, A, a)$ , then the independent rechecker, and finally the judgment $Γ ⊢ a : A$ . Only the last implication is the mathematical guarantee. The rechecker’s implementation, its parser, and the sound implementations of the conversion and inversion oracles remain in the trusted base; tactics and the elaborator do not.

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

Definition 110.22 — Independent annotation recheck ¶

A term certificate is a quintuple $(Γ, τ_{A}, e, A, a)$ . Here $τ_{A}$ is the fully annotated surface certificate for the claimed core type $A$ , and $e$ uses the full Timpl surface syntax of definition 48.16, including every written level, motive, vector parameter, and metadata bit. The claimed $A$ and $a$ are core syntax. The rechecker ignores any supplied derivation and evaluates three mutually recursive partial functions $R_{ty} (Γ, τ), R_{syn} (Γ, e), R_{chk} (Γ, e, A) .$ Their equations are the rule cards above, evaluated top to bottom. The table is exhaustive; each entry means “make exactly the recursive calls and oracle calls printed in this rule, then return its printed output.”

Function	recognized head, in order	defining clause
$R_{ty}$	$Π^{ϵ, ϱ}$ ; $Σ$ ; $Id$ ; $1$ ; $2$ ; $N$ ; $Vec [i]$ ; $U_{i}$ ; other	Ty-Pi; Ty-Sg; Ty-Id; Ty- $1$ ; Ty- $2$ ; Ty- $N$ ; Ty-Vec; Ty-Univ; Ty-El
$R_{syn}$	variable; application; first; second; $⋆$ ; $0$ ; $suc$ ; $tt$ ; $ff$ ; annotation; $2$ -induction; $N$ -induction; $J$ ; ${Nil}_{i} [-]$ ; ${Cons}_{i} [-; -]$ ; ${Ind}_{i, j} [-]$	Syn-Var; Syn-App; Syn-Fst; Syn-Snd; Syn- $⋆$ ; Syn-Zero; Syn-Suc; Syn-True; Syn-False; Syn-Ann; Syn-BoolInd; Syn-NatInd; Syn- $J$ ; Syn-VNil; Syn-VCons; Syn-VecInd
$R_{chk}$	lambda; pair; reflexivity; code $1$ ; code $N$ ; code $2$ ; code $U$ ; code $Π^{ϵ, ϱ}$ ; code $Σ$ ; code $Id$ ; code $Lift$ ; code $Vec [i]$ ; other	Chk-Lam; Chk-Pair; Chk-Refl; Chk-Code- $1$ ; Chk-Code- $N$ ; Chk-Code- $2$ ; Chk-Code-Univ; Chk-Code-Pi; Chk-Code-Sg; Chk-Code-Id; Chk-Code-Lift; Chk-Code-Vec; Chk-Conv

There is no implicit default: a head absent from its row fails. A recognized head whose selected clause fails is not retried as “other.” Binder freshening is deterministic up to alpha-equivalence. In particular, Syn-VecInd checks the motive in $Γ, n : N, v : Vec (A, n)$ and its successor method in the full $n, a, x s, q$ context; Syn- $J$ checks its motive in the full $x, y, p$ context. These are equations of the rechecker, not prose placeholders.

To decide a certificate, first run $R_{ty} (Γ, τ_{A}) = A^{'}$ and require $Γ ⊢ A^{'} \Leftrightarrow A type$ . Then run $R_{chk} (Γ, e, A) = a^{'}$ . Accept exactly when $a^{'} =_{α} a$ . The final term comparison is syntactic because the claimed $a$ carries no typing derivation. The type comparison is conversion because checking may end at a judgmentally equal expected type. All oracle calls occur only at the typed premises displayed in the rule cards.

Referenced from 5 locations

Theorem 110.23 — Recheck soundness and round trip ¶

Assume the full-Timpl conversion and constructor-inversion operations required in definition 48.16. Independent annotation recheck terminates. If it accepts $(Γ, τ_{A}, e, A, a)$ , then $Γ ⊢ a : A$ . Moreover, paired successful runs $Γ ⊢ τ_{A} \Leftarrow type ⇝ A^{'}$ and $Γ ⊢ e \Leftarrow A ⇝ a$ , with $A^{'} \equiv A$ , produce a certificate accepted by the independent pass.

Referenced from 4 locations

Proof of Theorem 110.23 — Recheck soundness and round trip

Proof. Termination is the lexicographic argument of proposition 48.17; the table introduces no call not present in its rule. For soundness, simultaneously induct on the selected table entry. The type row applies, in order, the Timpl formation rule for $Π, Σ, Id, 1, 2, N, U$ , or U-El. The $Vec$ entry first applies Vec-form to obtain a universe code and then U-El to obtain a type. The synthesis row applies variable, elimination, projection, constructor, annotation, or eliminator typing with exactly the displayed recursive premises. The checking row applies the matching introduction or universe-code rule; its final entry uses soundness of conversion. Thus a successful $R_{chk} (Γ, e, A) = a^{'}$ reconstructs $Γ ⊢ a^{'} : A$ . Alpha-renaming gives the claim for $a$ .

For the round trip, first induct on the successful type elaboration, which reconstructs $A^{'}$ and makes completeness of conversion accept $A^{'} \equiv A$ . Then induct on the successful term elaboration and use the table entry with the same head. The base and projection entries are literal. The metadata entries reproduce the stored $(ϵ, ϱ)$ bits; the Boolean and natural eliminators reproduce their written motives; the vector entries reproduce $i, j, A, n, P$ and every branch field; and the identity entry reproduces its carrier, endpoints, and motive. The induction hypotheses therefore make the same recursive calls and return the same core tree up to bound names. Completeness of conversion discharges precisely the comparisons printed in Ty-El, Chk-Refl, and Chk-Conv; universal coherence gives the same constructor display in the four inversion clauses. Hence the reconstructed term is alpha-equal to $a$ , and the certificate is accepted. ◻

Corollary 110.24 — Kernel guarantee ¶

Under the oracle contract of definition 48.16, an exported certificate accepted by an implementation of definition 110.22 denotes a derivable object-theory judgment, independently of how the elaborator constructed the certificate.

Referenced from 3 locations

Proof of Corollary 110.24 — Kernel guarantee

Proof. Acceptance and theorem 110.23 give $Γ ⊢ a : A$ . The theorem’s proof inspects only the certificate and the trusted rule/oracle interface, so it has no premise about the elaborator’s internal search. ◻

Example 110.25 — The annotation boundary ¶

The bare application $(λ x . x) 0$ fails in synthesis mode because its function subterm is an introduction and has no synthesis rule. The annotation supplies the missing direction change: $\frac{\frac{x : N ⊢ x \Rightarrow N ⇝ x}{\cdot ⊢ λ x . x \Leftarrow N \to N ⇝ λ (x : N) . x} C h k - L a m}{\cdot ⊢ ((λ x . x) : N \to N) \Rightarrow N \to N ⇝ λ (x : N) . x} S y n - A n n$ Together with Syn-App and Syn-Zero, this synthesizes $N$ for $((λ x . x) : N \to N) 0$ . Generated and handwritten programs contain such redexes frequently; the exact fact is only that an introduction in synthesis position needs a local annotation.

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

Lemma 110.26 — Formation generation for Timpl ¶

In the economical presentation of Timpl, formation of a $Π$ , $Σ$ , identity type, or universe code gives the formation premises of its unique head rule. In particular, $Γ ⊢ \prod_{x : A} B type ⟹ Γ ⊢ A type and Γ, x : A ⊢ B type,$ For every other Timpl type head, including $2$ and $Vec$ , the corresponding statement replaces the $Π$ -formation premises by the premises of that head’s formation rule and preserves the stored metadata.

Referenced from 3 locations

Trusted Kernels and Bidirectional Checking

Proof of Lemma 110.26 — Formation generation for Timpl

Proof. Translate by theorem 26.43. The final nonstructural rule is either direct head formation, which has the claimed premises, or U-El, whose premise types a code for the same head in a universe. Invert that code-typing derivation at its last nonstructural rule; the corresponding universe-closure rule again exposes the same component formation premises. For each other head, inversion stops at its direct formation rule or at the matching universe-code rule and returns precisely that rule’s component premises. ◻

Theorem 48.19 — Soundness ¶

Suppose $Γ ctx$ . If $Γ ⊢ τ \Leftarrow type ⇝ A$ , then $Γ ⊢ A type$ ; if $Γ ⊢ A type$ and $Γ ⊢ e \Leftarrow A ⇝ a$ , then $Γ ⊢ a : A$ ; if $Γ ⊢ e \Rightarrow A ⇝ a$ , then $Γ ⊢ A type$ and $Γ ⊢ a : A$ .

Referenced from 5 locations

Proof of Theorem 48.19 — Soundness

Proof. Use simultaneous induction on the algorithmic derivation.

Type formers. In Ty-Pi, the induction hypotheses give $Γ ⊢ A type$ and $Γ, x : A ⊢ B type$ , so $Π$ -form gives the conclusion. The $Σ$ and identity cases use their formation rules. For Ty-El, synthesis gives $Γ ⊢ a : C$ and $unUniv$ gives $C \equiv U_{i}$ ; conversion yields $a : U_{i}$ , and U-El yields $Γ ⊢ a type$ .

Application and projections. In Syn-App, synthesis gives $f : C$ . Soundness of $unPiMeta$ gives $C \equiv \prod_{x : A}^{ϵ, ϱ} B$ ; conversion, the checked argument $a : A$ , and $Π$ -elim give $f a : B [a / x]$ . In Syn-Snd, $unSg$ gives $C \equiv \sum_{x : A} B$ ; conversion gives $p : \sum_{x : A} B$ and then ${pr}_{2} (p) : B [{pr}_{1} (p) / x]$ .

Introductions and switching. In Chk-Lam, inversion gives a display $C \equiv \prod_{x : A}^{ϵ, ϱ} B$ . Presupposition and lemma 110.26 give $A type$ in $Γ$ and $B type$ in $Γ, x : A$ , so the extended context is well formed and the induction hypothesis gives $b : B$ ; domain-annotated abstraction with the recovered bits, followed by conversion, gives $λ^{ϵ, ϱ} (x : A) . b : C$ . In the pair case, inversion gives $C \equiv \sum_{x : A} B$ ; the two checking induction hypotheses give $a : A$ and $b : B [a / x]$ , so $Σ$ -intro followed by conversion gives the required term at $C$ . In Chk-Conv, synthesis gives $a : C^{'}$ and soundness of algorithmic equality gives $C \equiv C^{'}$ , so conversion gives $a : C$ .

Reflexivity. The premise gives $c : A$ , $c \equiv a$ , and $a \equiv b$ . Hence ${refl}_{c} : {Id}_{A} (c, c)$ , while identity congruence gives ${Id}_{A} (c, c) \equiv {Id}_{A} (a, b)$ ; the latter is judgmentally equal to $C$ by soundness of $unId$ . Two conversions finish.

Booleans and vectors. The Boolean constructors use $2$ -intro $_{1, 2}$ . In Syn-BoolInd, the scrutinee conversion, motive, and two checking induction hypotheses are exactly the four premises of $2$ -elim; substitution gives the printed result type. For Syn-VNil and Syn-VCons, the universe, index, element, and tail premises are respectively Vec-form and the vector introduction rules. In Syn-VecInd, the motive is checked at $U_{j}$ in the $n, v$ context; the two method hypotheses have types $P_{0}$ and $P_{s}$ ; and the final two premises give $m : N$ and $y s : Vec (A, m)$ . These are exactly the premises of Vec-elim, whose conclusion is $P [m / n, y s / v]$ . Stored levels and metadata bits are copied unchanged to the kernel node.

Natural-number elimination. The induction hypotheses give the motive $C$ in $Γ, k : N$ , the zero branch at $C [0 / k]$ , the step branch in $Γ, n : N, y : C [n / k]$ at $C [suc (n) / k]$ , and $m : N$ after the displayed conversion. The exact rule $N$ -elim then gives the synthesized term at $C [m / k]$ .

For $J$ , synthesis gives $Γ ⊢ q^{'} : D$ and $unId (Γ, D) = (A, a, b)$ gives $D \equiv {Id}_{A} (a, b)$ . Conversion therefore gives $q^{'} : {Id}_{A} (a, b)$ . The other induction hypotheses give $\begin{aligned} Γ, x : A, y : A, p : {Id}_{A} (x, y) ⊢ C type, \\ Γ, z : A ⊢ c : C [z / x, z / y, {refl}_{z} / p] . \end{aligned}$ The official Id-elim rule now gives $J_{A; a; b} (x . y . p . C; z . c; q^{'}) : C [a / x, b / y, q^{'} / p],$ exactly the raw term and type returned by Syn- $J$ .

Universe codes. For Chk-Code-Pi, the two checked premises are terms $A : U_{i}$ and $B : U_{i}$ in the extended context. Rule U-Pi gives the metadata-bearing product at $U_{i}$ , and the equality returned by $unUniv$ converts this to $C$ . The $Σ$ and identity entries apply U-Sig and Id-form- $U$ ; $1, N, 2$ apply their nullary code rules; Chk-Code-Univ uses U-Hier; Chk-Code-Lift uses strict lifting; and Chk-Code-Vec applies Vec-form to the checked $A : U_{i}$ and $n : N$ . Variables and fixed constructors use their typing rules directly. ◻

Theorem 48.20 — Completeness up to annotation ¶

For every judgment of Timpl:

if $Γ ⊢ A type$ , some annotation of its surface image checks as a type and returns $A^{'} \equiv A$ ;
if $Γ ⊢ a : A$ , some annotation of its surface image checks against $A$ and returns $a^{'} \equiv a : A$ ;
under the same hypothesis, some annotation synthesizes $A^{'} \equiv A$ and returns $a^{'} \equiv a : A$ .

The surface image erases a kernel abstraction’s domain annotation; rule Chk-Lam reconstructs it from $unPiMeta$ applied to the expected type, while retaining its explicitness and relevance bits. It is otherwise homomorphic and keeps the written vector levels, parameters, motives, and indices, except that ${refl}_{a}$ is written $refl (a)$ and the three raw carrier/endpoint annotations on $J_{A; a; b}$ are erased. Rule Syn- $J$ reconstructs the latter from the synthesized type of its eliminand. The only subsequently inserted surface constructors are annotations $(- : τ)$ .

Referenced from 6 locations

Proof of Theorem 48.20 — Completeness up to annotation

Proof. First translate the derivation to the economical structural presentation by theorem 26.43. The formers of Timpl satisfy the stability hypotheses there, so the translated derivation has no final weakening, substitution, equal-substitution, or context-conversion rule. The induction uses the following strengthened checking claim: $\begin{matrix} (*) & \begin{matrix} Γ ⊢ a : A, Γ ⊢ A \equiv C type \\ ⟹ \exists e, a^{'} . Γ ⊢ e \Leftarrow C ⇝ a^{'} and Γ ⊢ a^{'} \equiv a : C . \end{matrix} \end{matrix}$ This claim checks a typed term against any judgmentally equal expected type. It holds uniformly when declarations of $Γ$ are replaced by judgmentally equal types; lemma 26.40 transports each premise before the recursive call. Induct simultaneously on economical type formation and term typing.

Types. Direct formation cases follow the corresponding Ty-* rules and the type induction hypotheses. Suppose instead that Russell decoding makes the code $A : U_{i}$ into a type. By the term induction hypothesis its surface image checks at $U_{i}$ ; wrap that image in the annotation $(- : U_{i})$ . Rule Syn-Ann synthesizes $U_{i}$ , and then Ty-El returns a code $A^{'} \equiv A$ . Thus this case uses only the smaller code-typing premise.

Introductions. The economical generation rule exposes the constructor. For an abstraction, universal coherence of $unPiMeta (Γ, C)$ identifies its returned bits, domain, and body with the ones in the typing derivation. Context conversion and the strengthened term induction hypothesis check the body at the returned body type; hence Chk-Lam applies. Pairs are identical with $unSg$ . For ${refl}_{a}$ , use $refl (e_{a})$ and Chk-Refl; the three endpoint equalities needed there come from the induction hypothesis and the equality $C \equiv {Id}_{A} (a, a)$ . Universe codes use the corresponding Chk-Code-* rule. By completeness of algorithmic equality, each required judgmental equality yields the corresponding algorithmic comparison.

Boolean introduction uses Syn-True or Syn-False. Boolean elimination retains its motive and recursively annotates its scrutinee and two branches, so Syn-BoolInd applies. For vector formation, choose the level already printed in its Timpl derivation and use Ty-Vec; vector introduction stores that level and element parameter and uses Syn-VNil or Syn-VCons. A final Vec-elim derivation already contains $i, j, A, P, p_{0}, p_{s}, m, y s$ . Recursively annotate those eight fields in their displayed contexts and use Syn-VecInd. Equal substitution in $m$ and $y s$ identifies the returned $P [m / n, y s / v]$ with the original result. The surface image retains $(ϵ, ϱ)$ , and universal coherence of $unPiMeta$ returns that same pair before a lambda or application induction hypothesis is used.

Application. A final $Π$ -elim has proper premises $Γ ⊢ f : \prod_{x : A}^{ϵ, ϱ} B, Γ ⊢ a : A .$ Use type completeness on $\prod_{x : A}^{ϵ, ϱ} B$ to obtain $Γ ⊢ τ_{f} \Leftarrow type ⇝ P$ with $P \equiv \prod_{x : A}^{ϵ, ϱ} B$ . By the strengthened term induction hypothesis, an image $e_{f}$ checks at $P$ , so $(e_{f} : τ_{f})$ synthesizes $P$ . If $unPiMeta (Γ, P) = (ϵ, ϱ, A^{'}, x . B^{'})$ , universal coherence gives $A^{'} \equiv A$ and $B^{'} \equiv B$ after context conversion. The induction hypothesis for $a$ therefore checks an image $e_{a}$ at $A^{'}$ , and Syn-App returns $B^{'} [a^{'} / x] \equiv B [a / x] .$ Here the equality uses the returned $a^{'} \equiv a$ and equal substitution. Application congruence applied to the two term induction hypotheses gives the returned equality $f^{'} a^{'} \equiv f a$ at this common result type. One final Chk-Conv checks this synthesized application at the arbitrary $C$ in (*). Projections use the same calculation with $unSg$ .

Dependent eliminators. For natural-number elimination, first annotate the checked image of the scrutinee by $N$ , so it synthesizes a term $m^{'} \equiv m$ . Type completeness elaborates the motive in $Γ, k : N$ . The two branch induction hypotheses check at $C [0 / k]$ and, in $Γ, n : N, y : C [n / k]$ , at $C [suc (n) / k]$ , using context conversion for the returned motive; equal substitution then identifies the synthesized result $C [m^{'} / k]$ with $C [m / k]$ . The motive binder $k$ and predecessor binder $n$ are distinct: substituting $suc (n)$ for $k$ removes $k$ while retaining the well-scoped $n$ . The congruence rule for $N$ -elimination applied to the motive, branch, and scrutinee induction hypotheses gives equality of the returned recursor with the original one.

For $J$ , annotate the checked eliminand so that it synthesizes a type $D \equiv {Id}_{A} (a, b)$ . Universal coherence of $unId (Γ, D)$ identifies its returned carrier and endpoints with the hidden annotations $A_{0}, a_{0}, b_{0}$ of the original raw $J_{A_{0}; a_{0}; b_{0}}$ . Use these component equalities to context-convert the motive and branch induction hypotheses. Type completeness then elaborates the motive in $Γ, x : A, y : A, p : {Id}_{A} (x, y)$ , and the branch induction hypothesis, after the same context conversions, checks at $C [z / x, z / y, {refl}_{z} / p]$ . Rule Syn- $J$ reconstructs the raw annotations and returns $C [a^{'} / x, b^{'} / y, q^{'} / p]$ , judgmentally equal to the result type of the original derivation by the three equal-substitution equations. A final Chk-Conv proves (*). The dependent $J$ -congruence rule of remark 30.2, applied to those same carrier, motive, branch, endpoint, and eliminand equalities, gives equality of the returned $J_{A; a; b}$ term with the original $J_{A_{0}; a_{0}; b_{0}}$ term.

Variables and fixed constructors synthesize directly and then use Chk-Conv. An economical conversion ending needs no circular appeal: its proper typing premise is handled by (*) at the converted target. These cases prove (1) and the strengthened (2).

For (3), given $a : A$ , assertion (1) gives an annotated type image $τ$ elaborating to $A^{'} \equiv A$ . Convert the given derivation to $a : A^{'}$ , apply the already proved strengthened assertion (2) to obtain an image $e$ checking at $A^{'}$ , and wrap it as $(e : τ)$ . Rule Syn-Ann synthesizes $A^{'}$ and returns a term judgmentally equal to $a$ after conversion back to $A$ . ◻

The local theorem has the same outward shape as two older checker results, but their inputs and conclusions do not match Timpl. Printing the three interfaces prevents a similarity of prose from becoming an illicit theorem transfer.

Convention 110.29 — Source checker interfaces ¶

For Coquand’s closure machine, let ${Exp}_{96}$ be its expressions. Let ${Val}_{96}$ and ${Env}_{96}$ be its closure values and finite environments. The four algorithmic relations have signatures $\begin{aligned} {whnf}_{96}, {conv}_{96} & \subseteq {Val}_{96} \times {Val}_{96}, \\ {check}_{96}, {infer}_{96} & \subseteq {Env}_{96} \times {Env}_{96} \times {Exp}_{96} \times {Val}_{96} . \end{aligned}$ The two environments in the last line assign closure values and their type values. In the source notation they support the mutually defined judgments $ρ; δ ⊢ M \Leftarrow v$ and $ρ; δ ⊢ M \Rightarrow v$ . Its soundness result says that $\begin{matrix} {check}_{96} ((), (), A, Type), \\ {check}_{96} ((), (), M, A ()) \end{matrix} ⟹ \begin{matrix} [[A {]]}_{C} : Type, \\ [[M {]]}_{C} : [[A {]]}_{C} . \end{matrix}$ in every model satisfying the source’s application, product, and Berry conditions. The object language has only variables, $Type : Type$ , dependent products, abstractions, and applications. The paper proves soundness, not termination or completeness for that inconsistent universe rule.

For the bidirectional-PCUIC source calculus, fix checker flags, a well-formed global environment $Σ$ , and a local context $Γ$ . The mutually defined judgments are $Σ; Γ ⊢ t ▹ T, Σ; Γ ⊢ t ◃ T, Σ; Γ ⊢ t ▹_{h} H,$ where the third family constrains the inferred head $h$ to a sort, product, or inductive family and returns the corresponding head data $H$ . Its soundness and completeness signatures are $\begin{aligned} \begin{matrix} wf (Σ), {wf}_{Σ} (Γ), \\ Σ; Γ ⊢ t ▹ T \end{matrix} & ⟹ Σ; Γ ⊢ t : T, \\ \begin{matrix} wf (Σ), {wf}_{Σ} (Γ), \\ {isType}_{Σ, Γ} (T), Σ; Γ ⊢ t ◃ T \end{matrix} & ⟹ Σ; Γ ⊢ t : T, \\ wf (Σ), Σ; Γ ⊢ t : T & ⟹ \sum_{T^{'}} (Σ; Γ ⊢ t ▹ T^{'}) \times (T^{'} ⪯_{Σ, Γ} T) . \end{aligned}$ The judgment family includes the displayed well-formation inputs before the two translations are defined. The smaller ${CC}_{ω}$ presentation in the thesis states the analogous soundness and completeness formulas explicitly.

Referenced from 4 locations

Proposition 110.30 — Exact comparison boundary ¶

Neither source theorem in convention 110.29 proves theorem 48.20. The bidirectional-PCUIC signatures restrict to the annotated $Π$ -and-universe core of Timpl after deleting the global environment, inductives, fixed points, cumulativity, and the remaining Timpl formers. Coquand’s signature compares only with the corresponding checking-mode fragment after a derivation has been stratified by universe levels.

Referenced from 3 locations

Proof of Proposition 110.30 — Exact comparison boundary

Proof. For PCUIC, take an empty global environment, retain variables, stratified sorts, products, annotated abstractions, and applications, and specialize $⪯_{Σ, Γ}$ to Timpl conversion. The first two displayed source conclusions then have the shapes of the local synthesis and checking soundness clauses. This restriction deletes $Σ$ -lookups, inductive heads, recursion, and cumulativity; it also deletes Timpl’s $Σ$ , base, identity, vector, lift, and metadata-specific cases. Hence it supplies no case of the induction in theorem 48.20 outside the common core.

For Coquand’s calculus, a total rule-preserving translation cannot send its single judgment $Type : Type$ to a strict Timpl universe: $U_{i} : U_{i + 1}$ , never $U_{i} : U_{i}$ . Assigning a level to each source occurrence and requiring every source product and universe premise to respect the successor hierarchy removes that obstruction, but the unannotated abstraction rule still has checking mode only. The source result then proves semantic soundness for that stratified common fragment. It does not provide Timpl annotations, full-signature completeness, or the six-former conversion interface required above. Thus both comparisons require a stated restriction, and neither replaces the local proof. ◻

Exercise 48.3 ¶

★★★ Extend Timpl by coproducts and by a sound, complete, universally coherent operation $unSum (Γ, C) = (A, B)$ in the sense of definition 48.10. Give exact checking rules for $inl (e)$ and $inr (e)$ and a synthesis rule for the dependent eliminator of definition 28.17. Verify termination and the eliminator’s soundness case.

Referenced from 3 locations

Exercise 48.4 ¶

★★☆ Work in the empty context with $A : = N$ and $a : = 0$ . For a literal identity head, take $unId$ to return its displayed carrier and endpoints. Consider the reflexivity instance of Syn- $J$ . Its motive is ${Id}_{N} (x, y)$ and its branch is $refl (z)$ . Display all algorithmic queries. Use the annotated eliminand $refl (0) : {Id}_{N} (0, 0) .$ Show that the elaborated result has type ${Id}_{N} (0, 0)$ .

Referenced from 3 locations

Elaborating definitions

A later declaration may compute with an earlier definition. Its elaboration context must therefore store both the declared type and the elaborated body.

Remark 48.21 — A definition is not a variable ¶

Consider the script $def c : N = suc (suc (0))$ followed by $def p : {Id}_{N} (c, suc (suc (0))) = refl (c)$ . If the elaborator treats $c$ as a hypothetical variable $c : N$ , the second declaration fails: the check $c \Leftrightarrow suc (suc (0)) : N$ in Chk-Refl is false for a variable. The definition must enter the context with the judgmental equality $c \equiv suc (suc (0))$ : in the vocabulary of functional programming, dependent $let$ is not $λ$ .

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

The kernel theory need not be extended. A defined elaboration context stores the definiens as typed metatheoretic data. The variable rule below retrieves that stored term; a checker may represent the retrieval by lazy $δ$ -reduction without changing the declarative equality.

Definition 48.22 — Defined elaboration contexts ¶

A defined elaboration context $(Γ; D)$ consists of a well-formed object context $Γ$ and a finite partial map $D$ . If $D (x) = (A, a)$ , then $(x : A)$ occurs in $Γ$ and $a : A$ is derivable in the prefix before $x$ ; in the full context it is understood after ordered weakening through the remaining suffix.

Every judgment of definition 48.16 acquires the parameter $D$ , for example $Γ; D ⊢ e \Rightarrow A ⇝ a$ . Recursive calls preserve $D$ ; under a fresh local binder the stored terms are weakened once more. The variable rule splits into

(x : A) \in Γ x \notin dom D

Γ; D ⊢ x \Rightarrow A ⇝ x

Syn-Var-Plain

D (x) = (A, a)

Γ; D ⊢ x \Rightarrow A ⇝ a^{↑ Γ}

Syn-Var-Def

Here $a^{↑ Γ}$ denotes that ordered weakening. Both rules are sound by weakening admissibility.

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

Remark 48.23 — The singleton alternative ¶

One can instead extend the object theory by a singleton type ${Sing}_{A} (a)$ . In ETT the encoding ${Sing}_{A} (a) : = \sum_{x : A} {Eq}_{A} (x, a)$ works: projection and reflection give the defining equality, while pair congruence, Eq-Uniq, and $Σ$ -eta give singleton eta. We do not use this alternative, because it would add a former whose normalization clauses would also have to be proved.

Referenced from 3 locations

Trusted Kernels and Bidirectional Checking

[3]

Definition 48.24 — Elaboration of declaration lists ¶

A declaration list is $d s ::= ε ∣ (def x : τ = e); d s$ . Its elaboration judgment is $Γ; D ⊢ d s ok$ :

Γ; D ⊢ ε ok

Decls-Nil

Γ; D ⊢ τ \Leftarrow type ⇝ A

Γ; D ⊢ e \Leftarrow A ⇝ a

Γ, x : A; D [x \mapsto (A, a)] ⊢ d s ok

Γ; D ⊢ (def x : τ = e); d s ok

Decls-Cons

A script is accepted when $\cdot; \emptyset ⊢ d s ok$ .

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

Example 110.35 — Elaborating the two declarations ¶

The first declaration checks $N$ as a type and $suc (suc (0))$ against $N$ , producing $a : = suc (suc (0))$ . Its recursive premise is taken in $c : N; D (c) = (N, a) .$ In the type of the second declaration, Syn-Var-Def elaborates $c$ to $a$ , so the type becomes ${Id}_{N} (a, a)$ . The same rule turns the endpoint of $refl (c)$ into $a$ , and Chk-Refl returns ${refl}_{a} : {Id}_{N} (a, a)$ . The generated kernel term contains the definiens itself; it never asks a hypothetical variable to compute.

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

Exercise 48.5 ¶

★★☆ Verify the singleton alternative of remark 48.23: define its introduction and projection, derive the defining equality by reflection, and derive eta using pair congruence, Eq-Uniq, and $Σ$ -eta.

Referenced from 3 locations

Exercise 48.6 ¶

★★☆ Add the declaration $def q : \prod_{n : N} {Id}_{N} (c, c) = λ n . refl (c)$ as the third declaration in the script. Write its elaboration and show explicitly how the stored definiens for $c$ is weakened under the fresh local binder $n : N$ .

Referenced from 3 locations

The oracle boundary in ETT

The bidirectional rules are conditional on total conversion and inversion oracles. Equality reflection supplies an exact counterexample to treating that condition as automatic.

Theorem 48.40 — ETT lacks injective Π -types ¶

Extensional type theory with $U_{0}$ does not have injective $Π$ -types in the sense of definition 48.10.

Referenced from 3 locations

Trusted Kernels and Bidirectional Checking

Proof of Theorem 48.40 — ETT lacks injective Π -types

Proof. Put $P : = \prod_{x : 1} 0, Q : = \prod_{x : 2} 0, Γ_{0} : = (p : {Eq}_{U_{0}} (P, Q)) .$ Reflection and U-El-Eq give $Γ_{0} ⊢ P \equiv Q type$ . Injectivity would therefore give $Γ_{0} ⊢ 1 \equiv 2 type$ .

The environment used in proposition 35.4 interprets both $P$ and $Q$ by the empty function set, so the Eq fiber in $Γ_{0}$ is inhabited. It interprets $1$ by a singleton and $2$ by a two-element set. Soundness would equate these sets, a contradiction. ◻

Theorem 48.47 — Undecidability of extensional equality ¶

For ETT with the Russell universes, no total Turing machine decides, from derivations of two well-typed terms in a common context and type, whether they are judgmentally equal.

Referenced from 4 locations

Proof of Theorem 48.47 — Undecidability of extensional equality

Proof. This is the judgmental-equality instance of theorem 35.49. Its fixed effective coding and machine model are convention 90.50; its reduction maps SK trees to typed terms in $Γ_{SK}$ , and lemma 35.46, lemma 35.47 proves $t \sim u ⟺ Γ_{SK} ⊢ ⌜ t ⌝ \equiv ⌜ u ⌝ : X .$ Thus the theorem uses the exact signature, input contract, and two directions of the earlier reduction, rather than repeating the SK development. ◻

Corollary 48.48 ¶

ETT with Russell universes admits no effective conversion invariant of definition 48.8. Moreover, no total algorithm decides all of its raw term-typing queries.

Referenced from 6 locations

Proof of Corollary 48.48

Proof. The first claim follows from proposition 48.9, theorem 48.47. The second is the typechecking instance of theorem 35.49. Concretely, the reduction sends typed endpoints $a, b : A$ to $Γ ⊢ {eqrefl}_{a} : {Eq}_{A} (a, b) .$ This judgment is derivable exactly when $a \equiv b : A$ : conversion gives the forward direction and Eq-Reflect the reverse. ◻

Remark 48.49 — The intensional contrast ¶

The SK encoding uses equality reflection to turn the hypotheses $e_{K}, e_{S}$ into judgmental equations. Replacing Eq by intensional identity leaves those hypotheses propositional, so the reduction no longer proves undecidable conversion for the base. Conversely, the proof-relevant normalization theorem at its own cumulative universe-bearing signature supplies none of the oracles assumed here: not for $T_{el}$ , and not for the $Π$ / $2$ fragment either, since the universe fibre its construction is built on cannot be struck out. These are two honest signature boundaries, not opposite global conclusions about all intensional theories.

Referenced from 2 locations

Trusted Kernels and Bidirectional Checking

Exercise 48.12 ¶

★★☆ Using definition 35.45, lemma 35.46, reconstruct the reflected K equation and one application-congruence step. Identify which rules supply reflexivity, symmetry, transitivity, and congruence although $Γ_{SK}$ contains only the K and S equations.

Referenced from 3 locations

Exercise 48.13 ¶

★★☆ Write both directions of the typing reduction in corollary 48.48 as derivation trees. Use the annotated constructor ${eqrefl}_{a}$ , and mark the precise use of conversion in one direction and reflection in the other.

Referenced from 3 locations

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 110.9, then complete exercise 110.10.

Exercise 110.9 ¶

★★☆ For application, the natural-number eliminator, and identity elimination, write the annotated term returned by synthesis and a separate checking derivation for that annotation. Mark precisely where normalization, constructor inversion, and context conversion enter.

Referenced from 4 locations

Exercise 110.10 ¶

★★★ Practical project.bidirectional-kernel-recheck Before implementing either pass, derive on paper the accepted annotated application, the accepted $J$ certificate, and the rejected natural-number step branch. Record the claimed and reconstructed types at every recursive call; these form the implementation’s test oracle. Implement in Agda or Kappa the finite trust-boundary signature $T_{recheck}$ , consisting of natural numbers, Booleans, nondependent functions, ascriptions, the displayed constant-motive natural eliminator, and natural-number identity with a constant-motive $J$ instance. This is an executable sub-signature of Timpl, not the auxiliary $T_{el}$ , because it contains Booleans. Give an independent rechecker for every annotation in that slice. Preserve scoping and the well-formedness of every synthesized type. The corpus must accept an annotated application, identity and successor functions, and a reflexivity $J$ certificate; reject a natural-number step branch at the wrong motive; and demonstrate that mutating the elaborator’s result annotation is caught by rechecking. State explicitly that this executable slice is not a checker for the full dependent Timpl signature of convention 110.16.

Referenced from 5 locations

Bibliographic notes.

Coquand’s source-checker interface and soundness theorem are in [Coq96]. The bidirectional PCUIC judgment and translations are in [LB22]; its smaller ${CC}_{ω}$ presentation states soundness and completeness in Theorems 4.1 and 4.3 on pp. 55–57. The cumulative normalization boundary is [Coq19]. Angiuli and Gratzer supply the elaboration vocabulary [AG26]. Abel treats normalization by evaluation [Abe13]. Hofmann gives the universe semantics and an undecidability proof for reflection [Hof95]; see also [Hof97]. The SK encoding follows [CCD21], with operational input from Statman [Sta00].