From: Adam Megacz
Date: Sun, 3 Apr 2011 04:08:55 +0000 (+0000)
Subject: add README
X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=commitdiff_plain;h=0acb7427506809b45fade2fa7f16ad13d6df40b3
add README
---
diff --git a/README b/README
new file mode 100644
index 0000000..bc14203
--- /dev/null
+++ b/README
@@ -0,0 +1,24 @@
+------------------------------------------------------------------------------
+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.