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.

Last revised on November 19, 2022 at 11:03:33. See the history of this page for a list of all contributions to it.