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 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 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 [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 are cumulative, 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 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 collection of types varying over a given type $A$, we use functions $B:A\to 𝒰$ 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 $\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 family at 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)).

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