From 0acb7427506809b45fade2fa7f16ad13d6df40b3 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 3 Apr 2011 04:08:55 +0000 Subject: [PATCH 1/1] add README --- README | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 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. -- 1.7.10.4