The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

Quoting Benjamin Werner 
<benjamin.werner AT polytechnique.org>:

> Yes, it has been noticed that universe polymorphism can lead to some
> weird situations. [...]

It seems we need a clear definition of "universe polymorphism".  Bob  
Harper and I gave a definition of "universe polymorphism" that is  
sound w.r.t. a version of CC with universes [Type checking with  
universes. Theoretical Computer Science, 89:107-136, 1991].  The type  
system of this paper is pre-ECC (cumulative, but not "fully  
cumulative") and doesn't have inductive types.  I don't know how this  
old paper will stand up to modern scrutiny.

It seems that Agda has some experimental feature of explicit  
(outermost?) quantification over universe levels that should be looked  
into.

Best,
Randy
--
> [...] For instance, through a usual Aczel style encoding of
> set theory, one can formalize Russell's paradox. More precisely,
>
> - define Russell's "paradoxical set" R = {x : set |  x \notin x } : set
>     ( where set is a well chose inductive type, not "Set")
>
> - prove    R \in R      *and*      (R \in R) -> False
>
> but at the last step, when one wants to conclude False from the to   
> results above,
> the universe mechanism would refuse.
>
>
> I understand this can seem a little artificial. I am personally not   
> sure what is the
> best way to handle this question.
>
>
>
> Cheers,
>
> Benjamin
>
>
>
>
>
> > > The problem is that it would strongly suggest that T can be embedded
> > > inside an inhabitant of T,
> >
> > I find it convenient to think that the category of categories is a category.
> > Even though I know it is not a object of itself.
> > It allows me not to duplicate definitions.
> >
> > > And this exactly to avoid this that universes were introduced.
> >
> > Of course, I still want them behind the scene to avoid contradictions.
> >
> > > In the first case, this may slow down type-checking a lot.
> >
> > > From a user point-of-view, it cannot be worse than duplicating
> > definitions dozens of times, is it?



--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.