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 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 .