The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

So far I thought that "Type" is a placeholder
for a universe different from "Set" and "Prop".
But it turns out that

Check (fun X : Type => X) : Set -> Type.

is successful.  In fact, Coq replaces the left Type
with Set.  What is the motivation behind
this behavior?

- Gert