The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Richard Dapoigny wrote:
> I have some basic question about the hierarchy of universes in Coq. 
> Suppose that we have the following code fragment:
> Definition PT  := Type.
> Definition ED : PT := Type.
> Definition PD : PT := Type.
> Print Universes.
> Variable Test : ED->Prop.
> Variable x : ED.
> Variable y : PD.
> Check Test x.
> Check Test y.
> We expect that the universes ED and PD are different, however, the 
> test works for both.

Why do we expect that?  The act of calling [Test] on both asserts a 
relationship between them.