Definition 1.1.16.  Let U be a set, S, T ⊆ U. We define:
S ∪ T:= {x ∈ U : x ∈ S or x ∈ T}

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.