Fiber and fiber homotopy equivalence

For a continuous $p:E\to B$ and $b\in B$, its fiber over $b$ is $F_b=p^{-1}(\{b\})$ with the subspace topology of Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace; in CGWH constructions take the kified subspace. The fiber may be empty.

Given $p:E\to B$ and $q:E^{\mathrm{\prime }}\to B$, a map over $B$ is a continuous $u:E\to E^{\mathrm{\prime }}$ with $qu=p$. A homotopy over $B$ between such maps is $H:E\times I\to E^{\mathrm{\prime }}$ satisfying $qH(e,t)=p(e)$ at every time. A fiber homotopy equivalence is a map $u$ over $B$ for which a map $v:E^{\mathrm{\prime }}\to E$ over $B$ exists with $vu\simeq {\mathrm{i}\mathrm{d}}_E$ and $uv\simeq {\mathrm{i}\mathrm{d}}_{E^{\mathrm{\prime }}}$ through homotopies over $B$. This strengthens Homotopy equivalences, homotopy inverses and spaces of the same homotopy type by fixing every base coordinate.

Restriction gives ordinary homotopy equivalences $F_b\simeq F_b^{\mathrm{\prime }}$. In particular an empty fiber cannot be fiber homotopy equivalent to a nonempty one. When $B$ is one point this is precisely ordinary homotopy equivalence; when $B$ is empty both total spaces are empty. Comparing fibers over two different points as spaces is not itself a map over the original base. These definitions require no AC.