Categories library for Agda?

Question

Are there any "recommended" libraries that provide a easy-to-use formalisation of basic category theory in Agda? The Agda standard library seems to provide very little in this regard.

I'm looking for something with a low barrier to entry, similar to how one uses the algebraic structures such as Semigroup defined in the standard library.

For example, there are several notions of morphism in my current project, and overloading syntax for composition and identity gets awkward. The natural thing to do would be to introduce a suitable record type and use Agda's "instance arguments" mechanism to emulate a Morphism type class. But no doubt this must be a wheel that has been invented many times. (Ok, there is a structure called Morphism in the standard library which perhaps could be adapted to this purpose, so this isn't necessarily the best example, but you get the idea.)

I'm aware of this library, which looks comprehensive, but doesn't seem to be particularly active.

Answer 1

EDIT: The following was correct when it was written in Feb. 2022:

This is an old question, but it still gets hits on google and other searches, so: the de facto library is now agda-categories.

---

But now in Oct. 2024, this is not longer so. If one wants to do category theory in 'pure' MLTT then agda-categories is still the best choice. But if instead one wants 'book HoTT' then agda-unimath has a considerable amount of category theory too.

If instead one wants cubical type theory, there are two choices: the agda-cubical library and the 1lab. Choosing between them is complex, as they have different philosophies.

As maintainer of one of those libraries, I am too biased to offer a reliable opinion. But not so biased that I don't want to make sure "the world" knows the options.

Answer 2

I'm using the Categories library as mentioned above, and although I'm only using its basic features, it seems fine so far.