1.3 Universes and Families
So far, we have been using the expression “ is a type” informally. We are going to make this more precise by introducing universes. 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 theory, this is unsound, i.e. we can deduce from it that every type, including the empty type representing the proposition 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 paradox .
To avoid the paradox we introduce a hierarchy of universes
where every universe is an element of the next universe . Moreover, we assume that our universes are cumulative, that is that all the elements of the universe are also elements of the universe, i.e. if then also . 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 is a type, we mean that it inhabits some universe . We usually want to avoid mentioning the level explicitly, and just assume that levels can be assigned in a consistent way; thus we may write omitting the level. This way we can even write , which can be read as , 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 collection of types varying over a given type , we use functions 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 sets , where is a type with exactly 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 by , with subscripts to emphasize that the elements of are different from those of if is different from , and all are different from the ordinary natural numbers (which we will introduce in §1.9 (http://planetmath.org/19thenaturalnumbers)).
As a non-example, in our version of type theory there is no type family “”. Indeed, there is no universe large enough to be its codomain. Moreover, we do not even identify the indices of the universes 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