Yes, and in principle you can generalize the type language into a full language with lambdas and such (type constructor is a lambda(ground type)->ground type), though you typically want it to be strongly normalizing so you know that the compiler will eventually halt. Then you don't need kinds, kind polymorphism, sorts, etc., you just have a dependently typed language with types and universes.