Menu
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?
696
Set means rather different things in Coq and HoTT. In Coq, every object has a type, including types themselves. Types of types are usually referred to as sorts, kinds or universes. In Coq, the (computationally relevant) universes are Set , and Type_i , where i ranges over natural numbers (0, 1, 2, 3, ...).
As you already mentioned, Program Fixpoint allows the measure to look at more than one argument. Function creates a foo_equation lemma that can be used to rewrite calls to foo with its RHS. Very useful to avoid problems like Coq simpl for Program Fixpoint.
There are two parts to this answer.
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.
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.
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.
188
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
