Fiber transport is functorial on the base fundamental groupoid

Write $J_b:H_q(F_b;R)\to H_q(F_b^{\mathrm{\prime }};R)$ for the homology comparison. By [F1], ${\tau }_{\gamma }=J_c^{-1}{H}_q(T_{\gamma })J_b\mathrm{.}$ For the constant path, [F2]–[F3] give $H_q(T_{c_b})=\mathrm{id}$, so ${\tau }_{c_b}=\mathrm{id}$. Endpoint-fixed homotopic paths have equal middle maps. For composable $\gamma ,\eta$, the middle identity $H_q(T_{\gamma \ast \eta })=H_q(T_{\eta })H_q(T_{\gamma })$ makes the adjacent $J_c{J}_c^{-1}$ cancel and gives ${\tau }_{\gamma \ast \eta }={\tau }_{\eta }{\tau }_{\gamma }$. Thus [F4] applies, with no choice.

Under [F5], write $K_b=(j_b{)}^{\ast }:H^q(F_b^{\mathrm{\prime }};R)\to H^q(F_b;R)$. The formula in [F1] is $s_{\gamma }=K_c{H}^q(T_{\bar{\gamma }})K_b^{-1}\mathrm{.}$ Since $\overline{\gamma \ast \eta }=\bar{\eta }\ast \bar{\gamma }$, [F2]–[F3] give $T_{\overline{\gamma \ast \eta }}\simeq T_{\bar{\gamma }}{T}_{\bar{\eta }}$. Contravariance gives $H^q(T_{\overline{\gamma \ast \eta }})=H^q(T_{\bar{\eta }})H^q(T_{\bar{\gamma }})$. Cancelling $K_c{K}_c^{-1}$ now yields $s_{\gamma \ast \eta }=s_{\eta }{s}_{\gamma }$. Constants and endpoint-fixed homotopies are handled identically, so [F4] gives the cohomology local system.

If a component has empty fibers, all its stalks and maps are zero; a point fiber, the zero ring, and $q=0$ obey the same conjugation formulas. Reversal interchanges the two endpoints exactly as typed in step 1.2, and reversing twice returns the original class. The homology proof uses supplied maps and finite algebra only. The cohomology proof uses AC precisely through [F5] and does not spend it again. These checks establish every claimed functor law.