Definition 1.1.16. Let *U* be a set, *S*, *T* ⊆ *U*. We define:

Remarks.

Due to the type system of HLM, it is impossible to define the union of two arbitrary sets. Instead, both sets must be declared as subsets of a common superset `U`

, although the union is, of course, independent of `U`

. Since a suitable value for `U`

can always be inferred automatically, `U`

can be omitted from the notation.

References.