Homotopy between loop and composite with constant loop
Statement
Existential version
Suppose is a point in a topological space and is a loop based at , i.e., is a continuous map from to such that . Suppose is the constant loop based at , i.e., the loop that stays at throughout.
Denote by the composition of loops by concatenation. Then, is homotopic to the loops and .
Graphical version
Here is a pictorial description of the homotopy between and :
Here is a pictorial description of the homotopy between and :