What are the implications of Lean not having the type `Set`?

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?

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

StackExchange Computer Science Q#94192, answer score: 2