What are Prop and Type?

Stream: new members

[Leo Ericson]

I don't have much formal mathematical background so I would appreciate an explanation that is geared more towards computer science.

The context for this question is that I'm trying to understand what differentiates a inductive predicate inductive foo : ... -> Prop and an inductive type inductive bar : ... -> Type. I understand how to use them, but struggle to see how they work.

I also saw somewhere that Prop is Sort 0 and Type is Sort 1. What does this mean?

I would appreciate any resources for further reading on this topic.

[Julian Berman]

Hello.

(Fellow new member, so hopefully I don't get this wrong myself --) maybe this helps: Prop is a type, it's the type of propositional statements -- e.g. 2 = 2 or 8 is even -- and also of the type 2 = 8, which is also a proposition (even though it's a false one). The numbers you see in Sort, which I'll come back to in a sec, are universes -- there is an (infinite) hierarchy of types that live in successive universes, and essentially some rules that say you can't refer to types in higher universes from lower ones to prevent things like Russell's paradox. The universe at 0 is, in Lean, just a universe that Prop lives in -- and there's some further rules that let Prop refer to types in higher universes -- i.e. to allow one to state propositions about types no matter what universe they live in.

Sort is a word that just refers to both Prop and all the higher universe types, because well, Type is taken -- so Prop and Type <somenumber> are syntax sugar for Sort essentially.

There's some info in https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html and the preceding chapter on dependent type theory and how Lean calls things from it, and https://www.youtube.com/watch?v=3sKrSNhSxik from @Mario Carneiro has some explanation as well if you prefer videos.

[Leo Ericson]

There's some info in https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html and the preceding chapter on dependent type theory and how Lean calls things from it

Thanks! I must have missed that when I skimmed the TOC before. I had read the Hitchhiker's guide and thought it was largely similar content. This looks to be what I need so I'll be off reading.