Homotopy fiber of a map

For a based continuous map $f:(X,x_0)\to (Y,y_0)$, its homotopy fiber is the fiber of $p_f:E_f\to Y$ over $y_0$: $\mathrm{hofib}(f)=\{(x,\gamma ):\gamma (0)=f(x),\gamma (1)=y_0\},$ with basepoint $(x_0,c_{y_0})$. Its topology is the iterated subspace topology of Mapping path space replacement of a map and Fiber and fiber homotopy equivalence, or the specified kified topology in CGWH. Basedness ensures the displayed basepoint belongs to it. Unlike a literal fiber, its points include a specified path from the image to the basepoint.

For a strictly commuting square of based maps $a:X\to X^{\mathrm{\prime }}$, $b:Y\to Y^{\mathrm{\prime }}$ with $bf=f^{\mathrm{\prime }}a$, the induced map is $(x,\gamma )\mapsto (a(x),b\circ \gamma )$. The endpoint equations hold since $b\gamma (0)=f^{\mathrm{\prime }}a(x)$ and $b\gamma (1)=y_0^{\mathrm{\prime }}$. Postcomposition on path spaces is continuous: the inverse image of the compact-open condition $\eta (K)\subseteq U$ is $\gamma (K)\subseteq b^{-1}U$; kification gives the CG version. Hence the indicated map is continuous and preserves basepoints. Identity and composite squares give the identity and composite formulas pointwise; no path choices are required.

The existence of a basepoint excludes empty $X$ and $Y$ here. When $X$ is one point, this construction is the based loop space of $Y$; when $Y$ is one point it is $X$. These are identities of the specified path-subspace constructions, not claims that arbitrary literal fibers already have the same homotopy type.