> What are the existing formalizations of category theory in proof assistants? 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.