Survey of category theory in Coq

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

Category theory in Coq

Constructive category theory

Category theory in ZFC

Coalgebras in Coq

Math Classes

Other proof assistants


See also (and feel free to add to it)
and one in Idris:

copumpkin’s library ceases to work in recent versions of Agda and the following is a replacement in pure MLTT: