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 X {\displaystyle X\,\!} be a topological space, and let A ⊂ X {\displaystyle A\subset X} . We say that the pair ( X , A ) {\displaystyle (X,A)\,\!} has the homotopy extension property if, given a homotopy f ∙ : A → Y I {\displaystyle f_{\bullet }\colon A\rightarrow Y^{I}} and a map f ~ 0 : X → Y {\displaystyle {\tilde {f}}_{0}\colon X\rightarrow Y} such that f ~ 0 ∘ ι = f ~ 0 | A = f 0 = π 0 ∘ f ∙ , {\displaystyle {\tilde {f}}_{0}\circ \iota =\left.{\tilde {f}}_{0}\right|_{A}=f_{0}=\pi _{0}\circ f_{\bullet },} then there exists an extension of f ∙ {\displaystyle f_{\bullet }} to a homotopy f ~ ∙ : X → Y I {\displaystyle {\tilde {f}}_{\bullet }\colon X\rightarrow Y^{I}} such that f ~ ∙ ∘ ι = f ~ ∙ | A = f ∙ {\displaystyle {\tilde {f}}_{\bullet }\circ \iota =\left.{\tilde {f}}_{\bullet }\right|_{A}=f_{\bullet }} . That is, the pair ( X , A ) {\displaystyle (X,A)\,\!} has the homotopy extension property if any map G : ( ( X × { 0 } ) ∪ ( A × I ) ) → Y {\displaystyle G\colon ((X\times \{0\})\cup (A\times I))\rightarrow Y} can be extended to a map G ′ : X × I → Y {\displaystyle G'\colon X\times I\rightarrow Y} (i.e. G {\displaystyle G\,\!} and G ′ {\displaystyle G'\,\!} agree on their common domain). If the pair has this property only for a certain codomain Y {\displaystyle Y\,\!} , we say that ( X , A ) {\displaystyle (X,A)\,\!} has the homotopy extension property with respect to Y {\displaystyle Y\,\!} .
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 f ~ ∙ {\displaystyle {\tilde {f}}_{\bullet }} which makes the diagram commute. By currying, note that homotopies expressed as maps f ~ ∙ : X → Y I {\displaystyle {\tilde {f}}_{\bullet }\colon X\to Y^{I}} are in natural bijection with expressions as maps f ~ ∙ : X × I → Y {\displaystyle {\tilde {f}}_{\bullet }\colon X\times I\to Y} . 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.
… excerpt ends here. Continue reading the full article.

