Fibration sequence is natural

If $e\in F$, then $p^{\mathrm{\prime }}u(e)=vp(e)=v(b_0)=b_0^{\mathrm{\prime }}$, so restriction defines the continuous based $u_F$. The identities $ui=i^{\mathrm{\prime }}{u}_F$ and $p^{\mathrm{\prime }}u=vp$ imply commutation of the inclusion and projection squares in all degrees by F3, including maps of component sets.

For a based cube $b$ in $B$ choose a lift $a$ constant at $e_0$ on its $J$ faces. Then $ua$ lifts $vb$ and is constant at $e_0^{\mathrm{\prime }}$ on those faces. On the distinguished face its restriction is $u_F$ composed with the restriction of $a$. F2 therefore gives ${\mathrm{\partial }}_{p^{\mathrm{\prime }}}{v}_{\ast }[b]=u_{F\ast }{\mathrm{\partial }}_p[b]$. In degree one this is equality of the components of the initial endpoints, so the same calculation covers that square.

If $a$ lifts a loop $\gamma$ beginning at $e\in F$, then $ua$ lifts $v\gamma$ beginning at $u_F(e)$ and ends at $u_F(a(1))$. The independence of component lifts in F1 therefore gives the action identity on every component, without selecting a compatible family of lifting functions.

Steps 1.1–1.3 establish all arrows and the action. Basepoints exclude empty based fibers but no connectedness or surjectivity is needed; components not meeting the image of $u_F$ cause no change in the formulas. For point spaces and constant cubes the equations remain identities; degree zero stays a pointed-set assertion. Every choice above is one representative or lift for one equality, hence no AC.