In Coq we have an impredicative base type, called Prop, and a predicative base type, called Set, both of type Type 0.

On the other hand, in Lean we only have an impredicative base type. We do not have an equivalent to Set. Instead we use directly Type 0(a synonym of Sort 1).

What are the implications of this design decision?

  • 2
    $\begingroup$ I think this almost answers it. Would you agree? $\endgroup$ – chi Jul 12 '18 at 22:43
  • $\begingroup$ @chi Nice reference, but, in my limited understanding, I do not think this answers the question. I understand what is the purpose of Prop. The real question is what power adds to the system the introduction of Set (as in Coq) while using Type 0 directly (as in Lean) is sufficient. Maybe it has some relation with Coq having cumulative universes while Lean having not. $\endgroup$ – user3368561 Jul 13 '18 at 0:54
  • $\begingroup$ I would agree. I think the main reason of having Prop is just predicativity. What other reasons do you think there might be? $\endgroup$ – xuq01 Jul 13 '18 at 3:27
  • $\begingroup$ @xuq01 Both of you are right, but this question is not about Prop but about the presence/absence of Set. What are the advantages of having it (Coq) when you can live without it (Lean)? It increases the complexity of the system (this is a big thing for a theorem prover) so there must be a reason. $\endgroup$ – user3368561 Jul 13 '18 at 9:15
  • 1
    $\begingroup$ The linked answer still answers it. Set is predicative, so it has large elimination; Prop is impredicative, so it does not have large elimination. $\endgroup$ – xuq01 Jul 13 '18 at 9:34

In Coq Set behaves basically like the smallest possible Type. Unlike Coq however, Lean lets you select the "level" of the type manually, such as Type 9 (or Sort 10), something which is not allowed in Coq - meaning that you do not need Set in Lean, you can just use Type 0 (or just Type, or Sort 1) instead as it is basically the same thing. I should also note that in Lean Prop is the same as Sort 0 (or Sort) (which does not have large elimination) and Type n (for n : nat) is the same as Sort (n + 1) (which has large elimination).

TL;DR: Type (with no "arguments") is the Set of Lean

  • $\begingroup$ But in Coq Prop and Set are of the same type while in Lean they are not; in Lean one of them is in fact an element of the other. Does this have any significance to the logic theory behind? $\endgroup$ – user3368561 Sep 30 '18 at 22:08
  • 2
    $\begingroup$ @user3368561 As far as I know the only significance is that only Prop can be impredicative in Lean while in Coq both Prop and Set can be impredicative (as long as you stay in the bounds of intuitionistic type theory) - as only the lowest member(s) of the hierarchy can be impredicative if you do not want paradoxes. $\endgroup$ – Generic Anime Girl Oct 1 '18 at 13:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.