ch:definitional-functoriality: ch:definitional-functoriality

An element of $[[D_i{]]}_X$ is a triple $(j,r,x)$ with $j:I$, $r:R(i,j)$, and $x:X(j)$. Hence $${\mathsf{map}}_{D_i}(f)(j,r,x)=(j,r,f_j(x)):[[D_i{]]}_Y.$$ Structural induction follows theorem 120.6. The only changed clause is the parameter case: ${\mathsf{map}}_{\mathbf{X}(j)}(\mathsf{id})(x)\equiv {\mathsf{id}}_j(x)\equiv x$. The dependent-sum and constant-product cases leave $j$ and $r$ fixed and apply this induction hypothesis to $x$, so the entire triple is judgmentally unchanged.

For maps $g:A\to B$ and $f:B\to C$, constructor computation gives $$\mathsf{map}f(\mathsf{map}g[])⟶[],$$ and, for $[a_1,a_2]$, two outer and two inner constructor reductions give $[f(g(a_1)),f(g(a_2))]$, the same constructor form as $\mathsf{map}(f\circ g)[a_1,a_2]$. For a neutral $n$, constructor reduction cannot fire; the single compaction step is $$\mathsf{map}f(\mathsf{map}gn)⟶\mathsf{map}(f{\circ }_{\mathsf{List}}g)n.$$ No identity expansion is used.

For $(g,f):(A,B)\to (A^{\prime },B^{\prime })$, where $g:A^{\prime }\to A$ and $f:\mathrm{\Pi }x:A^{\prime }.B(gx)\to B^{\prime }(x)$, the action is $M(g,f)(h)=\lambda x.f_x(h(gx))$. Identity reduces pointwise to $\lambda x.hx$ and eta gives $h$. For composable $(g_1,f_1)$ and $(g_2,f_2)$, both nested action and action of the componentwise composite reduce to $$\lambda x.f_{2,x}(f_{1,g_{2}x}(h(g_1(g_{2}x)))),$$ whose intermediate fiber is $B_1(g_1(g_{2}x))$. Reversing the domain map to $g:A\to A^{\prime }$ makes the first occurrence $h(gx)$ ill typed: $x:A^{\prime }$, so the reversed $g$ cannot be applied to $x$.