nLab large set



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

Relation to classes

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

 See also

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