Possible incorrect explanation in Theorem Proving in Lean

Stream: general

[Donald Sebastian Leung]

In Chapter 9.1 of Theorem Proving in Lean, it says:

Recall that in Lean, Type 0 is Prop, which is impredicative and proof irrelevant.

But at least in Lean v3.5.c, Prop is Sort 0 and Type = Type 0 = Sort 1. I suppose this is unintentional?

[Kevin Buzzard]

That certainly looks like an error to me.

pprod : Sort u_1 → Sort u_2 → Sort (max 1 u_1 u_2)

Note "Sort" not "Type".

[Gabriel Ebner]

Once upon a time, Prop was Type 0 and Type u was just Type u; there was no Sort u. Then early in Lean 3, we changed this to improve universe level inference. Now Type u is Sort (u+1) and Prop is Sort 0.

[Donald Sebastian Leung]

Thanks @Gabriel Ebner for providing the historical background, I suspected that that might have been the case.

[Rob Lewis]

@Jeremy Avigad TPIL bug report :)

[Jeremy Avigad]

Thanks! I have fixed it.