Declaration checking, copattern compilation, and erasure

Timpl-data is the finite regular mutual indexed-family declaration card of definition 122.1, translated constructor by constructor by definition 122.12 to the printed Tfam-block rules of definition 122.2. Its occurrence judgment carries both polarity and function-domain ancestry, admits a block family only at $(+,\mathsf{open})$, rejects recursive arguments inside applications of a block family, and admits any external type-level application only when its head and arguments are block-family-free — a covariant occurrence is positive but would need an $\mathsf{All}$ combinator the target does not have. Identity and primitive-vector types require all displayed arguments to be block-family-free; strict lift recurses at the same sign and ancestry state, using Lift-El conversion in hypothesis generation. Strict positivity is a premise of Block-I, so theorem 122.15 has content: the target schema does not derive an introduction rule for a rejected block. Every accepted binder yields the hypothesis type of definition 122.8. The generalized term ${\mathsf{ih}}_{\overrightarrow{P}}(A,x)$ is generated structurally from the simultaneous eliminators and inserted after every block-mentioning field, so computation inducts over function-typed and pair-typed recursive fields and not only over exposed ones. Rejection returns the ordered record of definition 122.5; lemma 122.6 identifies the exact failed formation, positivity, universe, or generated-rule premise. No-confusion is stated at one index instance, since two constructor applications need not inhabit the same type; the total-space form is its $\mathrm{\Sigma }$-packaging. The local results are accepted positivity (lemma 122.11), checker termination (lemma 122.10), generated-rule well-formedness (theorem 122.15), and elaboration soundness (theorem 122.16). They exclude nested and inductive–recursive declarations. They also exclude quotients, higher inductives, and large elimination beyond the solved maximum constraints. The Coquand–Paulin source motivates the primitive strictly positive rule shape; it is not a proof about this checker. The Kappa corpus decides six finite block fixtures in its stated five-node subgrammar with computed failure paths, computes the hypothesis type of every binder of an accepted block, and proves no normalization theorem.

Timpl-rec accepts finite first-order recursive groups whose clause trees were already typed, and whose intra-component calls carry either direct-child or explicit lexicographic predecessor certificates. The structural and lexicographic relations are those of definition 123.3, definition 123.4, assembled into the single relation $R_S$ on the generated nonrecursive datatype ${\mathsf{State}}_S$, with one constructor ${\mathsf{in}}_i:(\overrightarrow{a}:{\mathrm{\Delta }}_i)\to {\mathsf{State}}_S$ per function, by definition 123.10; that is the relation over which every later statement of the chapter quantifies. In the mutual-block structural case it is the inverse image of ${\mathsf{DChild}}_{\mathcal{B}}$, defined on every tagged inhabitant of the mutual block, along ${\mu }_i^{\mathcal{B}}$. The number $r$ of block families is independent of the number $q$ of functions, and the stored map $\kappa :{\mathsf{Fin}}_{\mathsf{ind}}(q)\to {\mathsf{Fin}}_{\mathsf{ind}}(r)$ selects the named argument’s family. The dependent payload family over ${\mathsf{Fin}}_{\mathsf{ind}}(r)$, its total-space carrier, and the generated ${\mathsf{DChild}}_{\mathcal{B}}$ block have the explicit levels $L_{\mathcal{B}}$ and $K_{\mathcal{B}}$ computed in definition 123.7; the latter is accepted by the Timpl-data formation, universe-output, and positivity checks. A leaf-specific $\mathsf{Child}$ certificate supplies a generator of that relation by lemma 123.11; it does not define $R_S$. Primitive $\mathbb{N}$ and $\mathsf{Vec}$ components instead use carriers $\mathbb{N}$ and $\sum _{n:\mathbb{N}}\mathsf{Vec}(c,n)$, maps ${\mu }_i^{\mathbb{N}}$ and ${\mu }_i^{\mathsf{Vec}}$, and their displayed child generators. Neither has a $\kappa$ map. All block arguments share one parameter vector. The deterministic rejection record of definition 123.5 names the component, internal call site, caller and callee tuples, selected discipline, and first failed predecessor premise; its soundness is lemma 123.6. Inverse-image well-foundedness and finite lexicographic products are proved locally in lemma 123.8, lemma 123.9. The distinct source and compiled relations ${\Downarrow }_{\mathsf{R}}$ and ${\Downarrow }_{\mathsf{RC}}$ are fixed by definition 123.15; both are parameterized by the accepted signature and include every generated Block-comp equation. Source R-Call corresponds to target C-Call; the latter has a deterministic nonempty raw-core expansion through the outer definition beta prefix, the state-block equation, WF-$\beta$, and compiler administrative beta steps. Program contexts do not reduce inside compiler-generated accessibility or predecessor evidence. Compiler-administrative beta redexes in a C-Call region are not separate target program roots. Their one-step and finite-closure correspondence is lemma 123.17, lemma 123.18. Body translation is definition 123.13. The local theorem theorem 123.19 supplies checker termination, typed accessibility-recursion elaboration, finite evaluation on closed constructor data, and agreement of returned constructor values; corollary 123.20 exposes the induced clause principle. It does not admit size-change inference, course-of-values recursion, higher-order recursive arguments, or arbitrary general recursion. Abel–Altenkirch is the historical call-order source, not an imported proof for Timpl-rec. The Kappa corpus computes strongly connected components and checks four finite call-graph cases, demanding a certificate only from intra-component edges.

Timpl-co is the stream-only, observation-driven card of definition 124.1. Each finite group fixes one element type $A$ and all its declarations return $\mathsf{Stream}(A)$; streams at different element types are checked in separate groups. Its right sides are restricted to producers, head aliases, and tail steps, so every edge weight is total and lies in $\{0,1\}$; remark 124.7 refutes the cycle criterion for the excluded deeper destructors. Mutual calls form a finite weighted graph; the accepted condition is acyclicity of its zero-edge subgraph, with a stored decreasing topological rank. Coiterator elaboration first generates a nonrecursive Timpl-data state block and then resolves head aliases statically, which terminates by that rank. The helper signature is program data rather than a new Timpl-co rule. When a destructor forces a source call, runtime arguments normalize as demanded subevaluation, while erased arguments are canonicalized statically by the same normalizer and are never forced by a runtime frame. The coiterator is correspondingly strict in its generated state: Coiter-Head and Coiter-Tail first normalize the state, and the latter normalizes the transition result before returning the next stream. The group-free relation $t{\Downarrow }_{\mathsf{T}}n$ is defined by $n=\mathrm{nf}(t)$, where the accepted Timpl NbE normalizer is extended declaration-by-declaration over the finite nonrecursive generated datatype signature. It has no named-call clause. Lemma 124.3 proves totality, typing, soundness, completeness, stability, and substitution invariance before preparation uses that interface. The inductive card T-Val–T-Vec-Cons instead defines the optional implementation relation ${\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}$: whenever it returns $v$, normalizing $v$ gives exactly the ${\Downarrow }_{\mathsf{T}}$ result. The CBV card is not the semantics of preparation or of any stream rule. Source/map agreement is lemma 124.14; preparation totality, substitution composition, and idempotence are lemma 124.4, lemma 124.12, lemma 124.13. The local productivity and coiterator simulation theorems are theorem 124.10, theorem 124.15; they quantify over finite observation words and do not assert normalization of a complete stream. The copattern source supplies the observation-first rule design, and Giménez supplies the guarded-recursion boundary; neither source proves the chapter’s exact graph criterion. Coinductive families, sized types, effects, and arbitrary record corecursors are outside the card. The Kappa observer derives the weighted graph from the declarations, checks a computed rank certificate at every vertex, replays the static alias resolution, and checks one finite prefix.

Tcop-clause contains finite ordered input patterns followed by dependent record coprojections; Tcop-tree carries typed field frontiers, and Tcop-core contains the printed primitive record corecursor Rec-Corec of definition 125.9 for exactly the declared finite telescopes. For a mutual group the compiler also generates the nonrecursive indexed Timpl-data family ${\mathsf{State}}_{\mathcal{G}}$, with constructor ${\mathsf{in}}_d(\overrightarrow{ı},\overrightarrow{a})$ for each declaration fiber. Its universe is the maximum of the index-telescope level and all declaration-fiber levels, as required by the Timpl-data level solver; this helper is signature data, not a new core rule. A recursive method returns a state, not a record. Methods are checked sequentially, and a later codomain contains the actual earlier application $v_l=h_l\overrightarrow{ı}s$, never an arbitrary earlier-result binder. The rule decodes a recursive output to ${\mathsf{corec}}_R{\overrightarrow{ı}}_l{v}_l$ before substituting the field into every later dependent method type and body; substituting the raw state would be ill typed. It also substitutes the generated self object ${\mathsf{corec}}_R\overrightarrow{ı}s$ for every source occurrence of $z$ in a nonrecursive field type and body. This self substitution and decoded-field substitution distinguish the rule from an unrestricted fixed point. The constant is declared at its method-independent type in a provisional signature. Previously checked method terms may beta-reduce while the next method is checked, but no coprojection equation is then available. The constant plus all coprojection equations are committed only after the complete sequential method judgment succeeds. The legal label–tail–flag example uses the earlier generated projection $\mathsf{label}:R\to \mathbf{2}$, not an ambient constant mentioning a record before its declaration. It witnesses decoded-field substitution without a second syntactic occurrence of $R$ in the record telescope. Source and target path extension are restricted to recursive fields, and the target’s distinct observation relation is ${\Downarrow }_{\mathsf{CC}}$ from definition 125.17. Its separate deterministic preparation relation ${⟹}_{\mathsf{in}}$ contracts only the outer input lambdas to the primitive object ${\mathsf{corec}}_R\overrightarrow{ı}({\mathsf{in}}_d(\overrightarrow{ı},\overrightarrow{a}))$ before an observation begins. It cannot select a field, input branch, or row, use Block-comp, or contract a corecursor projection. Its totality and functionality are lemma 125.16. After projection selects one method, that method’s translated split tree preserves the least matching row among rows for the demanded field. Source observation and all intermediate-tree executions are restricted to closed well-typed ready tuples in the sense of definition 121.5; source selection uses the relational $\mathsf{matches}$ judgment of definition 121.6. Under that hypothesis, lemma 125.8 proves source–tree agreement, including least-row choice at each field, and lemma 125.18 proves tree–core agreement. The first local translation preserves coverage and frontier typing; the second translates the typed tree without re-running matching. Their typing and composed observation theorems are theorem 125.7, theorem 125.14, theorem 125.19. The Cockx–Abel import is limited to Definitions 13–14, Lemmas 15–16, and Theorem 17: well-typed case trees make the signature respectful and hence type-preserving. The primitive-corecursor translation remains local. Higher-order patterns, projection overloading, hidden eta laws, effects, and arbitrary coinductive families are excluded. The Kappa corpus compiles the three-field orbit fragment and reads its printed tree, frontiers, and observation trace back out of the compiled spine.

The erasure pass checks inherited Timpl binder relevance by definition 126.9 and extends it to declarations. Acceptance by Timpl-data or Timpl-rec neither selects the retained fields of a constructor nor proves erasure admissibility. The pass checks the exact first-order phrase grammar with the named Rel-Erased, Rel-Var, Rel-Lam-R, Rel-App-R, Rel-App-E, Rel-Pair, Rel-Fst, Rel-Snd, Rel-Refl, Rel-Con, Rel-Case, Rel-Call, Rel-Bool-Elim, Rel-Nat-Elim, Rel-J, and Rel-Vec-Elim rules of definition 126.3. Recursive calls are saturated and non-first-class. Every type-valued binder is erased because Texec represents neither universes nor source type expressions; only represented data-valued indices may be runtime. An erased application is admitted only as a visible administrative redex, so a variable-headed erased application is outside the card. Sigma components are retained. A reflexivity proof occurring in a Sigma pair or runtime constructor field is represented by a nullary target tag; only a whole premise checked by Rel-Erased is deleted. Identity elimination deletes its proof and motive but structurally erases the reflexive branch and then substitutes the retained endpoint erasure when its binder is runtime. Primitive natural and vector eliminators compile to closure/call records whose tags are stable source-occurrence identifiers and whose lexical capture slots have a fixed declaration order. Their recursive hypotheses are installed through explicit target beta-redexes, so the recursive call is evaluated before its value is substituted into a source-CBV branch. Ordinary source records ${\delta }_s$ compile to explicit target records ${\delta }_t$ retaining exactly the runtime captures, inputs, and erased body. Target case patterns follow constructor-field retention, not branch use; retained-but-unused fields still contribute binders. The relevance-substitution lemma treats an arbitrary checked runtime-relevant source term and an arbitrary checked erased substituend separately and derives both runtime relevance and the corresponding erasure equation. The source premise is the separate big-step rule card for $\Downarrow$ in definition 126.5; disjoint source and Texec grammars determine which rule card applies. The ordinary named rules are S-Val, S-App-R, S-App-E, S-Pair, S-Fst, S-Snd, S-Con, and S-Case. The primitive and declaration rules are S-Bool-T, S-Bool-F, S-Nat-Z, S-Nat-S, S-J, S-Vec-Nil, S-Vec-Cons, and S-Call. The source relation evaluates runtime arguments and substitutes erased arguments as checked static syntax without evaluating them, matching target deletion. Source evaluation is sound for judgmental equality by lemma 126.6; its proof converts application fibres, pair projections, motives, indices, and identity endpoints explicitly. Typing preservation is lemma 126.7; runtime-relevance preservation is the separate lemma 126.8. These are the two premises used at each substituting case of forward simulation. The translation then targets the untyped call-by-value Texec calculus whose evaluation rules are displayed in definition 126.1, with tagged constructor blocks and closures applied by $\mathsf{call}$. The value relation of definition 126.12 replaces target typing. Local forward simulation is theorem 126.14; its induction enumerates runtime and erased beta, pairs and projections, reflexivity, constructors, all four primitive eliminators, datatype cases, and recursive calls. Stream execution has the explicit functional target judgment $\mathsf{Obs}(q,o,w)$, the separate finite-observation theorem theorem 126.19 and accepted-call corollary corollary 126.20, and assumes the productivity result of chapter 124. The bridge lemma 126.18 is restricted to the runtime-first-order map grammar of definition 126.15. It constructs the unique source-CBV value, proves that its NbE normal form is the ${\Downarrow }_{\mathsf{T}}$ result, and proves that normalization preserves every retained target field. Retained higher-order fields and internal helper applications are outside that card. Its tail closure is a fresh wrapper tag that computes $t(s)$, uses the unique related erasure of the resulting source state value, and constructs the next stream block; it is not the ordinary tag of $t:S\to S$. MetaCoq Figure 11, Lemmas 4.1–4.4, and Theorem 4.7 motivate the verified erasure architecture but concern PCUIC, not Timpl. The System Fi Definitions 1–2 and Theorems 1–7 are imported only for the exact interface of theorem 126.22: sorted-kind, context, kinding, equality, and term-typing preservation under index erasure. The strong-normalization and void-type consistency consequences are corollary 126.23. They supply neither Texec representation nor Timpl simulation. The Church vector erases to the ordinary Church list; the separate equality-constraint safe-tail witness erases to the printed equality-decorated list representation and retains its term-level equality evidence. The Kappa runner implements a finite first-order slice of the displayed Texec rules, executes the erased recursive closure rather than simulating it, uses a global constructor signature with pairwise-distinct case tags, and checks finite arities, closures, relevance, and observations. It does not implement the primitive Nat/Vec compiler records and proves neither local theorem.