So we have the fundamental group $\pi_1 (X, x_0)$ with loops $f:I\rightarrow X $ and $e$ the constant loop. I’m trying to construct a homotopy between the concatenation $f •e $ and $f$.
I’m told and have verified that the homotopy $$F(s,t)= x_0 , 2s\leq t \text{ or } 2s-1\geq t $$ $$F(s,t)=f(2s-t) \text{ o/w } $$ works.
But I want to know how to come up with this because other parts of the proof that $(\pi _1(X,x_0 ), •)$ is a group depends on constructing homotopies.
[Here $I=[0,1] $].