README

   1 ------------------------------------------------------------------------------
   2 Category Theory Library for Coq (coq-categories)
   3 Adam Megacz <megacz@acm.org>
   4
   5
   6 One of the difficulties with putting together a formalization of
   7 category theory is deciding how to organize it.  For example: should
   8 the formalization of exponential objects be grouped with the
   9 formalization of adjunctions or the formalization of monoidal
  10 categories?
  11
  12 I took the easy route and imitated the structure of Awodey's book
  13 __Category Theory__.  If you're looking for a concept (like
  14 exponential objects), find it in his book first, then look in the file
  15 witht he corresponding chapter number.
  16
  17 IMPORTANT NOTE ABOUT BIFUNCTORS: I've come across this really hideous
  18 performance bug in Coq which seems to be triggered whenever you start
  19 using functors whose domain or codomain is the product of two
  20 categories (i.e., product object in __Cat__).  Nobody on coq-club
  21 seems to know what's going on, and several different representations
  22 all trigger the bug.  Therefore, I have -- unfortunately -- chosen
  23 definitions which avoid product categories and bifunctors wherever
  24 possible.
  25
  26 IMPORTANT NOTE ABOUT SUBCATEGORIES: non-wide subcategories (that is,
  27 subcategories which do not include all objects of the parent category)
  28 are awkward to handle in Coq.  This is because they unavoidably
  29 involve reasoning about equality of objects, and objects are the
  30 indices of the types of hom-sets.  Coq is not very good at dealing
  31 with equality between types which are the indices of other types.  For
  32 this reason, I have two kinds of subcategory: WideSubcategory (which
  33 behaves quite nicely) and FullSubcategory (which can cause problems).
  34 Every subcategory of C is a full subcategory of a wide subcategory of
  35 C, and you must formalize it this way.