feat(library/tactic): elaborate 'exact' tactic argument at tactic execution time
fix(library/general_notation): mark \tr as left associative
feat(library/hott): add adjointification and closure properties for equivalences

Port features from the Coq Hott library
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