feat(library/hott) port a good portion of FunextVarieties.v