(s, t) = (s', t') :⇔ s = s' and t = t'(s ∈ S, t ∈ T, s' ∈ S, t' ∈ T)
For S' ⊆ S and T' ⊆ T, we canonically treat elements of S' × T' as elements of S × T.
Remarks.
The Cartesian product is, again, a "construction." Note that HLM does not have any built-in notion of "tuple" – it is actually defined here as a constructor, with the usual notation.