Refactor around cumulative large sets #1847
Description
Possibly even most universe-polymorphic types in unimath -- certainly those that are sets at a universe level -- could probably use some amount of refactoring to the cumulative large set abstraction.