Well-defined loop concatenation
= Well-defined loop concatenation
Concatenating two based homotopies proves that loop concatenation depends only on based-homotopy classes. Endpoint-fixing reparametrizations provide associativity and the identity laws on classes.