Check nat. (* => Set *)
But I'm able to pass nat to functions that take a parameter of type Type, even though Set and Type aren't the same. That being said, Type clearly isn't just a catch-all -- for example, trying to pass the literal 5 (a value of type nat) to a function that takes a parameter of type Type causes an error.
So why are objects of type Set allowed where it expects Type, but values of type nat are not allowed?
A type is a collection of objects, which all behave similarly. This is used pragmatically to ensure that functions are used correctly. For instance, if you say that a function takes as input a natural number, you expect it to work correctly if it receives 1 as input and also if it receives 3 as input. In this respect, 1 and 3 behave similarly.
Now, nat is the name of the collection. It is very different from the number 1 or 3, don't you agree? This is why you can't pass 1 or 3 as arguments to a function that would accept nat as argument.
But what is the type of nat? Well, nat is a type, so one would expect to write nat : Type, to say exactly that, but there is a subtlety. It comes from the fact that Type itself should have a type.
In Coq, there is an almost invisible sequence of objects named Type_0 Type_1, such that Type_0 : Type_1, Type_1 : Type_2, etc, with a subtyping rule so x : Type_i is enough to also have x : Type_(i+1), and technically, Set is just another name for Type_0. In other words, Set is the type for all types whose elements are not themselves types.
Every object of type Set also has type Type_i.
By default, the index i of Type_i is not printed, so sometimes it is a bit confusing.
Roughly speaking, Set is a subtype of Type, so every T that is a Set can be used where a Type is expected.
You might also be interested in this answer, which discusses the differences between Set and Type.
