The Coq mailing list

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

Richard Dapoigny wrote:
> 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).

I'm not sure what you mean by the above.  Coq maintains a partial order 
(the universe constraint graph) that must always be concretizable to 
some total order, though Coq never materializes that order, to my 
knowledge.  The [Check Test y] line just has the effect of asserting [PD 
<= ED] in either of these kinds of order, which leads to a constraint 
system that is consistent.