[Agda] : vs. ∶

[Wolfgang Jeltsch]

Hello,

I propose to not use ∶ in the special syntax for Σ. Sure, it is intended
to be similar to :. However, I think this similarity is precisely its
weakness. You cannot tell from looking at the code whether your code is
syntactically correct or not. Furthermore, there is a semantic problem.
The symbol ∶ is called RATIO, but Σ does not have anything to do with
ratios. I propose to use an alternative syntax, maybe the following:

    syntax Σ A (λ x → B) = Σ[ x ∈ A ] B

What do others think?

Best wishes,
Wolfgang