Hello, Toby Bartels wrote:
(Although Coq has equality at all types, and so can express evil, this equality is never used except within a given hom-set, as you can see in that file and also in the other files there.)
I'd like to add that while it is possible to do strict (or "evil") category theory with dependent composition in Coq, it is not at all a natural environment for it. Even a hypothesis b = b' will not *easily* allow you to compose f : Hom(a,b) with g : Hom(b',c). In fact, an axiom (uniqueness of identity proofs might be sufficient) must be added to Coq, and some explicit type cast is needed each time you want to do such a composition. (* You can find that at http://web.math.unifi.it/~benedikt/coq/cat/html/SynCaT.CAT.category_hom_tran... *) The proper type theory to do strict category theory in is an *extensional* type theory, where type conversion comes automatically with the equality b = b'. Greetings, ben ps. I've recently mentioned that on the Coq mailing list as well, so sorry for repeating stuff if you happen to follow both lists. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]