nLab small set

Redirected from "small types".

Contents

 Idea

In some choices of foundations, one says small set in order to amplify that one really means a set and not a proper class. Strictly speaking, in this case one could just say “set”.

However, in other choices of foundations, such as Grothendieck universes, there exist both “small sets” (sets that belong to the universe) and “large sets” (sets that do not, such as the universe itself). In this case the adjective really is necessary. We also gain an intermediate notion of moderate set: a subset of the universe, which may be small or large. (Every small set is moderate, but not conversely; again, the universe itself is the standard counterexample.)

Since in many cases the choice of foundations is irrelevant, it makes sense to always say “small set” for emphasis even if one has in mind a foundation where all sets are small.

Similarly, a small family is a family indexed by a small set; the axiom of replacement (if it applies in the foundation in question) then says that the image of the family is also small.

We also have related notions of small ordinals, small categories, etc. In type theory, we also have a notion of small type.

 See also

Last revised on May 25, 2023 at 14:20:52. See the history of this page for a list of all contributions to it.