Proof: A loop is null homotopic iff it can be extended to a function of the disk

Solution 1:

For the forward direction, there is a much more direct proof - mainly, a homotopy between a loop and a constant is a map from the disc already. It's in the spirit of your proof, but doesn't require the homotopy extension theorem.

So, let $f:S^1\rightarrow X$ and assume $f$ is null homotopoic. Let $F(x,t)$ be a homotopy between $f$ and a constant map with $F(x,1) = f$ and $F(x,0) = x_0$.

Here's the trick - think of $(x,t)$ coordinates as polar coordinates on the disc where $x$ corresponds to $\theta$ and $t$ corresponds to $r$. Alternatively, the space $S^1\times [0,1]/$~ where we identify $S^1\times\{0\}$ to a point is clearly homeomorphic to the disc, and it's easy to see that since $F(x,0) = x_0$ independent of the $x$ value, that $F$ descends to map on $S^1\times [0,1]/$~.