# Contents

## 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.