Zulip Chat Archive

Stream: lean4

Topic: Sort vs Type

Tchsurvives (Mar 15 2023 at 06:00):

Hi sorry I am new to leanprover but I can't seem to find much information on the difference between Sort vs Type. there is a discussion here https://github.com/leanprover/lean/issues/1341 but it flies over my head. Could anyone point me anywhere?

Marcus Rossel (Mar 15 2023 at 06:45):

Note that the linked discussion is 6 years old. In today's Lean:

  • Sort 0 = Prop
  • Sort (n + 1) = Type n

Notably Type 0 can also be referred to as just "Type".

James Gallicchio (Mar 15 2023 at 06:54):

https://leanprover.github.io/theorem_proving_in_lean4/title_page.html is a good general reference for lean4!

James Gallicchio (Mar 15 2023 at 06:55):

https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects would be relevant here

James Gallicchio (Mar 15 2023 at 07:03):

the linked issue is actually a fun read, cool to see how we got here

Last updated: Dec 20 2023 at 11:08 UTC