Zulip Chat Archive

Stream: general

Topic: Possible incorrect explanation in Theorem Proving in Lean

Donald Sebastian Leung (Feb 23 2020 at 09:01):

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 (Feb 23 2020 at 09:40):

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 (Feb 23 2020 at 09:51):

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 (Feb 23 2020 at 09:54):

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

Rob Lewis (Feb 23 2020 at 10:12):

@Jeremy Avigad TPIL bug report :)

Jeremy Avigad (Feb 24 2020 at 00:48):

Thanks! I have fixed it.

Last updated: Aug 03 2023 at 10:10 UTC