Definition 1.1.26.  Let S, T be sets. We define:
S × T:=: {(s, t) | s ∈ S, t ∈ T}
(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.

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.