Sort

Stream: new members

[Holly Liu]

for universe u, #check Sort u evaluates Sort u as having type Type u, however the documentation says types are really just Sorts, i.e. Prop abbreviates Sort 0, Type abbreviates Sort 1, and Type u abbreviates Sort (u+1). is the point of Sort just to have an umbrella set that includes both Prop and Type?

[Kevin Buzzard]

Yes :-)

[Kevin Buzzard]

An umbrella universe in fact

[Kevin Buzzard]

For example this means that you can do induction and recursion on the naturals with the same function nat.rec