coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: David Nowak <David.Nowak AT lsv.ens-cachan.fr>
- To: coq-club <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] categories, functors and universes
- Date: Wed, 16 Oct 2002 11:40:11 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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/
- [Coq-Club] categories, functors and universes, David Nowak
Archive powered by MhonArc 2.6.16.