The Coq mailing list

[David Nowak <David.Nowak AT lsv.ens-cachan.fr>]

Hello,

In the Coq formalization of category theory by Huet and Saïbi, functors are only 
defined between categories of the same size, (the type constructor Functor is of 
type Category->Category->Type). I guess its due to limitations in the treatment 
of universes by Coq. Are there any plan to (or any patch that) extend Coq such 
that it deals better with universes ?

David.

--
David Nowak
LSV - CNRS UMR 8643 - ENS de Cachan
61, av. du Président Wilson, 94235 Cachan Cedex
tél: +33 1 47 40 55 69   fax: +33 1 47 40 24 64
http://www.lsv.ens-cachan.fr/~nowak/