fix(library/hott) : Convert to new path notations

Convert definitions and proofs to new notations for inverse and cocatenation. Adapt to now right associative of concatenation.