Survey of category theory in Coq

#1

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

Constructive category theory

Category theory in ZFC

Coalgebras in Coq

Math Classes

Other proof assistants


https://www.isa-afp.org/entries/Category2.html

3 Likes
#2

See also https://mathoverflow.net/questions/152497/formalizations-of-category-theory-in-proof-assistants (and feel free to add to it)

#3

https://math-classes.github.io/
and one in Idris:

#4

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