Also see Binary Disjoint Union for newer supplementary material.

next up previous contents index
Next: Integers Up: Extending the Typed Previous: Dependent Products

Disjoint Union

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 .

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995