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
.