Return to Question

What are the existing formalizations of category theory in proof assistants?

I'm primarily interested in public-domain code implementing category theory in a proof assistant, though I'm also interested in papers about formalizations of category theory in proof assistants.

I've added answers to this question for all of the papers and formalizations that I know about, and details about the constructions in my own repository as of the date of adding. In addition to adding formalizations that you don't see on here, you should feel free to add details and improve the formatting of the other entries (especially including what language the formalization is in, what category theory it covers, links to papers presenting it and/or publicly available source code, whether or not it's under active development, what the newest version of the proof assistant it compiles with is, etc.).

What are the existing formalizations of category theory in proof assistants?

I'm primarily interested in public-domain code implementing category theory in a proof assistant (Coq, Agda, Isabelle/HOL, Mizar, NuPRL, Twelf, Lego, Idris, Matita, etc.), though I'm also interested in papers about formalizations of category theory in proof assistants.

I've added answers to this question for all of the papers and formalizations that I know about, and details about the constructions in my own repository as of the date of adding. In addition to adding formalizations that you don't see on here, you should feel free to add details and improve the formatting of the other entries (especially including what language the formalization is in, what category theory it covers, links to papers presenting it and/or publicly available source code, whether or not it's under active development, what the newest version of the proof assistant it compiles with is, etc.).

Edit: Currently in the process of moving the list to separate answers.

The ones I know about are:

• https://bitbucket.org/JasonGross/catdb, which became https://github.com/JasonGross/HoTT-categories, which became https://github.com/HoTT/HoTT/tree/master/theories/categories
• https://github.com/benediktahrens/Foundations/tree/typesystems
• https://github.com/pcapriotti/agda-categories/
• https://github.com/jmchapman/restriction-categories
• https://github.com/konn/category-agda
• http://coq.inria.fr/pylons/pylons/contribs/view/MathClasses/v8.4
• http://www.cs.berkeley.edu/~megacz/coq-categories/
• http://coq.inria.fr/pylons/pylons/contribs/view/Coalgebras/v8.4
• http://coq.inria.fr/pylons/pylons/contribs/view/Algebra/v8.4
• https://github.com/copumpkin/categories
• https://github.com/crypto-agda/crypto-agda/tree/master/FunUniverse
• http://coq.inria.fr/pylons/pylons/contribs/view/ConCaT/v8.4
• http://coq.inria.fr/pylons/pylons/contribs/view/CatsInZFC/v8.4
• http://mattam.org/repos/coq/cat/
• https://github.com/benediktahrens/rezk_completion
• https://github.com/rs-/Triangles
• https://github.com/benediktahrens/coinductives

I also know about the following papers about formalizing category theory in proof assistants:

• "Verified Computing in Homological Algebra: A Journey Exploring the Power and Limits of Dependent Type Theory" by Arnaud Spiwack (http://assert-false.net/arnaud/papers/thesis.spiwack.pdf)
• "Galois: a theory development project" by Peter Aczel (http://www.cs.man.ac.uk/~petera/galois.ps.gz)
• "A mechanically assisted constructive proof in category theory" by James Altucher and Prakash Panangaden (http://link.springer.com/chapter/10.1007/3-540-52885-7_110)
• "Category Theory in Coq" by Carvalho (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.9846)
• "Category Theory as an Extension of Martin-Lof Type Theory" by http://rd.host.cs.st-andrews.ac.uk/publications/CTMLTT.pdf
• "Automating Proofs in Category Theory" by Dexter Kozen, Christoph Kreitz, and Eva Richter (http://www.cs.uni-potsdam.de/ti/kreitz/PDF/06ijcar-categories.pdf)
• "Towards a readable formalisation of category theory" by Greg O'Keefe (http://users.cecs.anu.edu.au/~okeefe/work/fcat4cats04.pdf)

I'm primarily interested in public-domain code implementing category theory in a proof assistant, though I'm also interested in papers about formalizations of category theory in proof assistants.

I'm primarily interested in public-domain code implementing category theory in a proof assistant, though I'm also interested in papers about formalizations of category theory in proof assistants.

I've added answers to this question for all of the papers and formalizations that I know about, and details about the constructions in my own repository as of the date of adding. In addition to adding formalizations that you don't see on here, you should feel free to add details and improve the formatting of the other entries (especially including what language the formalization is in, what category theory it covers, links to papers presenting it and/or publicly available source code, whether or not it's under active development, what the newest version of the proof assistant it compiles with is, etc.).

The ones I know about are:

Edit: Currently in the process of moving the list to separate answers.

The ones I know about are: