The expression of concepts from set theory in Nuprl
is facilitated by the
availability of the set type constructor as one
of the primitive
constructors of the underlying Nuprl
logic.
The notation for this constructor is { x:A|B}.
Intuitively
the set type constructor first forms a dependent sum of the two
component types and then
discards the second member of each pair in the dependent sum.
The members of this type are those
members a of the type A such that 
is inhabited.
Recalling the propositions--as--types principle,
we may think of B as a
propositional function and 
as a proposition. The
proposition 
is true when the corresponding type is inhabited;
thus the notation { x:A|B} defines the type whose members are members a
of A that make the proposition 
true. This is essentially
what the classical set formation construct means.
The simplest statements about sets that one can make involve subsets of a specific type such as int. In Nuprl we may represent such sets as set types over int in the following fashion. Given a predicate P on the integers, the set corresponding to P is,
{x:int | P(x)}.
This set type denotes those elements of int which
satisfy P.
Two important aspects of this type are that its members are elements of
int and that the proof of 
for an element a of int is not
available in computations.
For example, to prove that 9 belongs to
{x:int | some y:int. ~(y=x in int) & x mod y=0 in int}
we must prove that some number, such as 3, satisfies the defining predicate,
but we do not keep this factor as part of the membership condition.
This means that from an assumption such as
y in {x:int | P(x)} we do not have access to the proof of 
.
This aspect of the subset constructor
comes out as a restriction on the way hypotheses can be used
in the set--elimination rule.