The Coq mailing list

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

hi,

Daniel Schepler wrote:

> 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.

The propositional equality (Leibniz) is not compatible with/too weak for
the typing of the morphisms. This non-compatibility is like working with
a non-strict category. As soon as you want to formalize a strict
category concept, you need to do some acrobatics. So i should have said
that a formalization with dependent composition in intensional type
theory is "more suitable" to do non-strict category theory.

Are you using a setoidal equality on morphisms as in ConCaT ?

The definition of a heterogeneous equality predicate "===" on morphisms
(as done in ConCaT) might help. You can then define functor equality
extensionally as

Definition EXT_Functor: relation (Functor C D) :=
     fun F G => forall a b : C, forall f: a --> b,
                  F f === G f.

However, you'll still need Leibniz equality on functors, e. g. when you
want to establish properties of horizontal composition of natural
transformations.
(You can find all of this in my lib of cats on
http://math.unice.fr/~ahrens ;).

Apart from that i found that when working with some specific category,
you can often avoid equality on objects, say a = b, by translating them
to an isomorphim a -> b in your formalization.


> 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.

There are some theories in the proof assistant Isabelle/{HOL,HOLZF}
using this approach (e.g. G. O'Keefe). Also, as far as i remember,
Carlos Simpson's contrib in Coq uses this formulation.

> 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.

Sheaves have been formalized by Laurent Chicli in his PhD thesis. A
second part of his thesis is about quotients in Coq. Unfortunately it
seems that it is available in french only. The quotient part is also
treated in an article called "Mathematical quotients and quotient types
in Coq" by Chicli, Pottier and Simpson.

greetings,
b