Definition 1.1.25.  Let S, T be sets. We define:
S ⊎ T :=: {l(s) | s ∈ Sr(t) | t ∈ T}
l(s) = l(s')  :⇔  s = s'  (s ∈ S, s' ∈ S)
r(t) = r(t')  :⇔  t = t'  (t ∈ T, t' ∈ T)
For S' ⊆ S and T' ⊆ T, we canonically treat elements of S' ⊎ T' as elements of S ⊎ T.
Remarks.

In contrast to the definition of set union, the disjoint union of sets is a "construction," which is an HLM-specific concept very similar to an inductive definition in type theory. The disjoint union has two "constructors."

Note that the set and its constructors are introduced at the same time, hence the non-standard notation ":=:". The notation on both sides can be specified freely.

A construction always includes definitions of equality for each constructor. In this case, those definitions are what one might expect. (Different constructors are never considered equal.)

References.