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

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

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.