The Coq mailing list

[ben <Benedikt.Ahrens AT unice.fr>]

hi,

[snipped]

Daniel Schepler wrote:
> Hi, I just recently started playing around with Coq.  So far I've input 
> some 
> basic definitions of category theory, and formalized van der Waerden's 
> proof 
> that the free group is a group structure on a set of reduced words.  But as 
> part of that development, I ran into problems proving that functors are 
> equal 
> in general.

I ran into the same problems and i did the same thing as you in my
formalization. However, the issue is a theoretical one. Since your
equality on objects is convertability and hence on a meta-level, your
categories are not *strict*. The "correct" notion of functor is then
something called "anafunctor". In short, you should take a 2-categorical
point of view here, i. e.  you should opt for isomorphisms of functors,
not equality.

You might want to have a look at
http://ncatlab.org/nlab/show/strict+category
There was also a discussion about equality on objects on the
"Categories" mailing list at the beginning of this year.


> The other problem I ran into is that when I tried to define the category of 
> categories, it gave a universe error.  I think I see what it's complaining 
> about, that trying to input Category into an instance of Category violates 
> the 
> type hierarchy.  


Sozeau uses type classes to define CAT, see somewhere on
http://mattam.org

Sorry for the imcomplete pointers. I can try to find the links if necessary.

Greetings
ben