The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

On Tuesday 04 December 2007 11:42:55 am Theodoros Tsokos wrote:
> 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.

This statement is a little strange.  Its the usually way to start a 
definition-by-tactic, which I don't think is what you want.

I think you want

Define F := PROD C C : Category.

Which defines F as the product category of C and C.

If you have

Define F : PROD C C := ....

Then F is interpreted as an object of the category PROD C C, and will have 
type (Ob (PROD C C)), or whatever that reduces to.  This is due to coercion 
magic that automaticly inserts the Ob projection.

Does that help?


> 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