The Coq mailing list

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

Am 05.05.2011 18:01, schrieb Adam Chlipala:
> 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).

I don't think so.  Coq really changes the term on the left to
"fun X : Set => X" in the output.  Incidentally, the check

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

fails as I would expect.

- Gert