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{\u0e50\x9d\x92\u0e10}}_{\mathrm{\u0e42\x88\x9e}}$ including itself (that is, with ${\mathrm{\u0e50\x9d\x92\u0e10}}_{\mathrm{\u0e42\x88\x9e}}:{\mathrm{\u0e50\x9d\x92\u0e10}}_{\mathrm{\u0e42\x88\x9e}}$). 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
$${\mathrm{\u0e50\x9d\x92\u0e10}}_{0}:{\mathrm{\u0e50\x9d\x92\u0e10}}_{1}:{\mathrm{\u0e50\x9d\x92\u0e10}}_{2}:\mathrm{\u0e42\x8b\u0e0f}$$ |
where every universe ${\mathrm{\u0e50\x9d\x92\u0e10}}_{i}$ is an element of the next universe ${\mathrm{\u0e50\x9d\x92\u0e10}}_{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:{\mathrm{\u0e50\x9d\x92\u0e10}}_{i}$ then also $A:{\mathrm{\u0e50\x9d\x92\u0e10}}_{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 ${\mathrm{\u0e50\x9d\x92\u0e10}}_{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:\mathrm{\u0e50\x9d\x92\u0e10}$ omitting the level. This way we can even write $\mathrm{\u0e50\x9d\x92\u0e10}:\mathrm{\u0e50\x9d\x92\u0e10}$, which can be read as ${\mathrm{\u0e50\x9d\x92\u0e10}}_{i}:{\mathrm{\u0e50\x9d\x92\u0e10}}_{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 $\mathrm{\u0e50\x9d\x92\u0e10}$ is assumed, we may refer to types belonging to $\mathrm{\u0e50\x9d\x92\u0e10}$ as small types.
To model a collection^{} of types varying over a given type $A$, we use functions^{} $B:A\u0e42\x86\x92\mathrm{\u0e50\x9d\x92\u0e10}$ 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{\u0e50\x9d\x96\u0e05\u0e50\x9d\x97\x82\u0e50\x9d\x97\x87}:\mathrm{\u0e42\x84\x95}\u0e42\x86\x92\mathrm{\u0e50\x9d\x92\u0e10}$, where $\mathrm{\u0e50\x9d\x96\u0e05\u0e50\x9d\x97\x82\u0e50\x9d\x97\x87}\u0e42\x81\u0e02(n)$ is a type with exactly $n$ elements. (We cannot define the family $\mathrm{\u0e50\x9d\x96\u0e05\u0e50\x9d\x97\x82\u0e50\x9d\x97\x87}$ yet โ indeed, we have not even introduced its domain $\mathrm{\u0e42\x84\x95}$ yet โ but we will be able to soon; see \autorefex:fin.) We may denote the elements of $\mathrm{\u0e50\x9d\x96\u0e05\u0e50\x9d\x97\x82\u0e50\x9d\x97\x87}\u0e42\x81\u0e02(n)$ by ${0}_{n},{1}_{n},\mathrm{\u0e42\x80\u0e06},{(n-1)}_{n}$, with subscripts to emphasize that the elements of $\mathrm{\u0e50\x9d\x96\u0e05\u0e50\x9d\x97\x82\u0e50\x9d\x97\x87}\u0e42\x81\u0e02(n)$ are different from those of $\mathrm{\u0e50\x9d\x96\u0e05\u0e50\x9d\x97\x82\u0e50\x9d\x97\x87}\u0e42\x81\u0e02(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:\mathrm{\u0e50\x9d\x92\u0e10}$, which is of course the constant function^{} $(\mathrm{\u0e2e\u0e1b}(x:A).B):A\u0e42\x86\x92\mathrm{\u0e50\x9d\x92\u0e10}$.
As a non-example, in our version of type theory^{} there is no type family โ$\mathrm{\u0e2e\u0e1b}(i:\mathrm{\u0e42\x84\x95}).{\mathrm{\u0e50\x9d\x92\u0e10}}_{i}$โ. Indeed, there is no universe large enough to be its codomain. Moreover, we do not even identify the indices $i$ of the universes ${\mathrm{\u0e50\x9d\x92\u0e10}}_{i}$ with the natural numbers $\mathrm{\u0e42\x84\x95}$ of type theory (the latter to be introduced in ยง1.9 (http://planetmath.org/19thenaturalnumbers)).
References
- 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 |