Survey of category theory in Coq

Using 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

5 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:

5

Coq-HoTT actually has two “category theory libraries”. There is also the “WildCat” library which is based on typeclasses and makes “lazy” approximations to coherence. This has been quite a useful organisational principle, but when it comes to getting some actual results out of it, we have always fallen short, mostly due to lack of time and attention. I originally tried to prove that pushouts commute with pushouts in HoTT via the standard having a right adjoint preserves colimits argument, but I couldn’t pull through the coherence issues. [WIP] Adjunctions, limits, colimits in wildcats + possible progress towards 3x3 lemma for pushouts by Alizter · Pull Request #1571 · HoTT/Coq-HoTT · GitHub