Type/Kind hierarchy is unified when you write a dependently typed system
i'm being pedantic, but i don't think that's always the case. afaik
Type : Type
leads to "inconsistency" (sounds like Russell's paradox, but my knowledge of the theory gets flaky here). so e.g. in Coq there's actually a hierarchy of "universes":
"[The type of Int is Set, ] the type of Set is Type(0), the type of Type(0) is Type(1), the type of Type(1) is Type(2), and so on."
Comments
i'm being pedantic, but i don't think that's always the case. afaik
leads to "inconsistency" (sounds like Russell's paradox, but my knowledge of the theory gets flaky here). so e.g. in Coq there's actually a hierarchy of "universes":http://adam.chlipala.net/cpdt/html/Universes.html
(though a dependently-typed system may hide universes from the user by default and offer "universe polymorphism" to allow them to gloss over it)