Category Theory in Coq

This is a quick page I've thrown together for my Coq library formalizing basic category theory. The development follows Steve Awodey's book on category theory; the files are named after chapters and subchapters of that book for easy reference.

Getting It

The gitweb is here. You might also want to look at the README

Design Decisions

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 an existing book. If you're looking for a concept (like exponential objects), find it in Awodey's book first, then look in the file with the corresponding chapter number.

Comparison to Other Libraries

In general, what makes this library unique is:

• It uses Coq's type classes (which weren't available when most of the other libraries were written)

• It emphasizes enriched category theory. Rather than the collection of morphisms between two objects forming a set (which appeals to set theory) or a type (which appeals to type theory), an enriched category has an object of morphisms between any two objects. This “object of morphisms” is in a larger category, one level up a (potentially) infinite hierarchy.

• It does not rely on extra axioms (like JMEq or EqDep). This is partly because this library avoids “strict” concepts (e.g. strict monoidal functors); these concepts involve equality on objects, which often becomes some sort of heterogeneous equality in a formalization.

It also works with the latest version of Coq (8.3pl2); some of the other libraries have fallen into disrepair and no longer work with the latest version of Coq.

Deviations/Additions vs Awodey's Book

This is not a complete formalization of Awodey's book, but what I do formalize follows his book. Mostly what's missing is limits/colimits and almost everything after chapter 7.

PreMonoidal Categories: Awodey's book does not cover binoidal or premonoidal categories. This formalization includes them (BinoidalCategories.v, PreMonoidalCategories.v, and PreMonoidalCenter.v). Furthermore, in the Coq formalization a monoidal category is defined to be a premonoidal category in which all morphisms are central. There is a lemma proving that the usual construction (involving a bifunctor) produces a monoidal category in the sense used here. A monoidal functor is simply a premonoidal functor between monoidal categories; there is no actual MonoidalFunctor class.

Enrichment: I develop enriched categories much further than Awodey does, and give them a somewhat more central place.

Strictness: I work quite hard to avoid ever talking about equality between objects. This is not because it's evil, but rather because objects are indices of the types of hom-sets of categories in this development, and Coq has serious problems when it comes to reasoning about equality between type indices. Most “sensible” facts about these situations are independent of the axioms of CiC; although you can assert them as axioms, none of the Coq infrastructure (simpl, setoid rewriting, the termination checker, etc) knows about those axioms, so you end up having to work with one hand tied behind your back. I found it to be completely unworkable for a large development.

Large Categories: I don't formalize the category of categories because Coq's universe polymorphism is only π₁. There's an experimental “category of small categories” development which asks for a type indexing the “small” categories and then works one universe up from that. I'm still not sure that I can build functor categories that way, though.

Computational Irrelevance: I distinguish between naturally isomorphic functors (IsomorphicFunctors) and natural isomorphisms (NaturalIsomorphism). The formalization of “F and G are naturally isomorphic” is non-informative; the actual natural iso lives in Prop and you can't use it in any extracted computation; this is useful in situations where you've asserted the  1-truncation axiom (UIP) and in conjunction with -dont-load-proofs it can make Coq run much more quickly. There's a similar situation with Isomorphic vs Isomorphism although I don't use it as extensively.

Algebras: Awodey spends a decent amount of time on the notion of a “group internal to a category” but doesn't define the general case of an algebra internal a category; this is just as well, the subject of his book is category theory, not universal algebra. I'm working on moving towards a “bootstrapping” using monoidal categories and generalized algebraic theories, much like you can bootstrap using finite-limit categories and essentially algebraic theories. Briefly, the theory of finite limit categories is an essentially algebraic theory, and you can interpret an essentially algebraic theory in a finite limit category. The same goes for monoidal categories and GATs: the theory of monoidal categories is a GAT, and you can interpret any GAT in a monoidal category.

Miscellaneous: I include conservative functors, whiskering, and Freyd categories, which don't appear in his book. There's some experimental stuff on enriched fibrations and Street cleavages.

Problems/Issues

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.

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. WideSubcategory behaves very nicely and is quite easy to work with. Dealing with FullSubcategory tends to require a lot more work.

rendered from WIX