In Coq we have an impredicative base type, called
Prop, and a predicative base type, called
Set, both of type
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
What are the implications of this design decision?