Also see Binary Disjoint Union for newer supplementary material.

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

Thu Sep 14 08:45:18 EDT 1995