ch:datatype-descriptions: ch:datatype-descriptions

Interpretation gives Hence the two roll maps have types They are the curried vector constructors after Unit introduction and product currying. For $P(n,xs):=\mathbb{N}$, the zero method ignores its layer and its unit $\mathsf{All}$ witness and returns $\mathsf{0}$. At successor index, write the layer as $(a,xs)$ and its $\mathsf{All}$ witness as $(\star ,k)$, where $k:\mathbb{N}$ is the result for $xs$. The successor method returns $\mathsf{suc}(k)$. Thus description induction computes the element count, or length, which agrees with the vector index. The generic constructor-node size of construction 80.12 would instead return $\mathsf{suc}(n)$.

For the cons branch, $f:\mathbb{N}\to \mathbb{N}$ is successor. At output $m$, the ${\mathrm{\Sigma }}_f$ clause interprets as $$\sum _{n:\mathbb{N}}{\mathsf{Id}}_{\mathbb{N}}(\mathsf{suc}(n),m)\times (A\times \mathsf{Mu}(D)(n)).$$ A witness contributes only together with $p:\mathsf{suc}(n)=m$. At $m=\mathsf{suc}(k)$, successor injectivity converts $p$ to $n=k$; transport reduces the payload to $A\times \mathsf{Mu}(D)(k)$. Conversely $n=k$ with reflexivity constructs that branch. Thus the fiber is equivalent to the regular normal form $\mathsf{K}(A)\times \mathsf{X}(k)$, while the principal code still records the result-index equation explicitly.

For $f:A\to B$, take carrier $\mathsf{List}(B)$ and algebra $$\alpha (\mathsf{inl}(\star )):=\mathsf{nil},\alpha (\mathsf{inr}((a,ys))):=\mathsf{cons}(f(a),ys).$$ Equation (80.2) gives the usual nil and cons map equations. For identity, induct on $xs$. At nil, the fold equation gives $\mathsf{map}(\mathsf{id},\mathsf{nil})=\mathsf{nil}$. At cons, where constructor congruence uses the induction hypothesis. Fold fusion with $h=\mathsf{id}$ alone would only compare the same map fold with itself.

Add $\mathsf{pi}(A,E):{\mathsf{Desc}}_i(I)$ for $A:{\mathcal{U}}_i$ and $E:A\to {\mathsf{Desc}}_i(I)$, with $$[[\mathsf{pi}(A,E)]](X):=\prod _{a:A}[[E(a)]](X).$$ Every recursive occurrence remains in a codomain, hence positive. The code lies in ${\mathcal{U}}_{i+1}$ and its interpretation in ${\mathcal{U}}_i$. Traversal needs an operation $(\prod _{a:A}G(B(a)))\to G(\prod _{a:A}B(a))$ for the applicative $G:{\mathcal{U}}_i\to {\mathcal{U}}_i$ and every $B:A\to {\mathcal{U}}_i$; an ordinary applicative does not provide it for infinite $A$. Decidable equality requires finite enumerability of $A$, decidable equality in every codomain, and function extensionality to turn pointwise equality into function equality.

For $t:\mathsf{Tm}(B::\mathrm{\Gamma },C)$, the left side computes to $$\mathsf{lam}(\mathsf{ren}({\mathsf{lift}}_{[B]}(\rho ),\mathsf{sub}({\mathsf{lift}}_{[B]}(\sigma ),t))).$$ The induction hypothesis turns its body into substitution by $$\mathsf{rpost}({\mathsf{lift}}_{[B]}(\rho ),{\mathsf{lift}}_{[B]}(\sigma )).$$ The right side computes to substitution by ${\mathsf{lift}}_{[B]}(\mathsf{rpost}(\rho ,\sigma ))$. On the newest variable, both environments return $\mathsf{var}(\mathsf{vz})$. On an older variable $\mathsf{vs}(x)$, both return the weakening of $\mathsf{ren}(\rho ,\sigma (x))$; renaming composition proves the equality for the first expression. Environment congruence identifies the bodies, and congruence of $\mathsf{lam}$ closes the case. No equality between environment functions is used.

The mirror algebra fixes a leaf and exchanges the two recursively folded children at a fork. The counting algebra sends a leaf to $1$ and a fork layer $(m,n)$ to $1+m+n$. In the leaf summand the fusion premise is $1=1$. In the fork summand it is $1+m+n=1+n+m$, by commutativity of natural-number addition. Fold fusion therefore gives $\mathsf{size}(\mathsf{mirror}(t))=\mathsf{size}(t)$ for every tree $t$.

At $\mathsf{con}(u)$, the left side of renaming after substitution expands to a constructor whose recursive-position map is $${\mathsf{ren}}_F({\mathsf{lift}}_{\mathrm{\Xi }}(\rho ),{\mathsf{sub}}_F({\mathsf{lift}}_{\mathrm{\Xi }}(\sigma ),x)).$$ The free-syntax induction hypothesis identifies this term with substitution by $\mathsf{rpost}({\mathsf{lift}}_{\mathrm{\Xi }}(\rho ),{\mathsf{lift}}_{\mathrm{\Xi }}(\sigma ))$. The lift lemma identifies that environment pointwise with ${\mathsf{lift}}_{\mathrm{\Xi }}(\mathsf{rpost}(\rho ,\sigma ))$. Layer-action congruence applies these paths at every $\mathsf{rec}(\mathrm{\Xi },B)$ position of $u$, and constructor congruence closes the case. For $\mathsf{lam}(t)$ the code stores $\mathrm{\Xi }=[B]$, so the sole premise is exactly the body equation with both environments lifted through the new variable of type $B$.

The Sigma clause first compares the tags $\mathsf{false}$ and $\mathsf{true}$. Boolean equality returns their disequality, so the procedure rejects before inspecting $\star$, $l$, or $r$. If equality data omit the decision procedure for $\mathbf{2}$, the algorithm cannot execute this first tag comparison. In particular it cannot obtain either a disequality for immediate rejection or a path $p:b=b^{\prime }$ along which to transport the second payload into the branch code $F(b)$.