Homotopy between composites associated in different ways
and are homotopic loops, i.e., they are in the same homotopy class of loops based at .
This version is essentially the associativity part of showing that the Fundamental group (?) of a based topological space is indeed a group.
We first note the explicit piecewise definitions of and :
If we denote the homotopy by , we want and . This homotopy is explicitly given by:
This version is a little stronger than the other versions. Let be the loop space of , i.e., the space of all loops in based at under the compact-open topology. Then, consider the following two maps: