Not, false and empty.

Stream: new members

[Pedro Minicz]

Why not has type Prop → Prop and not Sort* → Prop? I believe inferring the universe level should be doable is almost every case.

[Jalex Stark]

does not : Sort* \to Prop have useful lemmas?

[Jalex Stark]

i guess Q \imp P \imp (\not P \imp \not Q) works for this sort of not

[Jalex Stark]

but where would you use it?

[Pedro Minicz]

Say I have an uncountable type α, i.e. there isn't a bijection between α and the naturals, then I could express that by ¬denumerable α.

[Pedro Minicz]

¬ nonempty (encodable ℝ)

[Pedro Minicz]

How does the universe hierarchy work in Lean?

[Johan Commelin]

@Pedro Minicz Not sure what you mean, but you have Type u := Sort (u+1), and for universe levels, you basically have a succ function, and max.

[Reid Barton]

And it's noncumulative, so each (fully elaborated) type belongs to just one universe

[Pedro Minicz]

I see. Sort 0 is an impredicative universe, right?

[Johan Commelin]

I think it is (-;