Functoriality with coefficient morphisms

Define $(f,\eta {)}_{\mathrm{\#}}(m\sigma )={\eta }_{\sigma (e_0)}(m)(f\sigma )$. On the exceptional zeroth face, [F2] says ${\eta }_{\sigma (e_1)}{T}_{\sigma [0,1]}^{\mathcal{L}}=T_{f\sigma [0,1]}^{\mathcal{K}}{\eta }_{\sigma (e_0)}$; all other faces use the same first vertex. Hence this is a chain map and carries the subcomplex on $A$ into that on $B$, so [F1] gives the asserted $f_{\ast }$.

For a cochain $\phi$ on $Y$, define $((f,\theta {)}^{\mathrm{\#}}\phi )(\sigma )={\theta }_{\sigma (e_0)}(\phi (f\sigma ))$. The same naturality square, inverted on the exceptional face, makes this commute with coboundary. It preserves the relative kernel because $f(A)\subseteq B$, and hence induces the asserted $f^{\ast }$. Taking $f=1_X$ proves covariance in a coefficient morphism for both theories.

Substitution in the two displayed chain-level formulas proves the identity laws. For composable maps $X\stackrel{f}{\to }Y\stackrel{g}{\to }Z$, the homology coefficient morphism is $\mathcal{L}\to f^{\ast }\mathcal{K}\to f^{\ast }{g}^{\ast }\mathcal{N}=(gf{)}^{\ast }\mathcal{N}$, and the cohomology coefficient morphism is the reverse composite; componentwise substitution proves the composition laws without a basepoint or lift choice.

For a homotopy $H$, define $({\tau }_H{)}_x=T_{t\mapsto H(x,t)}^{\mathcal{K}}$. A path square $(s,t)\mapsto H(\gamma (s),t)$ shows by its two boundary routes that these components satisfy the naturality equation, so ${\tau }_H$ is a coefficient isomorphism. Triangulate each prism ${\mathrm{\Delta }}^n\times I$ as in the ordinary prism operator and transport the coefficient from its initial first vertex along the corresponding prism edge. The usual oriented-prism cancellation is unchanged; the only new comparisons are transports along the two boundary routes of a triangular face, and those are equal because the face supplies an endpoint-fixed homotopy. Thus the resulting $P_H$ satisfies $(f_1,{\eta }_1{)}_{\mathrm{\#}}-(f_0,{\eta }_0{)}_{\mathrm{\#}}=\mathrm{\partial }{P}_H+P_H\mathrm{\partial }$ when ${\eta }_1={\tau }_H{\eta }_0$.

Precomposing a local cochain with the prism operator and applying the coefficient map in the reverse direction gives a cochain homotopy $(f_1,{\theta }_1{)}^{\mathrm{\#}}-(f_0,{\theta }_0{)}^{\mathrm{\#}}=P_H^{\ast }\delta +\delta P_H^{\ast }$ when ${\theta }_0={\theta }_1{\tau }_H$. Chain- or cochain-homotopic maps induce equal maps on (co)homology by applying the identity to cycles/cocycles and observing that the difference is a boundary/coboundary. This proves the homotopy clauses. Empty pairs, zero systems, degree zero, degenerate simplices, and constant homotopies obey the same formulas, and no AC is used.