The Coq mailing list

[Theodoros Tsokos <T.Tsokos AT cs.bham.ac.uk>]

Dear all,

I'm trying to define closed monoidal category [1] in Coq.
I'm using Amokrane Saibi's "Contructive Category Theory"
library [2] as a base, for that purpose.

To define a closed monoidal category, I need a functor F:
CxC->C, where C is a category. Using Saibi's PROD [3] I can
create the product category:

Define F : PROD C C.

I would like though the product category of two categories
to be of type "Category" and not "PROD C C" that comes after
the above definition. Do you have any clue on the way I
could do something like that?

Probably, it might be a trivial answer, so apologies for
bothering with the email, but  thanks in advance for your
interest.

Theo.


[1] http://en.wikipedia.org/wiki/Monoidal_category
[2] - http://coq.inria.fr/contribs/category.html
    - http://citeseer.ist.psu.edu/355887.html
[3]
http://www.cs.bham.ac.uk/~txt/coqdoc/CATEGORY_THEORY.CATEGORY.PROD.html 





--
| Theodoros G. Tsokos                                      |
| http://www.cs.bham.ac.uk/~txt                            ;|
| School of Computer Science, The University of Birmingham |
| Edgbaston, Birmingham, B15 2TT, United Kingdom           |
| -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- |
| "The freedom of speech includes the freedom to shut up"  |
| -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- |
| "Democracy: the freedom to say whatever one wants and    |
| the capital to implement whatever it wants"              |
--