Refactor large posets etc. to refer to cumulative large sets #1849
Description
Large meet and join semilattices in particular want to be cumulative large sets (so finite collections at any universe level have an appropriate meet/join).
{{ message }}
Large meet and join semilattices in particular want to be cumulative large sets (so finite collections at any universe level have an appropriate meet/join).