For some reason, category theory is often a target for formalization efforts, in particular in Coq.
This is an ongoing effort to document the growing collection of Coq category theory libraries and libraries that contain fragments of category theory. Relevant papers are also listed.
UniMath
HoTT
Experience Implementing a Performant Category-Theory Library in Coq (ITP '14, arXiv version, Springer version)
Categories
Category theory
Category theory in Coq
http://www.megacz.com/berkeley/coq-categories/
http://git.megacz.com/coq-categories.git