 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.