The definition of sigma could draw attention to the use of forall

[michaelpj]

Currently it uses (x: a) instead of \forall (x:a). Phil says this is deliberate to avoid confusing people, but after discussion we thought that it is in fact interesting and worth drawing attention to... but it might need some additional explanation if we do that.

[wadler]

I'll need to think about this. Wen, please remind me if I don't get to this by the end of June.

[wenkokke]

Currently it uses (x: a) instead of \forall (x:a). Phil says this is deliberate to avoid confusing people, but after discussion we thought that it is in fact interesting and worth drawing attention to... but it might need some additional explanation if we do that.

Could you explain why it is interesting?

[michaelpj]

It's surprising! We're defining existentials in terms of universals, is that okay? And the definition looks different to versions of that that people might be familiar with e.g. \exists x . P (x) := \neg \forall x . \neg P (x) in FOL.