Homotopy lifting property

Remarks

Example: every covering map has the homotopy lifting property with respect to every space, and the lift is then unique. For $X$ a point this is the path lifting property: for $p \colon \R \to S^1$, $p(t) = e^{2\pi i t}$, the loop $H(t) = e^{2\pi i t}$ with starting point $0$ lifts to $\tilde H(t) = t$.

Non-example: let $E = \set{0, 1}$ with the discrete topology, $B = [0, 1]$ and $p$ the inclusion. For $X$ a point, $\tilde f = 0$ and $H(t) = t$, clauses 1 and 2 would force $\tilde H$ to be a path in $E$ from $0$ to $1$, but $E$ is not path-connected.

In diagram form: every commutative square with $X \to E$ on top, $X \times \set{0} \hookrightarrow X \times I$ on the left and $p$ on the right has a diagonal $X \times I \to E$ making both triangles commute. A map with this property for all spaces $X$ is a Hurewicz fibration; for all cubes $I^n$, a Serre fibration.