feat(library/hott) port the rest of Funext_Varieties.v