The Coq mailing list

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

The lack of support for universe polymorphism is already present with
very simple examples (no need to consider the category of categories):

  Inductive T : Type := t : Type -> T.

Check t T  raises a universe inconsistency error.  But it should be
accepted by Coq because when I define the inductive type T'
(isomorphic to T) by

  Inductive T' : Type := t' : Type -> T'.

Check t T'  is OK!

> Every few months, someone asks this question on coq-club. :)

This is a pity that, in spite of the many requests, universe
polymorphism is not considered seriously by Coq developers. (Please
someone, tell me I am wrong).

>  there is no way to mention universe levels explicitly in source code

Even with that you would need to duplicate definitions. If you define
categories at level 0 and 1, then you have to duplicate 4 times the
definition of functors (depending on the levels of source and target
categories), 16 times the definition of natural transformation, and I
do not count the duplications for composition of functors and natural
transformations!!

> Sozeau uses type classes to define CAT

As far as I understand, it does not solve the problem at hand.