Homotopy between constant loop and composite of loop with inverse

Statement

Existential version

Suppose $x_{0}$ is a point in a topological space $X$. Suppose $f$ is a loop based at $x_{0}$, i.e., $f$ is a continuous map from the closed unit interval $[0,1]$ to $X$ such that $f(0)=f(1)=x_{0}$. Denote by $f^{-1}$ the loop defined as $f^{-1}(t)=f(1-t)$. Denote by $e$ the constant loop at the point $x_{0}$.

Denote by $*$ the composition of loops by concatenation. Then, the loops $f*f^{-1}$ and $f^{-1}*f$ are both homotopic to $e$.

Note that since $(f^{-1})^{-1}=f$, it suffices to show that $f*f^{-1}$ is homotopic to $e$.

This is the inverses part of the proof that the Fundamental group (?) of a based topological space is indeed a group.

Constructive/explicit version

We note that $f^{-1}(t)=f(1-t)$, so we have:

$\!(f*f^{-1})(t)=\lbrace {\begin{array}{rl}f(2t),&0\leq t<1/2\\f(2-2t),&1/2\leq t\leq 1\\\end{array}}$

The map $e$ to which we want to homotope this is:

$\!e(t)=x_{0},0\leq t\leq 1$

The homotopy is given by:

$\!F(t,s)=\lbrace {\begin{array}{rl}f(2t),&0\leq t\leq s/2\\f(s),&s/2<t<(2-s)/2\\f(2-2t),&(2-s)/2\leq t\leq 1\\\end{array}}$

Graphical version

Here is a pictorial description of the homotopy:

Uniform version

Suppose $(X,x_{0})$ is a based topological space. Let $L=\Omega (X,x_{0})$ be the loop space. Consider the following two maps from $L$ to itself:

$A:L\to L,\qquad A(f)=f*f^{-1}$

and:

$E:L\to L,\qquad E(f)=e$

Then, the maps $A$ and $E$ are homotopic maps.