The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thursday 09 September 2010 01:56:47 ben wrote:
> 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.

Well, I also proved a lemma that Leibniz equality of functors is equivalent 
to 
eq_dep of the (ObjFunc,MorFunc) pairs (assuming proof_irrelevance, of 
course).  
And I was always using Leibniz equality on Obj D (along with 
functional_extensionality) to compare ObjFunc.  So I think my categories were 
strict categories, unless I'm misunderstanding what you were saying.

I also thought of the possibility of using the source/target formulation of 
the category definition.  But that would have the disadvantage that you'd 
always have to be proving and passing around mini-lemmas on the compatibility 
of compositions.

Anyway, it looks like categories are well covered.  What about topological 
spaces / measure theory and functional analysis / homological algebra / 
sheaves and topoi?  I don't see general treatments of any of those on the Coq 
contrib page, but it looks like there's a lot of Coq material out there 
that's 
not posted on Coq contrib.

Also, I'm just curious: is there any particular reason the Coq standard 
library doesn't implement quotients by equivalence relations?  Granted, you'd 
need something like constructive_definite_description to define many 
functions 
with such types as domains.  But that axiom seems relatively unobjectionable 
to me (I think it's valid on any topos), and the construction would mean you 
wouldn't have to adapt everything taking in Types to be able to handle 
setoids 
as well.
-- 
Daniel Schepler