Mapping-path fibration replacement (source code)

= Mapping-path fibration replacement
{title2=$E_f=\{(x,\gamma):\gamma(0)=f(x)\}$}

For a map $f:X\to B$, let $E_f$ consist of points of $X$ and paths starting at their images, with projection $p(x,\gamma)=\gamma(1)$. Appending segments of a base homotopy proves the <homotopy lifting property>, so $p$ is a <Serre fibration>. The constant-path inclusion $s:X\to E_f$ satisfies $ps=f$ and is a <homotopy equivalence>: forget the path for an inverse, and shorten paths to prove the homotopy. The homotopy need not preserve the endpoint in $B$, so the statement concerns an equivalence of total spaces over a commuting triangle, not a fibrewise inverse. The fibre over $b_0$ is the <homotopy fibre> of $f$.