There are quite a few formalisations of category theory for proof assistants. For a relatively recent overview, see:

https://mathoverflow.net/questions/152497/formalizations-of-...

If I want to investigate this project, where should I start? (after configure/make)

Saunders MacLane: Category Theory for the Working Mathematician - most of the concepts implemented in this package are introduced there. I tend to dislike the "Category Theory for ___" type books, too much verbiage and misleading metaphors/analogies in many of them.

To my fellow self-taught mathematicians and computer scientists:

When I was starting out, I'd learn from what was too-dense-for-me (Mac Lane, Awodey, Spivak). When I didn't understand, I'd get frustrated, then go learn something else.

There are two differences between me-then, and me-now. First, I spend a lot more time choosing books to read. I find books that meet me where I am. I need all the help I can get. Second, when I don't understand, I skip being frustrated, and go learn something else.

I agree though with dkurai when it comes to math I'm already familiar with. If I'm reading what I already know, it's usually foundational to something I'm about to learn. Then, I need rigor and concision, to avoid being misled.

MacLane was too heavy for me, but I can wholeheartedly recommend lectures from Steve Awodey: https://www.youtube.com/watch?v=BF6kHD1DAeU

What's the license on this project? I'm wondering if it might fit in well with some work Tim Daly has started on the Axiom project hooking up computer algebra to coq et. al.:

https://lists.gnu.org/archive/html/axiom-developer/2015-07/m...