The Coq mailing list

[David Leduc <david.leduc6 AT googlemail.com>]

Bruno Barras 
<bruno.barras AT inria.fr>
 wrote:
> Are you saying you would expect "Check t T" to answer T ? Seriously ?

Yes, seriouly.

> 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?