The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Dear Bas,

> It seems that this could have been avoided if Definitions could be
> universe polymorphic.
> Are there any plans to change this?

Definitions that map to inductive types inherit the sort-polymorphism
of the underlying inductive type. So if your type of category is
defined inductively you should be able to reuse the definition for
talking both of small categories and of the category of small
categories.

Proper definitions of type "forall U:Type, ... -> Type" (such as
"Definition id A (x:A) := x") are not themselves sort-polymorphic. I
experimented it once but it induced a significant overhead and I
renounced to activate the corresponding code.

Best regards,

Hugo