A map i:A→X of spaces has the homotopy extension property for a space Y if
- for each homotopy H:A×I→Y
- and for each map f:X→Y with f(i(a))=H(a,0) for all a∈A
there is a homotopy H′:X×I→Y such that
H′(i(a),t)H′(x,0)==H(a,t)f(x)
for all a∈A, x∈X and t∈I. The idea can be expressed in the following commutative diagram:
The homotopy H′ is called the extension of H with initial condition f.