Skip to Content.
Sympa Menu

coq-club - [Coq-Club] categories, functors and universes

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] categories, functors and universes


chronological Thread 
  • 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/






Archive powered by MhonArc 2.6.16.

Top of Page