Definitional Functoriality and Generic Type-Former Action

Proof. Structural induction on $D$. For $\mathbf{1}$ and $\mathbf{K}(A)$, both sides reduce to the input. For $\mathbf{X}$, the first equation is the identity computation and the second is the definition of composition. For $D_1\times D_2$, the computation rule exposes two components; the two induction hypotheses make the corresponding components judgmentally equal, and pair congruence closes the equations. For $D_1\mathbf{+}{D}_2$, case analysis exposes $\mathsf{inl}$ or $\mathsf{inr}$, and the corresponding induction hypothesis closes that branch. For $\mathbf{\Sigma }(a:A).D(a)$, the first component is constant and the induction hypothesis for $D(a)$ proves the second component. These are all description constructors. The sum step uses the hypothesis that $v$ is constructor headed. Without it, the stuck term displayed before the proposition prevents the reduction. ◻

Proof. Identity is Desc-Map-Id. Composition is Desc-Map-Comp. The premises of those rules are exactly the typing hypotheses in the theorem; no case analysis on the argument is required. ◻

Proof. For $\mathrm{\Pi }$, apply the identity action to $h$ and $x$: beta reduction gives $\mathsf{id}(h(\mathsf{id}(x)))$, which reduces to $h(x)$; function eta closes the equation. For composition, beta-reduce the two nested actions. Both sides become the same term $$\lambda x.f_2(x)(f_1(g_2(x))(h(g_1(g_2(x)))))$$ after unfolding componentwise composition. For $\mathrm{\Sigma }$, projection and pair computation reduce identity to $(x,y)$, while both composite actions reduce to $(g_2(g_1(x)),f_2(g_1(x))(f_1(x)(y)))$. ◻

Proof. Induct on the first selection derivation. In Select-Here, $\mathsf{hred}(t)$ excludes Select-Under, whose first premise would be its negation; the second derivation is Select-Here. In Select-Under, the outer constructor of $t$ determines its unique frame $K$ because the frame grammar has one computational position per constructor. The second derivation cannot be Select-Here by the negative premise, so it uses the same frame. The induction hypothesis identifies the inner contexts and selected redexes. ◻

Proof. Apply the ordinary substitution lemma to the displayed derivation, first with $(\mathsf{id},u)$ and then with $(\mathsf{id},u^{\prime })$. This gives the two typing judgments with their possibly different result types. Substitution congruence applied to $u\equiv u^{\prime }:A$ gives both $B(u)\equiv B(u^{\prime })$ and equality of the plugged terms. The conversion rule changes the right-hand term from type $B(u^{\prime })$ to type $B(u)$, yielding the homogeneous equality displayed in the statement. For Frame-ListInd, these two types are exactly $P(u)$ and $P(u^{\prime })$; for Frame-Snd, they are $C({\pi }_{1}u)$ and $C({\pi }_1{u}^{\prime })$. The new Frame-Map has the constant family $B(z)=F(Y)$, so its case is Map-Ty and map congruence. ◻

Proof. Induct on $D$. The unit, constant, and parameter clauses follow by the definitions of substitution and generated action. The product clause applies the two induction hypotheses to the projections. The sum clauses apply the corresponding induction hypothesis below $\mathsf{inl}$ or $\mathsf{inr}$. For $\mathbf{\Sigma }(a:A).D(a)$, choose $a$ outside the five-set union printed in the statement. The first projection is substituted once, and the induction hypothesis for $D(a)$ gives the second projection. These are all description constructors. ◻

Proof. There are three action-bearing primitive families in the proved fragment. For $\mathrm{\Pi }$, write $\alpha =(g,f)$ and substitute into $\lambda x.f(x)(h(g(x)))$, alpha-renaming $x$ outside the six-set union printed in the statement; the ordinary substitution-under-binder equation gives the displayed right-hand side, and the formulas for $g_{12}$ and $f_{12}$ give identity and composition. For $\mathrm{\Sigma }$, again write $\alpha =(g,f)$ and substitute componentwise into $(g(x),f(x)(y))$; the formulas for $g_{21}$ and $f_{21}$ give the composition equation. For lists, substitution is defined homomorphically on the primitive syntax constructor ${\mathsf{map}}_{\mathsf{List}}$; identities and composites substitute in its map argument. $\mathbb{N}$ has no varying parameter and hence no action rule. These are all primitive formers in the proved fragment. ◻

Proof. Map-Comp instantiated at $f$, $g$ and $n$ is exactly $$\mathrm{\Gamma }⊢{\mathsf{map}}_F(f)({\mathsf{map}}_F(g)(n))\equiv {\mathsf{map}}_F(f{{\circ }_F}_{F}g)(n):F(Z)$$ and hence says $s\equiv s^{\prime }:F(Z)$. lemma 120.12 gives the type equality and places both sides in $E$, using conversion to compare them at $B(s)$. The neutrality side condition of definition 120.9 plays no part here: it schedules weak-head reduction deterministically and does not restrict the equation. ◻

Proof. We give the logical-relation argument, concentrating on the one clause changed by functoriality. Parameterize typing, multi-step weak-head reduction, and neutral conversion by an interface $I$ satisfying weakening, substitution, subject conversion, and deterministic weak-head reduction. Define type reducibility and reducible term conversion simultaneously by induction on a type-former tag. The $0,\mathbb{N},\mathrm{\Pi },\mathrm{\Sigma }$, and universe clauses are the usual Kripke clauses. A type $X$ is reducible as a list when it weak-head reduces to $\mathsf{List}(A)$ and every weakening of $A$ is reducible.

At a reducible list type, reduce both terms to normal forms. Two constructor forms are related when they are both nil with convertible stored parameters, or both cons with reducibly convertible heads and tails. For compacted neutrals use four clauses. Two ordinary neutrals are related by neutral conversion in $I$. Two forms ${\mathsf{map}}_{\mathsf{List}}(f)(n)$ and ${\mathsf{map}}_{\mathsf{List}}(f^{\prime })(n^{\prime })$ are related when $n$ and $n^{\prime }$ are neutrally convertible and, in every weakened context with $x:A$, the terms $fx$ and $f^{\prime }x$ are reducibly convertible at the target parameter. A mapped neutral is related to an ordinary neutral when the same condition compares its function body with $x$; the fourth clause is the converse. Eta-expansion of the two functions makes these clauses well typed even before reducibility of their source is known.

Simultaneous induction on the reducibility witnesses proves reflexivity, symmetry, transitivity, irrelevance of the chosen type witness, weakening, and closure under anti-reduction. Only transitivity of compacted neutrals is new. There are three middle-form possibilities: ordinary, mapped, or one of each. In each, transitivity of neutral conversion identifies the underlying neutrals; the induction hypothesis in the extended context composes the two body relations. If one side supplied the identity body, beta conversion turns that body into $x$. This produces exactly one of the four clauses above.

We next validate the functor equations. Induct on a reducible list term. Nil and cons compute constructorwise, using the induction hypotheses for the head and tail. An ordinary neutral uses the mixed compacted-neutral clause with body $\mathsf{id}x\equiv x$. A mapped neutral first uses definitionally associative composition in the domain category to compact nested maps, then uses the mapped–mapped clause and the induction hypothesis on the composed body. These four cases prove reducible identity and composition; no fusion equation is used.

The fundamental lemma is a simultaneous induction on typing and conversion. Variables use the related environment; substitution uses its Kripke extension; the ordinary constructor and eliminator cases use the corresponding reducibility clauses. Map-Ty uses the list clause just defined, Map-Id and Map-Comp use the preceding validation, and neutral compaction uses anti-reduction. Thus every well-typed term is reducible and every judgmental equality is reducible conversion. Instantiating $I$ by declarative typing gives weak-head normalization and subject reduction. Inspection of related normal forms gives injectivity and nonconfusion; inspection at $\mathbb{N}$ gives numeral canonicity.

For algorithmic typing, compare reduced types, ordinary neutrals, and compacted neutrals by mutual recursion. The compacted-neutral clauses are the four logical-relation clauses above, now read as syntax-directed rules; every recursive call either removes a constructor, descends into a neutral spine, or descends into a function body at a structurally smaller type. Hence comparison is decidable. Induction on algorithmic derivations proves soundness. Instantiating the same fundamental lemma by the algorithmic interface proves that every declarative equality is accepted, so declarative and algorithmic typing coincide. Decidable conversion and syntax-directed checking then give decidable type checking. This establishes every item in the theorem at the stated finite signature; no clause constructs actions for arbitrary indexed inductives. ◻

Proof. Use the type-former injectivity supplied by theorem 120.16. Induct on the first typing derivation and invert the second derivation after removing its final conversions. A variable has the unique declaration found at its de Bruijn position. The universe, $\mathbb{N}$, zero, and successor rules have fixed conclusions. Formation of $\mathrm{\Pi }$, $\mathrm{\Sigma }$, and lists is fixed by the types of their displayed components. For lambda and application, the induction hypotheses identify the annotated domain and function type; dependent-$\mathrm{\Pi }$ injectivity identifies the codomain after substitution. For a pair, the induction hypotheses identify the first component type and the second component type in its substituted fiber; dependent-$\mathrm{\Sigma }$ injectivity identifies the domain and fiber. For either projection, inversion gives the two candidate $\mathrm{\Sigma }$-types, and dependent-$\mathrm{\Sigma }$ injectivity identifies the selected component type. The $\mathbb{N}$- and list-eliminator syntax stores its motive and branches; inversion therefore gives the same motive instance, while the induction hypotheses identify the scrutinee and branch types.

For an action term, the annotated syntax stores $F,X,Y$. Inverting Map-Ty in both derivations gives the same result type $F(Y)$; constructor-action and neutral-action rules are instances of that rule, not additional typing conclusions. Map-Id, Map-Comp, and their description counterparts derive equality and introduce no typing alternative. Finally, if the first derivation ends in conversion, apply the induction hypothesis before that conversion and compose type equalities; if only the second ends in conversion, compose with its conversion premise. This list covers every term and conversion rule in the stated fragment. ◻

Proof. For the description rules, induction on $D$ gives ${\mathsf{map}}_D(f):[[D{]]}_X\to [[D{]]}_Y$; application typing then assigns the displayed common types. The fixed-former rules use the domain-morphism signatures in convention 120.1. This proves clause 1.

For clause 2, the only new reduction has source and target $$s={\mathsf{map}}_F(f)({\mathsf{map}}_F(g)(n)),s^{\prime }={\mathsf{map}}_F(f{{\circ }_F}_{F}g)(n).$$ The rule premises type both terms at $F(Z)$. The contextual reduction instance supplies $\mathrm{\Gamma },z:F(Z)⊢E[z]:B(z)$. By lemma 120.12, the target has type $B(s^{\prime })$ and $B(s)\equiv B(s^{\prime })$. Lemma 120.17 gives $A\equiv B(s)$; two conversions therefore assign $E[s^{\prime }]$ the original type $A$. This argument includes Frame-ListInd, where the two intermediate result types are $P(s)$ and $P(s^{\prime })$.

For clause 3, apply lemma 120.13 to the description rules and lemma 120.14 to Map-Ty, Map-Id, and Map-Comp. Substituting the typing premises rebuilds the same rule. These are the constructor computation, identity, composition, and neutral-compaction families introduced by the delta. ◻