Fiber transport gives the Serre local systems

If maps $a_0,a_1:X\to Y$ are homotopic, [F2] supplies $a_{1\mathrm{\#}}-a_{0\mathrm{\#}}=\mathrm{\partial }P+P\mathrm{\partial }$. Hence they induce the same map in homology. Precomposition with this equality gives $a_1^{\ast }-a_0^{\ast }=\delta P^{\ast }+P^{\ast }\delta$ on cochains, where $(P^{\ast }\phi )(c)=\phi (Pc)$; thus they induce the same map in cohomology as well. A homotopy equivalence therefore induces isomorphisms in both theories.

For homology, path-homotopy invariance and composition follow from [F1] and step 1.1: $H_q(T_{\gamma \ast \eta })=H_q(T_{\eta })H_q(T_{\gamma })$. Constant paths give identity maps in homology even if the chosen lifting function is not regular, because [F1] makes their transports homotopic to the identity. Reversed paths give inverse maps. This is the covariant groupoid functor required by [F4].

Define cohomology transport along $\gamma :b\to c$ to be $S_{\gamma }=H^q(T_{\bar{\gamma }}):H^q(F_b;R)\to H^q(F_c;R)$. Since $\overline{\gamma \ast \eta }=\bar{\eta }\ast \bar{\gamma }$, [F1] gives $T_{\overline{\gamma \ast \eta }}\simeq T_{\bar{\gamma }}{T}_{\bar{\eta }}$. Contravariance and step 1.1 then give $S_{\gamma \ast \eta }=S_{\eta }{S}_{\gamma }$. Constants give identities, and $S_{\bar{\gamma }}$ is inverse to $S_{\gamma }$. Thus this too is a covariant fundamental-groupoid functor.

In the commutative square, write $u_b:F_b\to F_{f(b)}^{\mathrm{\prime }}$. For a path $\gamma :b\to c$, the two maps $u_c{T}_{\gamma }$ and $T_{f\gamma }^{\mathrm{\prime }}{u}_b$ are fiber transports over the same base path with the same initial fiber map. The lifting comparison in [F1] gives a vertical homotopy between them. Step 1.1 therefore gives $H_q(u_c)H_q(T_{\gamma })=H_q(T_{f\gamma }^{\mathrm{\prime }})H_q(u_b)$, exactly naturality of $H_q(F_b)\to H_q(F_{f(b)}^{\mathrm{\prime }})$.

Apply the same comparison to $\bar{\gamma }$. Contravariance gives $H^q(T_{\bar{\gamma }})H^q(u_b)=H^q(u_c)H^q(T_{\overline{f\gamma }}^{\mathrm{\prime }})$ as maps from $H^q(F_{f(b)}^{\mathrm{\prime }};R)$ to $H^q(F_c;R)$. This is naturality of the stalk maps $H^q(u_b):H^q(F_{f(b)}^{\mathrm{\prime }};R)\to H^q(F_b;R)$ from the pulled-back cohomology system to the source system.

Empty fibers give zero modules, and [F1] makes emptiness constant along each path component; point fibers and $q=0$ obey the same formulas. The zero ring gives zero systems. Disconnected bases are handled componentwise. A universal lifting function is one supplied map, and all subsequent transports and prism homotopies concern specified paths or maps; no family of representatives is selected, so no AC is used.