1.3 Universes and Families

So far, we have been using the expression โ€œA is a typeโ€ informally. We are going to make this more precise by introducing universesPlanetmathPlanetmath. A universe is a type whose elements are types. As in naive set theory, we might wish for a universe of all types ๐’ฐโˆž including itself (that is, with ๐’ฐโˆž:๐’ฐโˆž). However, as in set theoryMathworldPlanetmath, this is unsound, i.e.ย we can deduce from it that every type, including the empty type representing the propositionPlanetmathPlanetmathPlanetmath False (see ยง1.7 (http://planetmath.org/17coproducttypes)), is inhabited. For instance, using a representation of sets as trees, we can directly encode Russellโ€™s paradoxMathworldPlanetmath [1].

To avoid the paradox we introduce a hierarchy of universes


where every universe ๐’ฐi is an element of the next universe ๐’ฐi+1. Moreover, we assume that our universes are cumulative, that is that all the elements of the ith universe are also elements of the (i+1)st universe, i.e.ย if A:๐’ฐi then also A:๐’ฐi+1. This is convenient, but has the slightly unpleasant consequence that elements no longer have unique types, and is a bit tricky in other ways that need not concern us here; see the Notes.

When we say that A is a type, we mean that it inhabits some universe ๐’ฐi. We usually want to avoid mentioning the level i explicitly, and just assume that levels can be assigned in a consistent way; thus we may write A:๐’ฐ omitting the level. This way we can even write ๐’ฐ:๐’ฐ, which can be read as ๐’ฐi:๐’ฐi+1, having left the indices implicit. Writing universes in this style is referred to as typical ambiguity. It is convenient but a bit dangerous, since it allows us to write valid-looking proofs that reproduce the paradoxes of self-reference. If there is any doubt about whether an argument is correct, the way to check it is to try to assign levels consistently to all universes appearing in it. When some universe ๐’ฐ is assumed, we may refer to types belonging to ๐’ฐ as small types.

To model a collectionMathworldPlanetmath of types varying over a given type A, we use functionsMathworldPlanetmath B:Aโ†’๐’ฐ whose codomain is a universe. These functions are called families of types (or sometimes dependent types); they correspond to families of sets as used in set theory.

An example of a type family is the family of finite setsMathworldPlanetmath ๐–ฅ๐—‚๐—‡:โ„•โ†’๐’ฐ, where ๐–ฅ๐—‚๐—‡โข(n) is a type with exactly n elements. (We cannot define the family ๐–ฅ๐—‚๐—‡ yet โ€” indeed, we have not even introduced its domain โ„• yet โ€” but we will be able to soon; see \autorefex:fin.) We may denote the elements of ๐–ฅ๐—‚๐—‡โข(n) by 0n,1n,โ€ฆ,(n-1)n, with subscripts to emphasize that the elements of ๐–ฅ๐—‚๐—‡โข(n) are different from those of ๐–ฅ๐—‚๐—‡โข(m) if n is different from m, and all are different from the ordinary natural numbersMathworldPlanetmath (which we will introduce in ยง1.9 (http://planetmath.org/19thenaturalnumbers)).

A more trivial (but very important) example of a type family is the constant type family at a type B:๐’ฐ, which is of course the constant functionMathworldPlanetmath (ฮป(x:A).B):Aโ†’๐’ฐ.

As a non-example, in our version of type theoryPlanetmathPlanetmath there is no type family โ€œฮป(i:โ„•).๐’ฐiโ€. Indeed, there is no universe large enough to be its codomain. Moreover, we do not even identify the indices i of the universes ๐’ฐi with the natural numbers โ„• of type theory (the latter to be introduced in ยง1.9 (http://planetmath.org/19thenaturalnumbers)).


  • 1 Coquand,Thierry. The paradox of trees in type theory. BIT Numerical Mathematics, 32:10โ€“14 1992
Title 1.3 Universes and Families
Canonical name 13UniversesAndFamilies
Date of creation 2013-11-12 21:01:43
Last modified on 2013-11-12 21:01:43
Owner PMBookProject (1000683)
Last modified by rspuzio (6075)
Numerical id 11
Author PMBookProject (6075)
Entry type Definition
Classification msc 03B15