ch:indexed-inductive-families: ch:indexed-inductive-families

Induct on $xs$. The empty branch has $k:{\mathsf{Fin}}_{\mathrm{ind}}(\mathsf{0})$ and closes by empty elimination. In a successor branch $xs=\mathsf{vcons}(n,a,as)$, eliminate $k$. For $k=\mathsf{fz}(n)$, both sides compute to $f(a)$, so use reflexivity. For $k=\mathsf{fs}(n,l)$, the calculation is The first step is the two constructor computations; the second is the propositional induction hypothesis at $l$. It is not a judgmental map–lookup equation for a neutral tail.

At a $\delta (A,S)$ node the constructor field is a pair $(f,x)$ with $f:A\to \mathsf{IR}(S_0)$ and $x:{\mathsf{E}}_{S(\mathsf{El}\circ f)}(\mathsf{IR}(S_0),\mathsf{El})$. Thus the continuation is selected by the decoded recursive field $\mathsf{El}\circ f$, not by $f$ alone. The $\delta$ clause of $\mathsf{mapIH}$ is $${\mathsf{mapIH}}_{\delta (A,S)}(g,(f,x))=((\lambda a.g(f(a))),{\mathsf{mapIH}}_{S(\mathsf{El}\circ f)}(g,x)).$$ At a chosen $a:A$ its first component computes to $g(f(a))$; for $g={\mathsf{elim}}_{\mathsf{IR}}(P,m)$ this has type $P(f(a))$, exactly the recursive hypothesis consumed by the method.

The method has type $$q:(c:C(\mathrm{\Gamma }))\to T(\mathsf{ext}(\mathrm{\Gamma },\mathsf{U}(\mathrm{\Gamma })),x(c,u(c)),\mathsf{El}(\mathrm{\Gamma })).$$ Instantiate $c$ with $\mathsf{elimCon}(\mathrm{\Gamma })$. The target demanded by $\mathsf{elimTy}(\mathsf{El}(\mathrm{\Gamma }))$ has context-result index $\mathsf{elimCon}(\mathsf{ext}(\mathrm{\Gamma },\mathsf{U}(\mathrm{\Gamma })))$. The preceding computation rule rewrites this judgmentally to $x(\mathsf{elimCon}(\mathrm{\Gamma }),\mathsf{elimTy}(\mathsf{U}(\mathrm{\Gamma })))$, and the $\mathsf{U}$ computation rewrites the second argument to $u(\mathsf{elimCon}(\mathrm{\Gamma }))$. The resulting classifier is precisely the displayed type of $q(\mathsf{elimCon}(\mathrm{\Gamma }))$.

The solution transition applies to $x=\mathsf{suc}(y)$ because $x\notin \mathrm{FV}(\mathsf{suc}(y))$; it records $[\mathsf{suc}(y)/x]$ and leaves the empty equation list. For $\mathsf{suc}(x)=\mathsf{suc}(x)$, constructor injectivity first passes the vacuous index self-unification check for $\mathbb{N}$ and produces $x=x$. No solution transition applies because its occurs side condition fails, and deletion is absent, so the problem is stuck. Adding deletion would remove $x=x$ and report a positive solution, which is the forbidden step.

Put $L(n):=\mathsf{Vec}(A,\mathsf{suc}(n))\to A$. Natural-number induction defines The operations head and tail are the Vec-elim terms of construction 78.2, so this construction uses no pattern principle. Their computation rules give The first equation uses head computation; the second uses tail computation before the induction equation.

The constructor clauses are The case tree first splits the vector at index $\mathsf{suc}(n)$. Its only root is $$\mathsf{vcons}(.n,a,ys),$$ where the dot records the index equation forced by the scrutinee. It then splits $n$. At zero, $ys$ can only be $\mathsf{vnil}$; at successor, its only root is $\mathsf{vcons}(.n,b,xs)$. Neither split deletes a reflexive equation. The tree therefore satisfies definition 78.9.

The translation of theorem 78.19 is the eliminator-only definition where $\mathsf{head}$ and $\mathsf{tail}$ are the Vec-elim terms of construction 78.2. On the first leaf, head computation gives $a$. On the second, tail computation exposes the successor vector. The natural-number computation rule then gives the displayed recursive call. These are exactly the two leaf calculations of definition 78.18.

With $ys:\mathsf{Vec}(A,n)$ fixed, use motive $P(m,xs):=\mathsf{Vec}(A,n+m)$, branch $ys$, and successor branch $m.a.xs.q.\mathsf{vcons}(n+m,a,q)$. This is the eliminator term for append; addition recurses on its second argument, so both constructor branches have the displayed types judgmentally.

For right identity, first prove $l_m:\mathsf{0}+m=m$ by natural-number induction, with $l_{\mathsf{0}}:=\mathsf{refl}$ and $l_{\mathsf{suc}(m)}:=\mathsf{ap}(\mathsf{suc},l_m)$. Vector elimination on $xs$ proves $${\mathsf{transport}}_{k.\mathsf{Vec}(A,k)}(l_m,\mathsf{append}(xs,\mathsf{vnil}))=xs.$$ The empty case is reflexivity. The successor branch uses the transport lemma for $r:p=p^{\prime }$, proved by identity induction on $r$. Congruence of $\mathsf{vcons}$ with the vector induction hypothesis closes that branch. For a neutral $xs$, the eliminator does not contract, so $\mathsf{append}(xs,\mathsf{vnil})\equiv xs$ is not judgmental.