In Coq there is a hierarchy of types each one denoting the type of the previous i.e. Type_0 : Type_1, Type_1 : Type_2 and so on. In coqtop however when I type Check Type. I get Type : Type which looks like a contradiction but is not since Type is implicitly indexed.
Question: How to enable explicit indexing of the Type universes?