The Coq mailing list

[Benjamin Werner <benjamin.werner AT polytechnique.org>]

Hello,

Le 10 sept. 2010 à 17:32, David Leduc a écrit :

Bruno Barras <bruno.barras AT inria.fr> wrote:

Are you saying you would expect "Check t T" to answer T ? Seriously ?

Yes, seriouly.

Yes, it has been noticed that universe polymorphism can lead to some

weird situations. 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?