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.
Experience Implementing a Performant Category-Theory Library in Coq (ITP '14, arXiv version, Springer version)
Category theory in Coq
Constructive category theory
Category theory in ZFC
Coalgebras in Coq
Other proof assistants
and one in Idris:
copumpkin’s library ceases to work in recent versions of Agda and the following is a replacement in pure MLTT: