Library Categories for Agda?

Question

Are there any “recommended” libraries that provide an easy-to-use formalization of the basic category theory in Agda? In this regard, the Agda standard library seems to be very small.

I'm looking for something with a low barrier to entry, similar to using algebraic structures like Semigroup defined in the standard library.

For example, in my current project there are several concepts of morphism, and overloading the syntax of composition and identity becomes inconvenient. It would be natural to introduce an appropriate record type and use the Agda "instance" argument mechanism to emulate a class like Morphism . But, of course, it should be a wheel that has been invented many times. (Well, the standard library has a structure called Morphism , which could possibly be adapted for this purpose, so this is not necessarily the best example, but you get the idea.)

I know this library that looks comprehensive, but doesn't seem particularly active.

Answer 1

I use the Categories library, as mentioned above, and although I use only its main functions, it seems so far away.