Add syntax sugar for nested sigma-types

[geffk2]

Closes #140.
Implemented syntax sugar allowing Sigma-types to accept more than one parameter in the parentheses with Rzk.TypeSigmaNested.
It will always desugar to left-associativity, i.e:

• Σ (a : A , b : B) , C a b desugars to Σ ( ( a , b) : Σ (a : A) , B) , C a b
• Σ ( a : A , b : B , c : C) , D a b c desugars roughly to Σ ((x , c) : Σ ((a , b) : Σ (a : A) , B) , C) , D (first x) (second x) c

[geffk2]

The sigma type part seems to work, tested with the following:

#lang rzk-1

#define test1
  ( A B : U)
  ( C : A → B → U)
  : ( Σ ( ( a , b) : Σ (a : A) , B) , C a b) = (Σ (a : A , b : B) , C a b)
  := refl

#define test2
  ( A B C : U)
  ( D : A → B → C → U)
  : ( Σ ( a : A , b : B , c : C) , D a b c) = (Σ ((x , c) : Σ ((a , b) : Σ (a : A) , B) , C) , D (first x) (second x) c)
  := refl

Not sure how to proceed with patterns, as adding syntax rules would either break existing stuff or warrant changes to semantic highlighting(I might be misunderstanding how it works).

[geffk2]

What are we calling those by the way? Not sure if "nested sigma types" is quite correct

[fizruk]

Ideally, I would like to reuse Param, but I think this should be a separate change, since Param allows shapes and we do not support shape types yet (see #50).

[fizruk]

What are we calling those by the way? Not sure if "nested sigma types" is quite correct

Perhaps, Σ-tuples?

[fizruk]

Not sure how to proceed with patterns

Here's a sketch: d8302a5