X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=README;h=579d6e1aa099ae8acb96a1f2f19ddccc66418efe;hp=bc1420380beb4beb217d7ab2c57dad2c3bd0f127;hb=20641452e40570b4bfc9429ca57b0cffca6eccfb;hpb=0acb7427506809b45fade2fa7f16ad13d6df40b3;ds=sidebyside

diff --git a/README b/README
index bc14203..579d6e1 100644
--- a/README
+++ b/README
@@ -22,3 +22,14 @@ 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.
+
+IMPORTANT NOTE ABOUT SUBCATEGORIES: non-wide subcategories (that is,
+subcategories which do not include all objects of the parent category)
+are awkward to handle in Coq.  This is because they unavoidably
+involve reasoning about equality of objects, and objects are the
+indices of the types of hom-sets.  Coq is not very good at dealing
+with equality between types which are the indices of other types.  For
+this reason, I have two kinds of subcategory: WideSubcategory (which
+behaves quite nicely) and FullSubcategory (which can cause problems).
+Every subcategory of C is a full subcategory of a wide subcategory of
+C, and you must formalize it this way.