Homotopy extension property

In mathematics, in the area of algebraic topology, the homotopy extension property indicates which homotopies defined on a subspace can be extended to a homotopy defined on a larger space. The homotopy extension property of cofibrations is dual to the homotopy lifting property that is used to define fibrations.
Definition.
Let formula_1 be a topological space, and let formula_2.
We say that the pair formula_3 has the homotopy extension property if, given a homotopy formula_4 and a map formula_5 such that formula_6, there exists an "extension" of formula_7 to a homotopy formula_8 such that
formula_9.
That is, the pair formula_3 has the homotopy extension property if any map
formula_11
can be extended to a map formula_12 (i.e. formula_13 and formula_14 agree on their common domain).
If the pair has this property only for a certain codomain formula_15, we say that formula_3 has the homotopy extension property with respect to formula_15.
Visualisation.
The homotopy extension property is depicted in the following diagram
If the above diagram (without the dashed map) commutes (this is equivalent to the conditions above), then pair (X,A) has the homotopy extension property if there exists a map formula_18 which makes the diagram commute. By currying, note that a map formula_19 is the same as a map formula_20.
Note that this diagram is dual to (opposite to) that of the homotopy lifting property; this duality is loosely referred to as Eckmann–Hilton duality.
Other.
If formula_28 has the homotopy extension property, then the simple inclusion map formula_29 is a cofibration.
In fact, if you consider any cofibration formula_30, then we have that formula_31 is homeomorphic to its image under formula_32. This implies that any cofibration can be treated as an inclusion map, and therefore it can be treated as having the homotopy extension property.