As I understand it, as a (value-level) function
f that takes a value
x of type
T and returns a value
f x of type
U has type
T → U, a type constructor
F (a type-level function) that takes a type
T and returns a type
F T is said to have kind
* → * or
Type → Type, where
Type is the type of "small" types, which are those types the values of which are not themselves types, unlike
Some languages focussed on writing mathematical proofs take care to distinguish different levels of
Type, to avoid ‘Girard's paradox’.
The function type
T → U has type
Type does not have type
Type but has type
Type₁ has type
Type₂, and so forth.
Coq and Agda call the types of types sorts and spell the type
Set and the types
Type(n) (in Coq) or
Setₙ (in Agda). This sequence of types
Typeₙ may be called a universe hierarchy.
I shall not be surprised if some of my above-stated understanding is wrong, as I have not studied any of this formally or systematically. If my understanding is not so wrong as to make my question meaningless, my question is:
As the type of value-level functions fits into the universe hierarchy, I wonder how kinds, the types of type-level functions, fit into the universe hierarchy. The things that fit into the universe hierarchy are things that have types, so what, if anything, is the type of a kind? If kinds do not have types, then do they have something like types? If so, do those kind-types form their own kind-universe hierarchy?
Google showed me pages about type universes and a few pages about kinds, but I see nothing that appears to discuss both together.