Consider the mutually recursive declarations 𝖳𝗋𝖾𝖾(𝐴)∋𝗅𝖾𝖺𝖿(𝑎)∣𝗇𝗈𝖽𝖾(𝑓),𝑓:𝖥𝗈𝗋𝖾𝗌𝗍(𝐴),𝖥𝗈𝗋𝖾𝗌𝗍(𝐴)∋𝖾𝗆𝗉𝗍𝗒∣𝗆𝗈𝗋𝖾(𝑡,𝑓),𝑡:𝖳𝗋𝖾𝖾(𝐴), 𝑓:𝖥𝗈𝗋𝖾𝗌𝗍(𝐴). Each recursive argument is data already constructed. Replacing the second constructor of 𝖳𝗋𝖾𝖾 by 𝖻𝖺𝖽:(𝖳𝗋𝖾𝖾(𝐴)→ℕ)→𝖳𝗋𝖾𝖾(𝐴) puts the family to the left of an arrow. The two declarations are equally short, yet only the first supports the induction step that receives hypotheses for every recursive child. A declaration processor must distinguish them before it generates a family or eliminator.
One declaration language
The checker below handles ordinary mutual indexed families. Nested, inductive–recursive, quotient, and higher inductive declarations require different rules and are not silently accepted.
Timpl-data is a surface declaration layer over the Timpl kernel as restated in convention 111.16. In particular, that signature contains the explicit strict lifts of definition 29.10 in addition to the type formers listed in convention 110.16. A finite block has the form B=𝖽𝖺𝗍𝖺 (Δ𝑝) {𝐷𝑟:(Δ𝑟)→Uℓ𝑟∣1≤𝑟≤𝑞} 𝗐𝗁𝖾𝗋𝖾 {𝑐𝑠:Θ𝑠→𝐷𝑟𝑠⃗𝑝⃗𝑢𝑠∣1≤𝑠≤𝑚}. The common parameter telescope Δ𝑝 is copied unchanged into every family and constructor. The family-specific telescope Δ𝑟 contains indices. Each constructor telescope Θ𝑠 may contain Timpl types, previous constructor arguments, and applications of a family in the same block. It may not quantify over a universe containing the block as data. The occurrence checker below has an explicit clause for every Timpl type former and every Timpl elimination form that can remain at the head of a type. Identity and primitive vector types are admitted only when all their type and term arguments are free of the block. Type-level eliminators and projections are admitted only when all their immediate subterms are free of the block. Supporting any of these forms over the block would require proof-specific or container-specific hypothesis generation absent from Tfam-block.
The target Tfam-block extends the same Timpl kernel, restated in convention 111.16 and named in convention 110.16. Its only primitive indexed family is the vector family of definition 78.1. Tfam-block adds one simultaneous formation rule for the finite family constants, one introduction rule for each constructor, and one simultaneous eliminator. It adds no equality reflection, quotient rule, large elimination beyond the universe maximum computed below, or nested fixed point. Constructor computation rules reduce only an eliminator whose scrutinee is headed by that constructor.
Referenced from 6 locations
The target name abbreviates the following rules, rather than an unspecified inductive extension. Write Σ ⊢Δ 𝖼𝗍𝗑 for telescope formation and assume that all displayed universes are accepted by the Timpl level solver.
For one component I ={𝐷1,…,𝐷𝑞}, simultaneous family formation and constructor introduction are Σ⊢Δ𝑝 𝖼𝗍𝗑(Σ,Δ𝑝⊢Δ𝑟 𝖼𝗍𝗑)1≤𝑟≤𝑞Σ⊢(𝐷𝑟:(Δ𝑝)(Δ𝑟)→Uℓ𝑟)1≤𝑟≤𝑞 𝗌𝗂𝗀Block−F and, for each constructor 𝑐𝑠, Σ,I,Δ𝑝⊢Θ𝑠 𝖼𝗍𝗑I⊢Θ𝑠 𝗉𝗈𝗌Σ,I,Δ𝑝,Θ𝑠⊢⃗𝑢𝑠:Δ𝑟𝑠Σ,I,Δ𝑝,Θ𝑠⊢𝑐𝑠(⃗𝑧):𝐷𝑟𝑠⃗𝑝⃗𝑢𝑠Block−I. The second premise is the strict-positivity judgment of definition 122.4, read on the whole telescope. It belongs to the target schema, not only to the source checker. If that premise were dropped, 𝖻𝖺𝖽 would be admitted. Blindly applying the function clause below to its field type would produce the method hypothesis ∏𝑦:𝖳𝗋𝖾𝖾(𝐴)𝟏. That hypothesis quantifies over the family being defined. The construction H is total only on accepted binder types, so the unchecked schema would otherwise be malformed. Theorem 122.15 discharges the premise from acceptance rather than assuming it.
For motives 𝑃𝑟:(⃗𝑝:Δ𝑝)(⃗𝑖:Δ𝑟)→𝐷𝑟⃗𝑝⃗𝑖→U𝑘𝑟 define the method type M𝑠(⃗𝑃,Θ) by scanning Θ𝑠. Its empty clause is M𝑠(⃗𝑃,⋅):=𝑃𝑟𝑠⃗𝑝⃗𝑢𝑠(𝑐𝑠(⃗𝑧)). A binder 𝑥 :𝐴 whose type is family-free contributes M𝑠(⃗𝑃,(𝑥:𝐴),Θ):=(𝑥:𝐴)→M𝑠(⃗𝑃,Θ). When 𝐴 mentions a family of I, the recursive clause is M𝑠(⃗𝑃,(𝑥:𝐴),Θ):=(𝑥:𝐴)→H⃗𝑃(𝐴,𝑥)→M𝑠(⃗𝑃,Θ), where the hypothesis type H⃗𝑃(𝐴,𝑥) is the induction hypothesis that 𝐴 yields for 𝑥, defined in definition 122.8 by recursion on the occurrence-check derivation of 𝐴. When 𝐴 contains no family of I, the hypothesis type is 𝟏, but the method’s second binder is omitted; when 𝐴 =𝐷𝑡 ⃗𝑝 ⃗𝑣 it is 𝑃𝑡 ⃗𝑝 ⃗𝑣 𝑥, the familiar case. The remaining telescope Θ keeps 𝑥 free.
Writing the clause this way, rather than only for an exposed recursive field, is what makes the eliminator usable on every binder the checker accepts. A field of type ℕ →𝖳𝗋𝖾𝖾(𝐴) or ∑𝑦:𝖳𝗋𝖾𝖾(𝐴)ℕ is strictly positive, and a schema whose only recursive clause were the exposed one would hand such a field no hypothesis at all — the generated eliminator would then not support induction over that field, and the block would be accepted on the strength of a rule that does not do its job.
The computation rule needs a term of every nontrivial hypothesis type, not only a type. Once the simultaneous eliminators are in scope, define 𝗂𝗁⃗𝑃(𝐴,𝑥) :H⃗𝑃(𝐴,𝑥) by the same recursion: 𝗂𝗁⃗𝑃(𝐴,𝑥):=⋆if no family of I occurs in 𝐴,𝗂𝗁⃗𝑃(𝐷𝑡⃗𝑝⃗𝑣,𝑥):=𝗂𝗇𝖽𝑡(⃗𝑝,⃗𝑣,𝑥),𝗂𝗁⃗𝑃(∏𝑦:𝐵𝐴′,𝑥):=𝜆𝑦.𝗂𝗁⃗𝑃(𝐴′,𝑥𝑦). For the pair clause, choose a binder 𝑤 ∉FV(𝐵) ∪FV(𝐴′) ∪FV(⃗𝑃) ∪{𝑥,𝑦}, and first form the recursive term in the context 𝑦 :𝐵,𝑤 :𝐴′. Then 𝗂𝗁⃗𝑃(∑𝑦:𝐵𝐴′,𝑥):=(𝗂𝗁⃗𝑃(𝐵,𝜋1𝑥),𝗂𝗁⃗𝑃(𝐴′,𝑤)[𝜋1𝑥/𝑦][𝜋2𝑥/𝑤]). The lift clause is 𝗂𝗁⃗𝑃(𝖫𝗂𝖿𝗍𝑢𝐴,𝑥):=𝗂𝗁⃗𝑃(𝐴,𝑥). The first clause again takes precedence. Hence its term is discarded when the corresponding 𝟏-hypothesis binder is omitted from the method.
With premises 𝑏𝑠 :M𝑠(⃗𝑃,Θ𝑠) for every constructor, simultaneous elimination and constructor computation are (𝑃𝑟:(⃗𝑝:Δ𝑝)(⃗𝑖:Δ𝑟)→𝐷𝑟⃗𝑝⃗𝑖→U𝑘𝑟)1≤𝑟≤𝑞(𝑏𝑠:M𝑠(⃗𝑃,Θ𝑠))1≤𝑠≤𝑚𝗂𝗇𝖽𝑟:(⃗𝑝:Δ𝑝)(⃗𝑖:Δ𝑟)(𝑧:𝐷𝑟⃗𝑝⃗𝑖)→𝑃𝑟⃗𝑝⃗𝑖𝑧Block−E,𝗂𝗇𝖽𝑟𝑠(⃗𝑝,⃗𝑢𝑠,𝑐𝑠(⃗𝑧))≡𝑏𝑠(⃗𝑧,⃗𝑧𝗂𝗁)(𝐵𝑙𝑜𝑐𝑘−𝑐𝑜𝑚𝑝). Here ⃗𝑧𝗂𝗁 contains, immediately after every field 𝑧 :𝐴 whose type mentions the block, the term 𝗂𝗁⃗𝑃(𝐴,𝑧). In the exposed recursive case 𝐴 =𝐷𝑡 ⃗𝑝 ⃗𝑣, this term is 𝗂𝗇𝖽𝑡(⃗𝑝,⃗𝑣,𝑧); the function and pair clauses supply the hypotheses for recursive values nested under those strictly positive type formers.
No-confusion is stated at one index instance, because 𝑐𝑠(⃗𝑎) and 𝑐𝑡(⃗𝑏) inhabit 𝐷𝑟𝑠 ⃗𝑝 ⃗𝑢𝑠[⃗𝑎] and 𝐷𝑟𝑡 ⃗𝑝 ⃗𝑢𝑡[⃗𝑏], and an identity type between them is not even well formed until those two types agree. Fix therefore a family 𝐷𝑟, an index vector ⃗ı :Δ𝑟, and arguments with 𝑟𝑠 =𝑟𝑡 =𝑟, ⃗𝑢𝑠[⃗𝑎] ≡⃗ı ≡⃗𝑢𝑡[⃗𝑏]. Distinct constructor tags then generate a map into the Timpl-definable encoded empty type 𝖤𝗆𝗉𝗍𝗒𝖳𝗂𝗆𝗉𝗅:=∏𝑋:U0𝑋. Thus the distinct-tag rule is 𝗇𝗈𝖢𝗈𝗇𝖿𝑠,𝑡:𝖨𝖽𝐷𝑟⃗𝑝⃗ı(𝑐𝑠(⃗𝑎),𝑐𝑡(⃗𝑏))→𝖤𝗆𝗉𝗍𝗒𝖳𝗂𝗆𝗉𝗅(𝑠≠𝑡), while one constructor tag generates an injection into the iterated, transported identity telescope of its arguments. Use the homogeneous telescopic equality ⃗𝑎 ≡Θ⃗𝑏 of definition 78.8; its recursive definition is exactly the required iterated transported identity telescope. The equal-tag rule has type 𝗂𝗇𝗃𝑠:𝖨𝖽𝐷𝑟𝑠⃗𝑝⃗ı(𝑐𝑠(⃗𝑎),𝑐𝑠(⃗𝑏))→⃗𝑎≡Θ𝑠⃗𝑏, again under ⃗𝑢𝑠[⃗𝑎] ≡⃗ı ≡⃗𝑢𝑠[⃗𝑏]. The displayed statements are the fiber at ⃗ı of the total-space rules of definition 78.11; the fiber form is the one the pattern compiler consumes. These are the only formation, introduction, elimination, computation, and no-confusion rules added by Tfam-block.
Referenced from 5 locations
Parameters and indices play different roles. In the tree–forest block, 𝐴 :U𝑖 is a parameter copied into every recursive occurrence. In 𝖵𝖾𝖼(𝐴,𝑛), the natural number 𝑛 is an index selected by each constructor result. Treating 𝑛 as a parameter would make 𝗏𝖼𝗈𝗇𝗌 return the same length that it receives and would destroy the intended family.
The dependency graph of B has a vertex 𝐷𝑟 for each family. Put 𝐷𝑟 →𝐷𝑡 exactly when an argument type of a constructor for 𝐷𝑟 mentions 𝐷𝑡. A strongly connected component (SCC) is a maximal vertex set whose members are mutually reachable. The processor treats each SCC as one mutual block and schedules it after all outside dependencies have passed. During constructor checking, all family constants of the block remain in scope.
Referenced from 2 locations
For tree and forest the graph has the two edges 𝖳𝗋𝖾𝖾 →𝖥𝗈𝗋𝖾𝗌𝗍 and 𝖥𝗈𝗋𝖾𝗌𝗍 →𝖳𝗋𝖾𝖾; hence one simultaneous block is forced. A one-family list declaration gives a singleton component with a self-loop.
Variance forces strict positivity
Let I be the set of families in one component. The checker traverses a type with a sign 𝜖 ∈{ +, −} and an ancestry flag 𝛿 ∈{𝗈𝗉𝖾𝗇,𝖻𝗅𝗈𝖼𝗄𝖾𝖽}. A function domain reverses the sign and blocks a recursive occurrence. A codomain preserves both data. Recall that Lift-U and Lift-El of definition 29.10 give 𝖫𝗂𝖿𝗍𝑖𝐴 :U𝑖+1 and 𝖫𝗂𝖿𝗍𝑖𝐴 ≡𝐴 whenever 𝐴 :U𝑖.
The judgment I;𝜖;𝛿⊢𝐴 𝗉𝗈𝗌 is generated by the following clauses.
A universe, a variable, an argument-free constant, 𝟏, 𝟐, and ℕ pass at either sign.
An application 𝐷 ⃗𝑝 ⃗𝑢 with 𝐷 ∈I passes exactly at state ( +,𝗈𝗉𝖾𝗇), provided no argument in ⃗𝑝,⃗𝑢 contains a family of I.
A dependent function type ∏𝑥:𝐴𝐵 passes at sign 𝜖 when I;−𝜖;𝖻𝗅𝗈𝖼𝗄𝖾𝖽⊢𝐴 𝗉𝗈𝗌andI;𝜖;𝛿⊢𝐵 𝗉𝗈𝗌.
A dependent pair ∑𝑥:𝐴𝐵 passes at sign 𝜖 when both components pass at state (𝜖,𝛿).
Any other well-formed type-level application 𝐻 ⃗𝑎, whose head is not a family of I, passes at either sign exactly when 𝐻 and every argument in ⃗𝑎 contain no family of I. Thus 𝐻 may be a local type-family variable or a family accepted in an earlier component.
An identity type 𝖨𝖽𝐵(𝑢,𝑣) passes at either sign exactly when 𝐵,𝑢,𝑣 contain no family of I.
A primitive vector type 𝖵𝖾𝖼(𝐵,𝑛) passes at either sign exactly when 𝐵,𝑛 contain no family of I.
A type-level eliminator or projection headed by 𝗂𝗇𝖽𝟐, 𝗂𝗇𝖽ℕ, 𝖩, 𝗏𝗂𝗇𝖽, 𝗉𝗋1, or 𝗉𝗋2 passes at either sign exactly when every immediate type and term argument contains no family of I. The checker treats such a type opaquely rather than reducing its head.
A strict lift 𝖫𝗂𝖿𝗍𝑢𝐴 passes at state (𝜖,𝛿) when I;𝜖;𝛿 ⊢𝐴 𝗉𝗈𝗌.
A constructor telescope Θ𝑠 is strictly positive, written I ⊢Θ𝑠 𝗉𝗈𝗌, when each binder type passes at state ( +,𝗈𝗉𝖾𝗇). A block passes when its telescopes are well formed, its dependency components are closed, and every constructor in every component is strictly positive.
Referenced from 11 locations
The declaration processor either returns an accepted Tfam-block signature or one record 𝖣𝖺𝗍𝖺𝖱𝖾𝗃𝖾𝖼𝗍(𝜙,𝐷𝑟,𝑐𝑠,𝜔,𝐸,𝑂). The phase 𝜙 is one of header formation, dependency closure, constructor-telescope formation, result-index checking, positivity, universe solving, or generated-rule checking. The family 𝐷𝑟 and constructor 𝑐𝑠 are present exactly when that phase lies inside their declarations. The path 𝜔 is the binder position followed by the preorder path in its type. The expected datum 𝐸 is the missing formation judgment, result telescope, positivity state (𝜖,𝛿), level inequality, or generated-rule type; 𝑂 is the observed head, sign and ancestry flag, index tuple, unsolved inequality, or inferred type that failed it.
Phases are tried in the displayed order. Components use topological order, families, constructors, and binders use source order, and a type scan uses left-to-right preorder. The processor returns the first failing record in that order. Thus a positivity failure reports the computed path and state, and a universe failure reports the first unsolved or inconsistent inequality; neither diagnostic is a fixture name or a fixed message.
Referenced from 4 locations
If the declaration processor returns 𝖣𝖺𝗍𝖺𝖱𝖾𝗃𝖾𝖼𝗍(𝜙,𝐷𝑟,𝑐𝑠,𝜔,𝐸,𝑂), then the declaration cannot produce a Tfam-block signature through the checked rule instance at that path: the premise named by 𝐸 has no derivation with observed datum 𝑂.
Referenced from 3 locations
Proof of Lemma 122.6 — Datatype rejection records a failed premise
Proof. Inspect 𝜙. Header, telescope, and result-index phases return only after the corresponding Timpl formation or typing procedure has rejected its printed judgment. Dependency closure returns an edge whose target is absent from the scheduled signature. In the positivity phase, induction along 𝜔 reconstructs every outer clause of definition 122.4; its final head has no clause at the stored sign and ancestry state. Universe solving returns an inequality with no solution in the accepted level algebra. Generated-rule checking returns a premise of Block-F, Block-I, or Block-E whose inferred type is not convertible to its expected type. These are all phases, and each failed premise is required by definition 122.2. ◻
Clauses 5–8 draw the opaque application-and-elimination boundary of Timpl-data. The generated eliminator, rather than polarity alone, determines this boundary. The lift clause is structural because Lift-El identifies the lifted type with its argument by conversion, without adding a new recursive container. A covariant occurrence such as 𝖫𝗂𝗌𝗍(𝐷) is perfectly positive; but the hypothesis for a field of that type is “𝑃𝐷 holds of every element of the list”, an 𝖠𝗅𝗅 combinator for 𝖫𝗂𝗌𝗍 that Tfam-block does not have. Excluding it here keeps the method construction below total.
For example, 𝖨𝖽ℕ(𝑚,𝑛) and 𝖵𝖾𝖼(ℕ,𝑛) pass whenever their terms are well scoped. The near variants 𝖨𝖽𝐷(𝑥,𝑦) and 𝖵𝖾𝖼(𝐷,𝑛) fail the family-free argument test. The former could be supported by a proof-specific clause and the latter by an 𝖠𝗅𝗅 hypothesis; this regular card provides neither construction.
If I;𝜖;𝛿 ⊢𝐴 𝗉𝗈𝗌 and (𝜖,𝛿) ≠( +,𝗈𝗉𝖾𝗇), then no family of I occurs in 𝐴.
Referenced from 3 locations
Proof of Lemma 122.7 — A nonpositive state is family-free
Proof. Induct on the displayed occurrence derivation. The base clause contains no family of I. The family clause has the two side conditions 𝜖 = + and 𝛿 =𝗈𝗉𝖾𝗇, contradicting the hypothesis. For a function type, a state different from ( +,𝗈𝗉𝖾𝗇) sends its domain to either negative sign or blocked ancestry, and sends its codomain the unchanged nonpositive state; apply the two induction hypotheses. The pair clause passes the same state to both components, so its two induction hypotheses apply directly. The lift clause uses its induction hypothesis at the unchanged state. The external-application, identity, vector, and opaque-elimination clauses require all displayed type and term arguments to be family-free. These are all rule families. ◻
Each accepted binder type determines the induction hypothesis its field contributes.
Fix motives ⃗𝑃. For a type 𝐴 with I; +;𝗈𝗉𝖾𝗇 ⊢𝐴 𝗉𝗈𝗌 and a variable 𝑥 :𝐴, define H⃗𝑃(𝐴,𝑥) by recursion on the occurrence-check derivation. When no family of I occurs in 𝐴, put H⃗𝑃(𝐴,𝑥):=𝟏. Otherwise use the following clauses. In the pair clause, suppose the type is ∑𝑦:𝐵𝐴′. Choose 𝑤 ∉FV(𝐵) ∪FV(𝐴′) ∪FV(⃗𝑃) ∪{𝑥,𝑦}, and define the recursive factor before substitution: H⃗𝑃(𝐷𝑡⃗𝑝⃗𝑣,𝑥):=𝑃𝑡⃗𝑝⃗𝑣𝑥,H⃗𝑃(∏𝑦:𝐵𝐴′,𝑥):=∏𝑦:𝐵H⃗𝑃(𝐴′,𝑥𝑦),H⃗𝑃(∑𝑦:𝐵𝐴′,𝑥):=H⃗𝑃(𝐵,𝜋1𝑥)×H⃗𝑃(𝐴′,𝑤)[𝜋1𝑥/𝑦][𝜋2𝑥/𝑤],H⃗𝑃(𝖫𝗂𝖿𝗍𝑢𝐴,𝑥):=H⃗𝑃(𝐴,𝑥). The first clause takes precedence over the others, so the recursion stops as soon as the block has disappeared from the type. There is no recursive clause for clauses 5–8 of definition 122.4, and none is needed: those clauses admit an external type-level application, identity, vector, opaque eliminator, or projection only when all of its arguments are family-free, so each such type falls under the first clause.
Referenced from 9 locations
The function clause is the one that uses polarity. It quantifies over the same domain 𝐵 that the field itself quantifies over, and that is legitimate only because 𝐵 was checked at negative sign: a family of I there would have been rejected, so the generated hypothesis never quantifies over the block being defined. For 𝗇𝗈𝖽𝖾 :𝖥𝗈𝗋𝖾𝗌𝗍(𝐴) →𝖳𝗋𝖾𝖾(𝐴) the hypothesis is 𝑃𝐹 𝐴 𝑓; for a field of type ℕ →𝖳𝗋𝖾𝖾(𝐴) it is (𝑛 :ℕ) →𝑃𝑇 𝐴 (𝑥 𝑛); and for a field of type ∑𝑦:𝖳𝗋𝖾𝖾(𝐴)ℕ it is 𝑃𝑇 𝐴 (𝜋1𝑥) ×𝟏, whose second factor is trivial because the ℕ component carries nothing to induct over. For 𝑥 :𝖫𝗂𝖿𝗍𝑢(𝖳𝗋𝖾𝖾(𝐴)), Lift-El converts 𝑥 to 𝖳𝗋𝖾𝖾(𝐴), so the generated hypothesis is 𝑃𝑇 𝐴 𝑥; the lift creates no extra recursive layer.
The check of the bad constructor reaches its argument type at ( +,𝗈𝗉𝖾𝗇), then reaches the domain 𝖳𝗋𝖾𝖾(𝐴) at ( −,𝖻𝗅𝗈𝖼𝗄𝖾𝖽), and rejects there. For 𝗇𝗈𝖽𝖾 :𝖥𝗈𝗋𝖾𝗌𝗍(𝐴) →𝖳𝗋𝖾𝖾(𝐴), the constructor telescope stores an argument of type 𝖥𝗈𝗋𝖾𝗌𝗍(𝐴); this is not the domain of a function occurring inside that argument type. The family is therefore visited at sign + and accepted.
For every finite Timpl-data block, dependency analysis, universe-constraint generation, and the occurrence check terminate.
Referenced from 4 locations
Proof of Lemma 122.10 — Termination of the declaration checker
Proof. Tarjan’s component procedure removes one unclassified vertex at each outer step and scans each finite edge list once. Universe generation traverses each finite telescope and emits finitely many inequalities between finite level expressions. The positivity procedure recurses on a strict syntactic subterm of the type being checked. In the two application clauses it inspects a finite argument list for occurrences of the block and never unfolds a family in it. The identity, vector, and opaque-elimination clauses likewise inspect finitely many type and term arguments without unfolding them. Lexicographic induction on the number of unclassified vertices and the remaining syntax size proves termination of the combined procedure. ◻
If Timpl-data accepts a block B, then for every component I and every constructor binder type 𝐴 in that component it returns a derivation I;+;𝗈𝗉𝖾𝗇⊢𝐴 𝗉𝗈𝗌. Every occurrence headed by a family of I in such a derivation is at state ( +,𝗈𝗉𝖾𝗇); none of its arguments contains a family of I; and no such occurrence lies in the domain of a function type or in an argument of an external type-level application, identity, vector, or opaque elimination.
Referenced from 4 locations
Proof of Lemma 122.11 — Accepted blocks are strictly positive
Proof. Acceptance checks every binder of every constructor telescope and stores the resulting occurrence derivation. Induct on one stored derivation. The base, pair, function, and lift clauses pass the induction hypotheses to their immediate subderivations. External-application, identity, vector, and opaque-elimination clauses contain no block family by their explicit side conditions. The only clause whose head belongs to I has the premises 𝜖 = +, 𝛿 =𝗈𝗉𝖾𝗇, and I ∩𝖥𝖺𝗆(⃗𝑝,⃗𝑢) =∅. Thus every such leaf has the two asserted properties. The outer checker starts each binder at ( +,𝗈𝗉𝖾𝗇), which gives the displayed derivation. For the last clause, a function domain is visited at ( −𝜖,𝖻𝗅𝗈𝖼𝗄𝖾𝖽). At sign − the family clause is not applicable, and at sign + the flag is 𝖻𝗅𝗈𝖼𝗄𝖾𝖽, so neither state admits an occurrence. Arguments of external applications, identities, vectors, and opaque eliminations are excluded by clauses 5–8 themselves. ◻
★☆☆ Trace definition 122.4 on (ℕ →𝖳𝗋𝖾𝖾(𝐴)) →ℕ. State the sign at the occurrence of 𝖳𝗋𝖾𝖾, and give the exact checker result.
Referenced from 3 locations
Generating the simultaneous family
Passing positivity is useful only because it constructs the premises needed by the eliminator. For each 𝐷𝑟, fix a motive 𝑃𝑟:(⃗𝑝:Δ𝑝)(⃗𝑖:Δ𝑟)→𝐷𝑟⃗𝑝⃗𝑖→U𝑘𝑟. Traverse a constructor telescope from left to right. Every argument is copied. Immediately after an argument 𝑧 :𝐴 whose type mentions the block, insert 𝑧𝗂𝗁:H⃗𝑃(𝐴,𝑧)with value𝗂𝗁⃗𝑃(𝐴,𝑧). For an exposed recursive argument 𝑧 :𝐷𝑡 ⃗𝑝 ⃗𝑣, these reduce to 𝑃𝑡 ⃗𝑝 ⃗𝑣 𝑧 and 𝗂𝗇𝖽𝑡(⃗𝑝,⃗𝑣,𝑧). Function and pair fields use the other two recursive clauses displayed in definition 122.2.
For tree and forest the generated methods have types 𝑏𝗅𝖾𝖺𝖿:(𝑎:𝐴)→𝑃𝑇(𝐴,𝗅𝖾𝖺𝖿(𝑎)),𝑏𝗇𝗈𝖽𝖾:(𝑓:𝖥𝗈𝗋𝖾𝗌𝗍(𝐴))→𝑃𝐹(𝐴,𝑓)→𝑃𝑇(𝐴,𝗇𝗈𝖽𝖾(𝑓)),𝑏𝖾𝗆𝗉𝗍𝗒:𝑃𝐹(𝐴,𝖾𝗆𝗉𝗍𝗒),𝑏𝗆𝗈𝗋𝖾:(𝑡:𝖳𝗋𝖾𝖾(𝐴))→𝑃𝑇(𝐴,𝑡)→(𝑓:𝖥𝗈𝗋𝖾𝗌𝗍(𝐴))→𝑃𝐹(𝐴,𝑓)→𝑃𝐹(𝐴,𝗆𝗈𝗋𝖾(𝑡,𝑓)). The simultaneous eliminators 𝗂𝗇𝖽𝑇,𝗂𝗇𝖽𝐹 apply the matching method and recursively supply the displayed hypotheses.
After solving levels, translation processes each dependency component once. It emits these target declarations in order.
Each source family header 𝐷𝑟 :(Δ𝑟) →Uℓ𝑟 emits the same family constant under the copied parameter telescope by Block-F.
Each source constructor 𝑐𝑠 :Θ𝑠 →𝐷𝑟𝑠 ⃗𝑝 ⃗𝑢𝑠 emits one Block-I instance with the same name, argument order, result indices, and homomorphic translation of every nonrecursive type former.
Each constructor binder is copied into the method telescope and followed by the hypothesis binder of definition 122.8, which is omitted exactly when that binder does not mention the block.
The source mutual eliminator emits the family (𝗂𝗇𝖽𝑟)𝑟 from Block-E; the equation for constructor 𝑐𝑠 emits exactly its displayed constructor computation rule.
Each ordered pair of distinct constructor tags emits 𝗇𝗈𝖢𝗈𝗇𝖿𝑠,𝑡; each constructor emits its transported argument injection. No other declaration is generated.
Referenced from 4 locations
The construction Θ′(𝑋,𝑃,𝑢) of Coquand and Paulin-Mohring places all source fields before all generated hypotheses. Tfam-block instead places a field’s hypothesis immediately after that field. Repeated dependent exchange transports between the two telescopes: a generated hypothesis does not occur in any later source field type, and a later source field does not occur in the earlier hypothesis type.
Define the level of a telescope by 𝗅𝖾𝗏(⋅):=0,𝗅𝖾𝗏(𝑥:𝐴,Δ):=max(𝑗,𝗅𝖾𝗏(Δ))when 𝐴:U𝑗. For a constructor returning 𝐷𝑟 :Uℓ𝑟, every argument type must inhabit a universe accepted by Timpl. For motives 𝑃𝑟 :(⃗𝑝 :Δ𝑝)(⃗𝑖 :Δ𝑟) →𝐷𝑟 ⃗𝑝 ⃗𝑖 →U𝑘𝑟, the declaration processor emits the maximum 𝐿:=max(𝗅𝖾𝗏(Δ𝑝),max𝑟𝗅𝖾𝗏(Δ𝑟),max𝑠𝗅𝖾𝗏(Θ𝑠),max𝑟ℓ𝑟,max𝑟𝑘𝑟). The maximum of an empty finite list of telescope levels is 0. The generated eliminator package inhabits U𝐿. Thus parameter- and index-telescope levels contribute even when no constructor argument mentions them. The processor sends this maximum and the component inequalities to the level solver; a failed or stuck solve rejects the block. Independently, 𝖤𝗆𝗉𝗍𝗒𝖳𝗂𝗆𝗉𝗅 :U1, so each distinct-tag no-confusion map has a fixed, solved codomain level.
Referenced from 8 locations
★☆☆ Give the tree–forest block the parameter telescope Δ𝑝 =(𝐴 :U𝑖), no index telescope, family levels ℓ𝑇 =ℓ𝐹 =𝑖, and motive levels 𝑘𝑇 =𝑘𝐹 =𝑘. Assume every constructor-field type inhabits U𝑖. Compute 𝗅𝖾𝗏(Δ𝑝), the maximum 𝐿 emitted by definition 122.13, and the maximum obtained if the parameter telescope were incorrectly omitted.
Referenced from 3 locations
Let 𝐴 satisfy I; +;𝗈𝗉𝖾𝗇 ⊢𝐴 𝗉𝗈𝗌 and let 𝑥 :𝐴. Then H⃗𝑃(𝐴,𝑥) of definition 122.8 is defined and is a well-formed type. Every function type introduced by the recursive Π-clause of H has a domain containing no family of I. The family-free clause is selected exactly when no family of I occurs in 𝐴, and that clause returns 𝟏. Once the simultaneous eliminators (𝗂𝗇𝖽𝑟)𝑟 are in scope, the term 𝗂𝗁⃗𝑃(𝐴,𝑥) has type H⃗𝑃(𝐴,𝑥).
Referenced from 3 locations
Proof of Lemma 122.14 — Every accepted binder yields a hypothesis
Proof. Induct on the occurrence-check derivation of 𝐴. If no family of I occurs in 𝐴, the first clause gives 𝟏 and there is nothing more to check. This covers the base, external-application, identity, vector, and opaque-elimination clauses, because their side conditions say directly that every displayed type and term argument is family-free.
If 𝐴 =𝐷𝑡 ⃗𝑝 ⃗𝑣, the family clause of the occurrence check gives 𝜖 = +, 𝛿 =𝗈𝗉𝖾𝗇 and family-free ⃗𝑝,⃗𝑣, so 𝑃𝑡 ⃗𝑝 ⃗𝑣 𝑥 is well formed. No restriction is imposed on function types chosen inside the motive value itself. The eliminator typing rule gives 𝗂𝗇𝖽𝑡(⃗𝑝,⃗𝑣,𝑥) :𝑃𝑡 ⃗𝑝 ⃗𝑣 𝑥.
If 𝐴 =∏𝑦:𝐵𝐴′, the occurrence check derived I; −;𝖻𝗅𝗈𝖼𝗄𝖾𝖽 ⊢𝐵 𝗉𝗈𝗌. By lemma 122.7 no family of I occurs in 𝐵, so the induction hypothesis applies to 𝐴′ in the context extended by 𝑦 :𝐵, and ∏𝑦:𝐵H⃗𝑃(𝐴′,𝑥 𝑦) is well formed with a family-free domain. This is the step at which polarity is doing the work: without it the generated hypothesis could quantify over the very family being defined. Lambda abstraction over the induction-hypothesis term gives 𝜆𝑦.𝗂𝗁⃗𝑃(𝐴′,𝑥 𝑦) the displayed function type.
If 𝐴 =∑𝑦:𝐵𝐴′, the stored derivation has a subderivation for 𝐵 and a subderivation for 𝐴′ in the context extended by 𝑦 :𝐵. Choose 𝑤 ∉FV(𝐵) ∪FV(𝐴′) ∪FV(⃗𝑃) ∪{𝑥,𝑦}. The two induction hypotheses give H⃗𝑃(𝐵,𝜋1𝑥) and, in context 𝑦 :𝐵,𝑤 :𝐴′, the type H⃗𝑃(𝐴′,𝑤) together with its generated term. First substitute 𝜋1𝑥 for 𝑦; then substitute 𝜋2𝑥 for 𝑤. Pair introduction gives (𝗂𝗁⃗𝑃(𝐵,𝜋1𝑥),𝗂𝗁⃗𝑃(𝐴′,𝑤)[𝜋1𝑥/𝑦][𝜋2𝑥/𝑤]):H⃗𝑃(𝐵,𝜋1𝑥)×H⃗𝑃(𝐴′,𝑤)[𝜋1𝑥/𝑦][𝜋2𝑥/𝑤]. If 𝐴 =𝖫𝗂𝖿𝗍𝑢𝐴′, the occurrence derivation has a strict subderivation for 𝐴′ at the same state. Rule Lift-El gives 𝖫𝗂𝖿𝗍𝑢𝐴′ ≡𝐴′, so conversion types 𝑥 :𝐴′. The induction hypothesis defines and types H⃗𝑃(𝐴′,𝑥) and its generated term. This is exactly the displayed lift clause of H and 𝗂𝗁⃗𝑃. Finally, the recursion terminates because each clause recurses on a strict subderivation. ◻
Let B be accepted by Timpl-data. Every generated family, constructor, mutual eliminator, constructor computation rule, and no-confusion instance is well formed in Tfam-block at the levels solved for B.
Referenced from 7 locations
Proof of Theorem 122.15 — Generated-rule well-formedness
Proof. Process dependency components in topological order. Simultaneous formation puts precisely the family constants of one component in scope. Constructor typing follows from the accepted telescope and result checks in definition 122.12. The remaining premise of Block-I is I ⊢Θ𝑠 𝗉𝗈𝗌, and lemma 122.11 supplies exactly that derivation for every constructor binder; this is the step at which a rejected block such as 𝖻𝖺𝖽 fails to produce a Tfam-block introduction rule. For each constructor method, lemma 122.14 supplies a well-typed hypothesis type after every binder. The family-free clause is selected exactly at binder types that do not mention the block, and every function domain introduced by the hypothesis recursion is family-free. The mutual eliminator is then the simultaneous Tfam-block rule for those methods. Substitution of a constructor into its motive gives the type of the corresponding computation rule.
For no-confusion, distinct constructor heads map to distinct tags. Equal heads reduce constructor equality to equality of their telescope arguments, transported along the result-index equality generated by the constructor typing derivation. Repeat the two case analyses of definition 78.11. In a distinct-tag branch, fix 𝑋 :U0; the branch gives a map from constructor equality to 𝑋. Abstracting 𝑋 gives the displayed map into 𝖤𝗆𝗉𝗍𝗒𝖳𝗂𝗆𝗉𝗅. In an equal-tag branch, the same construction returns ⃗𝑎 ≡Θ𝑠⃗𝑏. Universe well-formedness follows from the solved maximum constraint and the fixed U1 codomain recorded in definition 122.13. ◻
If the declaration processor accepts B and returns a Tfam-block signature ΣB, then ΣB is a well-formed extension of Timpl. Every source constructor application elaborates to the constructor of the same name and type, and every generated source eliminator equation is a Tfam-block computation rule.
Referenced from 3 locations
Proof of Theorem 122.16 — Timpl-data elaboration soundness
Proof. Checker termination is lemma 122.10. Acceptance gives well-formed telescopes, solved levels, closed dependency components, and the positivity derivations. Apply theorem 122.15 component by component. Translation is homomorphic on parameters, indices, constructor arguments, and constructor names, so constructor typing is preserved. The translation of an eliminator is the generated simultaneous eliminator; at a constructor its target reduction is the generated computation rule. Thus all three conclusions hold. ◻
The primitive-inductive restriction and the role of strict positivity follow the rule construction of Coquand and Paulin-Mohring, Sections 1.1–1.4 [CPM90]. Their calculus does not prove the checker theorem for Timpl-data; the preceding proofs use the finite grammar fixed in definition 122.1.
Suggested first pass.
None of these problems is a prerequisite for a later chapter. Begin with exercise 122.3, then complete exercise 122.5.
★★☆ For the tree–forest block, write the two motives, all four method types, and the computation of 𝗂𝗇𝖽𝐹 on 𝗆𝗈𝗋𝖾(𝗅𝖾𝖺𝖿(𝑎),𝖾𝗆𝗉𝗍𝗒). Annotate both recursive steps by the constructor computation rule used.
Referenced from 4 locations
★★☆ Compare (𝐷 →ℕ) →ℕ and ℕ →𝐷 as constructor argument types for a family 𝐷. Give the complete polarity trace and explain why the first is outside the regular Timpl-data card even though its two sign reversals leave the occurrence positive.
Referenced from 3 locations
★★★ Practical project.datatype-block-positivity-checker Implement in Kappa the five-node grammar of base, function, pair, block-family, and external-family applications. Implement occurrence clauses 1–5 and then definition 122.8. Identity, primitive-vector, and strict-lift clauses, together with the opaque-elimination clause, remain outside the program. The finite program is simply typed: its function and pair nodes bind no variable, so it does not exercise the dependent-pair substitution of definition 122.8. Maintain positive sign, open ancestry, and exclusion from recursive or external-family arguments. Derive the first failing path rather than printing a fixed diagnostic. Accept tree-forest and branching; for the latter, print every generated hypothesis type. Reject negative-bad, nested-bad, double-negative, and former-bad, naming the failing sign, flag, or argument. Replay three oracle-failing mutations: treat a function domain as a codomain; reverse its sign but leave ancestry open; and omit the hypothesis generated for a function field. The second is not exposed by negative-bad, and the third changes no acceptance verdict. The program proves no normalization theorem and does not implement clauses 6–9.
Referenced from 5 locations