²There is an unfortunate clash of notation with dependent pair types, which of course are also written with a Σ. However, context usually disambiguates.