Subsets of the integers of the form are especially useful.
We call them * intervals,* and they are defined as follows.
First we define the symbol ` <=` to mean ``less than or equal to'' with
the following definition:

<x:int>\<=<y:int>==((<y><<x>)->void)}.Now the concept of interval can be defined by

{<n:int>,...,<m:int>}=={x:int| <n><=x # x<=<m>}.Using intervals we can define the concept of an

a:{1,...,n}->A.

A very important concept in set theory is the concept of
* equal cardinality*. We shall use the
term * equipollent* to signify the type--theoretic
analogue of equal cardinality. As in classical set theory,
two types are equipollent if there are a pair of invertible
functions between them. This is captured by the following definition.

<A:type> is equipollent with <B:type>== (some ab:<A>-><B>.some ba:<B>-><A>.all x:<A>.all y:<B>. ba(ab(x))=x in <A> & ab(ba(y))=y in <B>)In the constructive account, however, we must exhibit the two functions that establish equipollence, so it is not permissible to use the Schroeder--Bernstein theorem, for example, to establish equipollence. Thus equipollence is not identical to the classical notion of equal cardinality.

The following three Nuprl theorems express basic facts about equipollence.

>>all A:U1. A is equipollent with A >>all A:U1.all B:U1. A is equipollent with B => B is equipollent with A >>all A:U1.all B:U1.all C:U1. A is equipollent with B & B is equipollent with C => A is equipollent with C

Using the notions of intervals and equipollence we can define the concept of a
* finite type*.
We say that a type **A** is finite if and only if
it is equipollent
with some interval.

<A:type> is finite== some n:int.{1,...,n} is equipollent with <A>We say that

A nontrivial statement that can be made with the definitions introduced in this section is the pigeonhole principle. The following Nuprl theorem expresses the principle.

>>all n:int.all m:int. all f:{1,...,m}->{1,...,n}. 0<n<m => some i,j:int.i<j & f(i)=f(j) in intThe proof of such a proposition in Nuprl will include a procedure which, given a function

Thu Sep 14 08:45:18 EDT 1995