Mapping path factorization

Direct evaluation gives $p_f{j}_f=f$ and $r_f{j}_f={\mathrm{i}\mathrm{d}}_X$. The formula $D((x,\gamma ),t)=(x,s\mapsto \gamma ((1-t)s))$ is continuous by F3 applied to its adjoint. It remains in $E_f$ because its path starts at $f(x)$, begins at $(x,\gamma )$ and ends at $j_f{r}_f(x,\gamma )$. It fixes every constant path. Thus $j_f$ and $r_f$ are homotopy inverses, even with a strong deformation retraction onto $j_f(X)$.

For the given HLP problem define ${\eta }_{z,t}:I\to Y$ by ${\eta }_{z,t}(s)={\gamma }_z((1+t)s)$ if $(1+t)s\le 1$, and ${\eta }_{z,t}(s)=H(z,(1+t)s-1)$ if $(1+t)s\ge 1$. Both domains are closed and cover $Z\times I\times I$. At their intersection the values are ${\gamma }_z(1)=H(z,0)$, so F3–F4 prove the joint continuity of the adjoint. All arguments of $H$ lie in $[0,t]$. In particular no division by $t$ occurs at $t=0$.

Transpose step 1.2 and put $\tilde{H}(z,t)=(x(z),{\eta }_{z,t})$. The path begins at ${\gamma }_z(0)=f(x(z))$, so this lands continuously in $E_f$. At $t=0$ it is exactly $(x(z),{\gamma }_z)$, and $p_f\tilde{H}(z,t)={\eta }_{z,t}(1)=H(z,t)$, including $t=0$ by compatibility. Hence F2 holds for every parameter space, and the same adjoint formulas establish the CG version.

Empty $X$ makes all initial-map test domains empty. A one-point $X$ gives the usual based path space; a one-point $Y$ reduces the deformation to the identity of $X$. Both deformation endpoints and both path endpoints were checked above. Existence of a path in $E_f$ forces its final point into a component meeting $f(X)$, explaining the absence of a surjectivity claim. Every operation was a formula, not a path selection. Together steps 1.1 and 2.1 establish the factorization.