Is there an equality or inequality relation between Type and Set in Coq ?
I am learning about Coq's type system and understand that the type of Set is Type@{Set+1}, and that the type of Type@{k} is Type@{k+1}. I tried to prove that Type = Set, and then tried to prove Type <> Set, but I failed in both cases.
I started with
Lemma set_is_type : Type = Set.
Proof.
reflexivity.
which gives an error message saying that Unable to unify "Set" with "Type@{Top.74}".
Then I tried
Lemma set_is_not_type : Type <> Set.
Proof.
intros contra.
At this point I do not know how to proceed. The tactic discriminate did not work, neither inversion contra.
Which one of the above two lemmas can be proved?
This actually isn't an entirely trivial theorem. To show that Type = Set results in a paradox (and hence that having separate levels of Type is necessary), you'll need to use a standard result akin to Russell's paradox from set theory. Specifically, you'll need Hurken's paradox, which essentially says that smaller Types can't be on equal footing to larger Types (remember that Type is polymorphic in Coq, and in particular, Set is the lowest level (or second lowest if you include Prop)).
The particular theorem we want can be found in the standard library.
Require Logic.Hurkens.
Import Logic.Hurkens.TypeNeqSmallType.
Check paradox.
paradox has the type signature forall A : Type, Type = A -> False. This is pretty much what we want to prove, since Set: Type (at least if Type is large enough).
Lemma set_is_not_type: Type <> Set.
Proof.
intro F.
exact (paradox _ F).
Defined.
Coq automatically sets restrictions on the Type in this lemma to ensure that Set: Type.
On the other hand, Set is equal to some level of Type, so we should be able to prove that Type = Set with some different constraints on this Type. The easiest way I found to do this was to prove that Type = Type, but then instantiate this theorem with Set. For whatever reason, as you found, reflexivity can't enforce universe constraints by itself. To do this, we need to make both the lemmas universe polymorphic so that they can be instantiated with a particular universe level.
Polymorphic Lemma type_is_type: Type = Type.
Proof.
reflexivity.
Defined.
Polymorphic Lemma type_is_set: Type = Set.
Proof.
apply type_is_type.
Defined.
The easier way to make everything universe polymorphic is to put Set Universe Polymorphism. before everything.