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.
fix(library/hott) fix funext.lean to match equivalence notation
chore(library/hott): add Jakob to list of authors
chore(library/hott): add Jakob to list of authors