The symbol ⌜Σ⌝ is used for the dependent product or existential type constructor, which is a generalisation of a labelled
disjoint union.
It takes a set which must be a function and which is interpreted as an indexed collection of sets.
It returns a set of ordered pairs the first of which is some value (the index) in the domain of the function, and the second
is a value in the set which the function maps that index.
The function is interpreted as assigning to each element in the index set a "type", and the result is the labelled disjoint
union of all these types, the labels being the indexes.