From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7984 Path: news.gmane.org!not-for-mail From: Jason Gross Newsgroups: gmane.science.mathematics.categories Subject: Fwd: Formalizations of category theory in proof assistants? Date: Sun, 19 Jan 2014 12:27:10 -0500 Message-ID: Reply-To: Jason Gross NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1390158600 18657 80.91.229.3 (19 Jan 2014 19:10:00 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 19 Jan 2014 19:10:00 +0000 (UTC) To: "categories@mta.ca" Original-X-From: majordomo@mlist.mta.ca Sun Jan 19 20:10:09 2014 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.186]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1W4xl2-0004aP-IE for gsmc-categories@m.gmane.org; Sun, 19 Jan 2014 20:10:08 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:40703) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1W4xjT-0006XY-G3; Sun, 19 Jan 2014 15:08:31 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1W4xjS-0000Mm-U4 for categories-list@mlist.mta.ca; Sun, 19 Jan 2014 15:08:30 -0400 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7984 Archived-At: Hi, I have asked mathoverflow for formalizations of category theory in proof assistants at http://mathoverflow.net/questions/152497/formalizations-of-category-theory-= in-proof-assistants, 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/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: * "Veri=EF=AC=81ed Computing in Homological Algebra: A Journey Exploring th= e 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=3D10.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. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]