feat(library/hott): multiple changes in the HoTT library

I do not plan to make any changes to the library next couple of days, so Jakob can move the HoTT library.

---
commit message:

Jakob accidentally undid some of my changes. Revert that;
make style changes in multiple files;
in types/sigma: finish porting Coq-HoTT, and finish unfinished proof;
in axioms/funext: rename path_forall, make some arguments implicit and make instance visible