1.3 Universes and Families

So far, we have been using the expression “$A$ is a type” informally. Weare 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 ${𝒰}_{\mathrm{\infty }}$ including itself(that is, with ${𝒰}_{\mathrm{\infty }}:{𝒰}_{\mathrm{\infty }}$).However, as in settheory, 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 arepresentation of sets as trees, we can directly encode Russell’sparadox [1].

To avoid the paradox we introduce a hierarchy of universes

$${𝒰}_0:{𝒰}_1:{𝒰}_2:\mathrm{\cdots }$$

where every universe ${𝒰}_i$ is an element of the next universe${𝒰}_{i+1}$. Moreover, we assume that our universes arecumulative,that is that all the elements of the $i^{\mathrm{th}}$universe are also elements of the ${(i+1)}^{\mathrm{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 wemay write $A:𝒰$ omitting the level. This way we can even write$𝒰:𝒰$, which can be read as ${𝒰}_i:{𝒰}_{i+1}$, having left theindices implicit. Writing universes in this style is referred to astypical 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 $A$, we use functions $B:A\to 𝒰$ whosecodomain is a universe. These functions are calledfamilies of types (or sometimes dependent types);they correspond to families of sets as used inset theory.

An example of a type family is the family of finite sets $\mathrm{𝖥𝗂𝗇}:\mathbb{N}\to 𝒰$, where $\mathrm{𝖥𝗂𝗇}(n)$ is a type with exactly $n$ elements.(We cannot define the family $\mathrm{𝖥𝗂𝗇}$ yet — indeed, we have not even introduced its domain $\mathbb{N}$ yet — but we will be able to soon; see ex:fin.)We may denote the elements of $\mathrm{𝖥𝗂𝗇}(n)$ by $0_n,1_n,\mathrm{\dots },{(n-1)}_n$, with subscripts to emphasize that the elements of $\mathrm{𝖥𝗂𝗇}(n)$ are different from those of $\mathrm{𝖥𝗂𝗇}(m)$ if $n$ is different from $m$, and all are different from the ordinary natural numbers (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 familyat a type $B:𝒰$, which is of course the constant function $(\lambda (x:A).B):A\to 𝒰$.

As a non-example, in our version of type theory there is no type family “$\lambda (i:\mathbb{N}).{𝒰}_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 $\mathbb{N}$ of type theory (the latter to be introduced in §1.9 (http://planetmath.org/19thenaturalnumbers)).