Prove that $\lambda$ is a homotopy equivalence. The  based mapping cylinder of $f$, written $Cyl f$, is the based pushout of the maps $f:X\to Y$ and $i_0:X\to X\wedge I_+$. We know that maps $f\wedge 1:X\wedge I_+\to Y\wedge I_+$ and $i_0: Y\to Y\wedge I_+$ exist and that $f\wedge1 \circ i_0=i_0\circ f$. This means there exists a base point preserving continuous map $\alpha:Cyl f\to Y\wedge I_+$ that makes the appropriate diagram commute. We call $f$ a based cofibration if $\alpha$ has a base point preserving continuous retract.
Let $f:X\to Y$ be a based cofibration. We call $X\wedge I$ the cone on $X$, where $I$ has basepoint $1$. The mapping cone $Cf$ is the pushout of the maps $f$ and $i_0:X\to X\wedge I$. We know that there exists a unique basepoint preserving continuous function $\lambda:Cf\to Y/f(X)$ induced by the  pushout. How would I prove that $\lambda$ is a homotopy equivalence? I was told that $f$ being a based cofibration was sufficient to prove this but I don't know how.
 A: Let $Z(f)$ be the ordinary mapping cylinder of $f$ which is defined as
$$Z(f) = (X \times I + Y) / \sim $$
where $(x,0) \sim f(x)$. Let $p : X \times I + Y \to Z(f)$ denote the quotient map.
The space $\text{Cyl} f$ is nothing else than the quotient $Z(f) / p(\{x_0\} \times I)$. The map $i_1 : X \to \text{Cyl} f, i_1(x) = [x,1]$, is an embedding.
This also shows that $Y \wedge I_+ = \text{Cyl} id_Y$ is the quotient $Y / (\{y_0\} \times I)$ and that $i_1 : Y \to Y \wedge I_+$ is an embedding.
The map $\alpha : \text{Cyl} f \to Y \wedge I_+$ is given by $\alpha([x,t]) = [f(x),t)]$ and $\alpha([y]) = [y]$.
$f$ is a based cofibration if there is a map $r : Y \wedge I_+ \to \text{Cyl} f$ such that $r \circ \alpha = id$. This implies that $\alpha$ is an embedding. Thus also $\alpha \circ i_1 = i_1 \circ f$ is an embedding. We conclude that $f$ is an embedding, i.e. identifies $X$ with $f(X) \subset Y$. The image of $\alpha$ is therefore $(Y \times \{0\} \cup f(X) \times I) / (\{y_0\} \times I)$ which must be retract of $Y / (\{y_0\} \times I)$. It is well-known that this implies that $f$ has the pointed homotopy extension property.
The previous section shows that it is no restriction to assume that $f$ is the inclusion of a subspace $X \hookrightarrow Y$. The mapping cone $Cf$ is the pushout of $f$ ands $j_0 : X \to CX$, where $CX = (X \times I)  / (X \times \{1\} \cup \{x_0\} \times I)$ is the reduced cone of $X$ which is pointed contractible. Thus $Cf = Y \cup CX$, where we identify $X$ with the base $j_0(X)$ of $CX$. The pushout construction has the property that if one the source maps has the pointed homotopy extension property, then so has the map on the opposite side of the pushout square. We conclude that $CX \hookrightarrow Y \cup CX$ has the pointed homotopy extension property.
It is a well-known fact that if $A \hookrightarrow B$ has the pointed homotopy extension property and $A$ is pointed contractible, then the quotient map $\pi : B \to B/A$ is a pointed homotopy equivalence. Thus
$$\pi : Y \cup CX \to  (Y \cup CX)/CX = Y/X $$
is a pointed homotopy equivalence.
