sort vs type

Stream: general

[Johan Commelin]

I realise that I don't actually quite understand what the distinction is between sort and type. Somehow I treat them as interchangeable, but of course that is not a very solid strategy. So, what exactly is a sort, and when should I use it?

[Reid Barton]

Basically, Sort* = Prop union Type*. Sort 0 = Prop, and Sort (u+1) = Type u.

[Johan Commelin]

Hmm, so that kind explains my thinking that I could equate Sort* and Type*. But it doesn't explain why we have these two notions that are almost the same. Lean seems to prefer to have only 1 concept when 1 suffices...

[Sean Leather]

@Johan Commelin Here's some of the design discussion.

[Johan Commelin]

Thanks!