+-- {: .rightHandSide} +-- {: .toc .clickDown tabindex="0"} ### Context #### Foundations +-- {: .hide} [[!include foundations - contents]] =-- =-- =-- \tableofcontents ## Overview There are various ways to deal with size issues in the [[foundations]] of [[mathematics]]. All of them involve the notion of [[universe]] in one way or another. * In [[set theory]], one usually either uses [[Grothendieck universes]], or some internal model of [[set theory]] or [[class theory]], whether [[well-pointed category|well-pointed]] [[Heyting categories]], [[well-pointed category|well-pointed]] [[division allegories]], [[sets]] with [[extensional relation|extensional]] [[well-founded relation|well-founded]] [[transitive relation|transitive]] relations, [[categories with class structure]], et cetera. * In [[class theory]], the notion of universe is already in the theory via the [[universal class]], which is by definition a [[class]] [[universe]]. * In [[dependent type theory]], one uses [[univalent universe|univalent]] [[Russell universes]] or [[Tarski universes]], which are basically internal models of [[dependent type theory]]. In any case, given a universe $U$, we say that a [[collection]] is **$U$-small** if it is in $U$, a [[collection]] is **$U$-large** if it is not in $U$, any subcollection of $U$ is a **class**, and a subcollection of $U$ is a **proper class** if it is not a [[singleton]] subcollection of $U$. ## See also * [[set]], [[proper class]], [[Grothendieck universe]] * [[small category]], [[essentially small category]], [[large category]] * [[Set]], [[Cat]], [[michaelshulman:category of all sets]] * [[small presheaf]], [[accessible category]], [[presentable category]] * [[resizing axiom]] [[!redirects size]] [[!redirects size issue]] [[!redirects size issues]]