Higher homotopy groups are functorial and based homotopy invariant

Postcomposition with f sends boundary-fixed homotopies to boundary-fixed homotopies, now with value $y_0$, by F2. Hence $f_{\ast }[a]$ is well-defined. Pointwise on both half-cubes, $f\circ (a\ast b)=(f\circ a)\ast (f\circ b)$, so F1 makes it a homomorphism. A path is similarly sent to a path, giving a well-defined map on components.

For based maps f,g one has $g\circ (f\circ a)=(g\circ f)\circ a$ and $\mathrm{i}\mathrm{d}\circ a=a$, proving functoriality. If $H:X\times I\to Y$ is a based homotopy, $H(a(u),t)$ is continuous by F2 and equals $y_0$ on the cube boundary for every t. Thus its two endpoints define the same class, giving $f_{\ast }=g_{\ast }$. The same formula on points gives equality on components.

If based maps f and h are inverse up to based homotopy, step 2.1 gives $h_{\ast }{f}_{\ast }=(hf{)}_{\ast }=\mathrm{i}\mathrm{d}$ and $f_{\ast }{h}_{\ast }=(fh{)}_{\ast }=\mathrm{i}\mathrm{d}$. Thus these are inverse homomorphisms for positive degrees and inverse pointed bijections in degree zero.