Homotopy between loop and composite with constant loop

Statement

Existential version

Suppose $x_0$ is a point in a topological space $X$ and $f$ is a loop based at $x_0$, i.e., $f$ is a continuous map from $[0,1]$ to $X$ such that $f(0)=f(1)=x_0$. Suppose $e$ is the constant loop based at $x_0$, i.e., the loop that stays at $x_0$ throughout.

Denote by $*$ the composition of loops by concatenation. Then, $f$ is homotopic to the loops $e*f$ and $f*e$.

This statement is essentially the identity element part of the proof that the Fundamental group (?) of a based topological space is indeed a group.

Constructive/explicit version

For a loop $f$ based at $x_0$, the loop $e*f$ is given by:

$(e*f)(t)=\{\begin{array}{cc}{x}_0,& 0\le t\le 1/2\\ f(2t-1),& 1/2<t\le 1\\ \end{array}$

The homotopy between $f$ and $e*f$ is given by:

$F_{\ell }(t,s)=\{\begin{array}{cc}{x}_0,& 0\le t\le s/2\\ f((2t-s)/(2-s)),& s/2<t\le 1\\ \end{array}$

The loop $f*e$ is given by:

$(f*e)(t)=\{\begin{array}{cc}f(2t),& 0\le t\le 1/2\\ x_0,& 1/2<t\le 1\\ \end{array}$

The homotopy between $f$ and $f*e$ is given by:

Failed to parse (unknown function "\begin{array}"): {\displaystyle \! F_r(t,s) = \lbrace\begin{array}{rl} f(2t/(2 - s)), & 0 \le t \le (2 - s)/2 \\ x_0 , & (2 - s)/2 < t \le 1 }

Graphical version

Here is a pictorial description of the homotopy between $f$ and $e*f$:

Here is a pictorial description of the homotopy between $f$ and $f*e$: