Paths and cylinders
A (continuous) map of topological spaces is said to satisfy the homotopy extension property (HEP) with respect to a space if for any map and a homotopy such that , a homotopy exists such that .
If we write
then this is expressed by means of the commutative diagram
Here we denote , so that . The map is sometimes said to be the initial condition of a homotopy extension problem. is the extension of the homotopy with given initial condition which itself extends .
Of course it is superfluous to write the arrow : if we erase it, the commutativity of the remaining square just surrounding its position is saying ; however it is conceptually nice to think of as extending some .
One can instead of the diagram above write a diagram involving adjoint maps. In other words, instead of any homotopy we use the exponential law to write where the correspondence is given by the formula . Then the homotopy lifting property is the existence of the diagonal map in the diagram:
where is the map of evaluation at zero . This is an instance of right lifting property with respect to maps .
A map is a Hurewicz cofibration if it satisfies the homotopy extension property with respect to all spaces.
If a map has the homotopy extension property with respect to a space , then for any map , the pushout has the homotopy extension property with respect to the space .
We would like to find to complete the commutative diagram
Consider the external square obtained by composing the horizontal arrows:
By the assumption on , there is a as in the diagram, such that both triangles commute, i.e. and .
If is satisfying the HEP with respect to then there is a diagonal in that external square which is some map . This map together with , by the universal property of pushout, determines a unique map such that and . We need to show only that as holds by the construction of as stated.
By the definition of and the commutativity of the original double square diagram, and . This is almost what we wanted except that we precompose the wanted identity with both maps into the pushout. Thus by the uniqueness part of the universal property of pushout it follows that .