Type : Type in Coq

Question

By accident, I found that one can make the following definition in Coq:

Definition x := Type : Type.

What does Type : Type mean? What are some use cases for such definition?

Answer 1

There are two parts to this answer.

What does Definition x := y : A mean?

This means that x is defined to be y and there is an assertion that y is of type A. Usually, this assertion is superfluous because Coq is able to determine the type of y just by itself. However, sometimes a term has too many implicit parts, so the assertion is needed in order to determine all those implicit parts.

What does Type : Type mean?

An example of having implicit parts is Type. It may come as a surprise to you that there isn't a single Type in Coq. Instead there is an infinite hierarchy of types Type@{0}, Type@{1}, Type@{2}… with Type@{i} : Type@{j} if i < j. This means that every universe (Type@{j}) contains every universe with a smaller level as an element.

However, by default, Coq doesn't explicitly show these "universe levels". Coq is usually smart enough that it can figure out the universe levels (or make them generic) without bothering you at all. You can tell Coq to show them with the vernacular command Set Printing Universes. or by setting the option in the IDE menu if you're using that. Then, after defining x as you did, using the command Print x. will display

x = 
Type@{Top.2}
     : Type@{Top.1}
(* {Top.2 Top.1} |= Top.2 < Top.1
                     *)

So x is defined to be Type@{Top.2} and has type Type@{Top.1}. Top.1 and Top.2 are just names for generic universe levels. The part of the message at the bottom is simply stating that Top.2 must be less than Top.1. This is because we need Type@{Top.2} to have the type Type@{Top.1}. Remember that universes contain the universes below them, but not the ones above them.

Side question: Why are there multiple levels of Type?

In short, if we only had a single Type with Type : Type, it would be possible to show that the system is inconsistent. This is called Girard's paradox (or a simpler variant known as Hurkens' paradox). See this answer for some nice details.

If you want another explanation of Coq's universes, see this great answer.