Homotopy equivalence between $X/A$ and $X$? Consider the following definition:
Definition: Let $(X, A)$ be a topological pair. We say $A$ has the homotopy extension property with respect to a space $Y$ if given any continuous map $f:X\longrightarrow A$ then every homotopy $F:A\times I\longrightarrow Y$ such that $F(x, 0)=f(x)$ for all $x\in A$ extends to a homotopy $G:X\times I\longrightarrow Y$ such that $G(x, 0)=f(x)$ for all $x\in X$.
Using this I'd like to show:
Theorem. Let $(X, A)$ be a topological pair where $A$ is contractibe. If $A$ has the homotopy extension property then $q:X\longrightarrow X/A$ is a homotopy equivalence.
Can anyone help me showing this?
Remark: (i) A topological space $X$ is said to be contractible if $id_X$ is null-homotopic. 
(ii) I know this is proven in Hatcher, but I don't like his exposition and I didn't understand his proof.
 A: First, an inclusion $A \subset X$ has HEP when for any $Y$, any map from cylinder $X \times \{0\} \cup A \times [0, 1] \to Y$ extends to a map from the whole $X \times [0, 1] \to Y$ -- this is pretty obviously equivalent to your definition.
So, let $H: A \times [0, 1] \to A$ be a homotopy contracting $A$. Glue $H$ with identity to obtain a map $C: X \times \{0\} \cup A \times [0, 1] \to X$. Extend it via HEP to $\tilde{H}: X \times [0, 1] \to X$. Let $f: X \simeq X \times \{1\} \to X$ be the restriction of $\tilde{H}$ to the top part of cylinder. Since $f$ is constant on $A$, it induces a map $\tilde{f}: X/A \to X$.
Let $p: X \to X/A$ be the quotient map. We'll show that $\tilde{f}$ is homotopy inverse to $p$. 
The composition $\tilde{f}p: X \to X$ is precisely $f$, and $\tilde{H}$ gives a homotopy between $f$ and identity, so $\tilde{f}$ is left inverse to $p$.
Composing $\tilde{H}$ with $p$ gives us a homotopy $p \tilde{H}: X \times [0, 1] \to X/A$ between $pf$ and $p$. But, $p\tilde{H}$ is constant on $A \times [0,1]$ (because $\tilde{H}$ restricted to $A \times [0, 1]$ is by construction just $H$, a contraction of $A$). Thus, $p \tilde{H}$ induces a map $F: (X/A) \times [0, 1] \to X/A$, which is a homotopy between identity and $p \tilde{f}$.
A: I feel that this situation is best understood as a special case of a more general gluing theorem for homotopy equivalences, though of course the special case stated has a special argument.  For the record, I should state that this theorem was first stated and proved in my book "Elements of Modern Topology" McGraw Hill, 1968, and is now seen as a standard part of abstract homotopy theory. The original proof gives tighter control over the homotopies involved. 
