nLab large set

Definition

Given a universe $U$, a $U$-large set is a set which is not a $U$-small set. $U$-large sets can be contrasted with $U$-small sets.

Relation to classes

Every proper class in set theory is a $U$-large set. However, in dependent type theory, only material proper classes are always $U$-large h-sets; structural proper classes in dependent type theory are h-groupoids if the universe $U$ is a univalent universe.

 See also

• universe, Grothendieck universe, well-pointed Heyting pretopos, well-pointed division allegory, Tarski universe, cumulative hierarchy

• class

• small set

• universe enlargement