Category Theory in Coq by Adam Megacz.
From the webpage:
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
You will find the following helpful:
The Coq Proof Assistant (v8.4 2012) Links to source, binaries and documentation.
I first saw this in a tweet by Algebra Fact.