The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Gert Smolka wrote:
> 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?

I think this is standard contravariant subtyping for function types, 
since [Set] is a subtype of [Type] (for any universe index attached to 
the latter).