Hi,
I have asked mathoverflow for formalizations of category theory in
proof assistants at
http://mathoverflow.net/questions/152497/formalizationsofcategorytheoryinproofassistants,
and was told that my list (copied below) was approximately complete.
I would like to know if anyone on this list knows of formalizations
that I missed; feel free to respond either by email or on the
mathoverflow thread.
Thanks,
Jason
The mathoverflow question:
The ones I know about are:
* https://bitbucket.org/JasonGross/catdb,
which became
https://github.com/JasonGross/HoTTcategories,
which became
https://github.com/HoTT/HoTT/tree/master/theories/categories
* https://github.com/benediktahrens/Foundations/tree/typesystems
* https://github.com/pcapriotti/agdacategories/
* https://github.com/jmchapman/restrictioncategories
* https://github.com/konn/categoryagda
* http://coq.inria.fr/pylons/pylons/contribs/view/MathClasses/v8.4
* http://www.cs.berkeley.edu/~megacz/coqcategories/
* 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/cryptoagda/cryptoagda/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:
* "Veriļ¬ed Computing in Homological Algebra: A Journey Exploring the
Power and Limits of Dependent Type Theory" by Arnaud Spiwack
(http://assertfalse.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/3540528857_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 MartinLof Type Theory" by
http://rd.host.cs.standrews.ac.uk/publications/CTMLTT.pdf
* "Automating Proofs in Category Theory" by Dexter Kozen, Christoph
Kreitz, and Eva Richter
(http://www.cs.unipotsdam.de/ti/kreitz/PDF/06ijcarcategories.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 publicdomain code implementing category
theory in a proof assistant, though I'm also interested in papers
about formalizations of category theory in proof assistants.
[For admin and other information see: http://www.mta.ca/~catdist/ ]
