feat(library/hott) add: if precompositions with f are equivalences, then f is
feat(library/hott) use class inference for IsEquiv
fix(library/hott/funext): compilation error