Homotopy between composites associated in different ways
Statement
Existential version
Suppose are loops based at a point in a topological space . We can consider two differently associated products of these three loops:
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.
Constructive/explicit version
We first note the explicit piecewise definitions of and :
and:
If we denote the homotopy by , we want and . This homotopy is explicitly given by:
Graphical version
Uniform version
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:
and:
Then, the maps and are homotopic maps. This is part of the proof that is a H-space, which is a homotopy variant of topological monoid.