Question on equivalent ways of describing homotopy extension property. I am following a lecture note in algebraic topology. There I came across a property which is known as Homotopy Extension Property or in short HEP. The definition is given as follows $:$
Definition $:$ Let $X$ be a topological space and let $A$ be a subspace of $X.$ Then the pair $(X,A)$ is said to satisfy HEP if for a given map $f_0 : X \longrightarrow Y$ and a homotopy $g_t : A \longrightarrow Y$ of $f_0 \big\rvert_A$ there is an extension $h_t : X  \longrightarrow Y$ such that $h_t \big\rvert_A = g_t,$ for all $t \in I$ and $h_0 = f_0.$
It has been stated as an easy fact without proof that a pair $(X,A)$ has the homotopy extension property if and only if $(X \times \{0\}) \cup (A \times I)$ is a retract of $X \times I.$
But I don't get the point. Suppose that the pair $(X,A)$ has the  homotopy extension property then how does it imply that $X \times I$ retracts to $(X \times \{0\}) \cup (A \times I)\ $? Also how do I go the other way round? Would anybody please help me in this regard?
Thanks for your time.
 A: For $A\subseteq X$ consider the map $f_0\colon X\ni x\longmapsto x\in X$ and the map $g_t\colon A\ni a\longmapsto a\in X$ for each $t\in I$. Note that $g_0=f_0\big|A$. So, if $(X,A)$ has homotopy extension property then we have a map $h_t\colon X\to X$  such that $h_0=f_0$ and $h_t\big|A=g_t$ for each $t\in I$. In other words, $h(x,0):=h_0(x)=f_0(x)=x$ for all $x\in X$ and $h(a,t):=h_t(a)=g_t(a)=a$ for all $(a,t)\in A\times I$. That is, $h\colon X\times I\to (X\times 0)\cup (A\times I)$ is our required retraction.
Conversely, let $r\colon X\times I\to (X\times 0)\cup (A\times I)$ be a retraction. Suppose, $Y$ is another topological space and we are given a map $f_0\colon X\to Y$ and a homotopy $g_t\colon A\to Y,\ t\in I$ such that $g_0(a)=f_0(a)$ for all $a\in A$. So, we have a well-defined map $\varphi\colon(X\times 0)\cup (A\times I)\to Y$ given by $$\varphi(z)=\begin{cases}f_0(x) &\text{ if }z=(x,0)\text{ for some }x\in X,\\ g(a,t) &\text{ if }z=(a,t)\text{ for some }(a,t)\in A\times I.\end{cases}$$ Note that $\varphi$ will be continuous if we assume $A\subseteq_\text{closed}X$. Then our required homotopy $h_t\colon X\to Y$ can be defined as $h_t(x):= \varphi\circ r(x,t)$ for $(x,t)\in X\times I$.

So, I have proved the equivalence under the assumption that $A$ is closed in $X$. But, this equivalence is still true without the closedness assumption, and the proof is quite long. For example, see $\text{Proposition A.18. on page 533}$ of Hatcher's Algebraic Topology.
