Paths and cylinders
In classical homotopy theory, a homotopy lifting property is a condition satisfied by continuous maps between topological spaces. More generally, such a condition may appear in more general context of a category with products and with an interval object :
The Eckmann–Hilton dual of the homotopy lifting property is the homotopy extension property.
Let be a category with products and with interval object .
A morphism has the homotopy lifting property if it has the right lifting property with respect to all morphisms of the form .
This means that for all commuting squares
there exists a morphism such that both triangles in
For a generator this can be rephrased as saying that the universal morphism induced by the commuting square
is an epimorphism. If it is even an isomorphism then the lift exists uniquely .
The homotopy lifting property is an instance of a right lifting property.
For topological spaces
Here the ambient category if Top and the interval object is .
A continuous map of topological spaces satisfies the homotopy lifting property (or covering homotopy property) with respect to a space if for every commuting square in
there is a diagonal such that the entire diagram commutes. The map is given by for .
A map is a Hurewicz fibration if it satisfies the homotopy lifting property with respect to all spaces . A map is a Serre fibration if it satisfies the homotopy lifting property with respect to all disks (equivalently, all topological cubes).
There are weaker notions than the usual homotopy lifting property. For example, in the notion of Dold fibration one requires in the above diagram that the lower triangle is commutative while the upper one is commutative only up to a homotopy. Alternatively, one can characterize the Dold fibrations by the delayed homotopy lifting property, where instead the notion of delayed homotopy is used, but the lift makes the division of the square strictly commutative.
For metric spaces
For metric spaces, there is also a weaker notion, the approximate homotopy lifting property.
Morphism between quasi-categories that are left fibrations of quasi-categories satisfy the homotopy lifting property with respect to
For smooth bundles