Syntax sugar for nested Sigma types

[fizruk]

It is possible to generalise Σ to accept arbitrary parameters like in #define:

Σ (a : A), ∑ (b : B), C a b       -- current syntax (right assoc)
Σ ((a, b) : ∑ (a : A), B), C a b  -- current syntax (left assoc)
Σ (a : A) (b : B), C a b          -- generalised syntax (should be desugared to left assoc)

Originally posted by @fizruk in emilyriehl/yoneda#14 (comment)

Correspondingly, there should be syntax sugar for pair patterns:

\ (a, (b, c)) -> ...        -- explicit patterns (right assoc)
\ ((a, b), c) -> ...        -- explicit patterns (left assoc)
\ (a, b, c) -> ...          -- explicit patterns (should be desugared to left assoc)

This should be a simple change.

[TashiWalde]

Ideally it should be possible to fully specify the mixed associativity of a Σ-type with only a single Σ symbol.
For example I would like to be able to write any of the following if I care about the exact bracketting of my terms.

Σ (a : A , (b : B a , c : C a b)) , (d : D a b c)
Σ (a : A , b : B a) , (c : C a b , d : D a b c)

And I would probably prefer one of the following for the unbiased version (which then secretly desugars to left assoc).

Σ (a : A , b : B a , C a b)
Σ (a : A) (b : B a) (C a b)

It just seems a bit asymmetric to have one but not all commas.

One additional alternative which I also quite like is to use the × as an infix operator for dependent sums. For example:

(a : A) × B × (c : C a) × (D a c)