type of `not`

Stream: new members

[Scott Olson]

Is there a reason we have def not : Prop → Prop rather than def not : Sort u → Prop?

I had some proofs of ¬foo which I had to change to foo → false when I changed foo from a simple ∃ Prop to a structure sigma Type, but it seems like it would make sense to still say ¬foo.

[Simon Hudon]

It's probably a matter of convention. ¬p, you usually assume that p is a proposition . An operation such as you describe might more usefully be called is_empty

[Mario Carneiro]

there used to be a ~A notation for this, but it didn't get used enough to be worth it.