The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Le 30/06/2012 00:52, Adam Chlipala a écrit :
> 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.
The point here was to check with the test whether ED and PD correspond 
to distinct universes which means that the universe hierarchy is a 
partial order (as in ECC) . If it is not the case then the hierarchy 
simply correspond to a total order (linear).

--
And the wounded skies above say
it's much too much too late.
Well, maybe we should all be praying for time.

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard