nLab large set

\tableofcontents

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.

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.