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
array a of type A as
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 n is the cardinality of A.
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 int
The proof of such a proposition in Nuprl
will include a procedure which,
given
a function f from the interval 
to the interval
with m > n, produces the values i and j for which
. The constructive proof is considerably harder than the
(trivial) proof of the classically interpreted pigeon--hole principle, but the
information contained in the constructive proof is correspondingly much
greater.