------------------------------------------------------------------------------
Category Theory Library for Coq (coq-categories)
Adam Megacz
One of the difficulties with putting together a formalization of
category theory is deciding how to organize it. For example: should
the formalization of exponential objects be grouped with the
formalization of adjunctions or the formalization of monoidal
categories?
I took the easy route and imitated the structure of Awodey's book
__Category Theory__. If you're looking for a concept (like
exponential objects), find it in his book first, then look in the file
witht he corresponding chapter number.
IMPORTANT NOTE ABOUT BIFUNCTORS: I've come across this really hideous
performance bug in Coq which seems to be triggered whenever you start
using functors whose domain or codomain is the product of two
categories (i.e., product object in __Cat__). Nobody on coq-club
seems to know what's going on, and several different representations
all trigger the bug. Therefore, I have -- unfortunately -- chosen
definitions which avoid product categories and bifunctors wherever
possible.