A union operator represents another basic way of combining concepts. For example, if T represents the type of triangles, R the type of rectangles and C the type of circles, then we can say that an object is a triangle or a rectangle or a circle by saying that it belongs to the type T or R or C. In Nuprl this type is written T|R|C.
In general if A and B are types, then so is their
disjoint union, A|B.
Semantically, not only is the union disjoint, but given an
element of A|B, it must be possible to decide
which component it is in.
Accordingly, Nuprl
uses the
canonical forms 
and 
to
denote elements of the union; for 
is in A|B,
and for 
is in A|B.
To discriminate on disjuncts, Nuprl
uses
the form 
.
The interpretation is that if d denotes terms
of the form 
then
and if it denotes terms of the form
then
The variable u is bound in e and v is bound in f. It is noteworthy that the type A|B can be defined in terms of
and a two--element type such as
.
