Homotopy lifting property

In mathematics, in particular in homotopy theory within algebraic topology, the homotopy lifting property (also known as an instance of the right lifting property or the covering homotopy axiom) is a technical condition on a continuous function from a topological space "E" to another one, "B". It is designed to support the picture of "E" "above" "B" by allowing a homotopy taking place in "B" to be moved "upstairs" to "E".
For example, a covering map has a property of "unique" local lifting of paths to a given sheet; the uniqueness is because the fibers of a covering map are discrete spaces. The homotopy lifting property will hold in many situations, such as the projection in a vector bundle, fiber bundle or fibration, where there need be no unique way of lifting.
Formal definition.
Assume from now on all maps are continuous functions from one topological space to another. Given a map formula_1, and a space formula_2, one says that formula_3 has the homotopy lifting property, or that formula_4 has the homotopy lifting property with respect to formula_5, if:
there exists a homotopy formula_10 lifting formula_11 (i.e., so that formula_12) which also satisfies formula_13.
The following diagram depicts this situation. 
The outer square (without the dotted arrow) commutes if and only if the hypotheses of the lifting property are true. A lifting formula_14 corresponds to a dotted arrow making the diagram commute. This diagram is dual to that of the homotopy extension property; this duality is loosely referred to as Eckmann–Hilton duality.
If the map formula_4 satisfies the homotopy lifting property with respect to "all" spaces "X", then formula_4 is called a fibration, or one sometimes simply says that "formula_4 has the homotopy lifting property".
Note that this is the definition of "fibration in the sense of Witold Hurewicz", which is more restrictive than "fibration in the sense of Jean-Pierre Serre", for which homotopy lifting only for formula_5 a CW complex is required.
Generalization: homotopy lifting extension property.
There is a common generalization of the homotopy lifting property and the homotopy extension property. Given a pair of spaces formula_19, for simplicity we denote formula_20. Given additionally a map formula_1, one says that "formula_22 has the homotopy lifting extension property " if:
there exists a homotopy formula_10 which covers formula_27 (i.e., such that formula_28) and extends formula_29 (i.e., such that formula_30).
The homotopy lifting property of formula_3 is obtained by taking formula_32, so that formula_33 above is simply formula_34.
The homotopy extension property of formula_35 is obtained by taking formula_36 to be a constant map, so that formula_36 is irrelevant in that every map to "E" is trivially the lift of a constant map to the image point of formula_36.