42
$\begingroup$

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.).

Improve this question
$\endgroup$
7
  • $\begingroup$ Here is a suggestion that you may ignore if you want: make the entries in your list into individual answers, and encourage people to add a brief description to each. $\endgroup$
    – S. Carnahan ♦
    Dec 21, 2013 at 5:23
  • 2
    $\begingroup$ One suggestion : the proof assistant Mizar works in a variant of ZFC. And its library of certified proofs is already very huge. You could investigate in this direction. Unlike many people, I don't think that coq is appropriate for formalizing math: because the axiom of choice and the law of excluded middle cannot live together in coq. The situation seems to be different with HoTT, as far as I understand the theory. $\endgroup$
    – Philippe Gaucher
    Dec 21, 2013 at 8:42
  • $\begingroup$ The Algebra contribution also has some category theory. coq.inria.fr/pylons/pylons/contribs/view/Algebra/v8.4 $\endgroup$
    – Rui Baptista
    Dec 22, 2013 at 14:44
  • 1
    $\begingroup$ The problem with the question is that OP listed all existing libraries. There is nothing to answer. $\endgroup$
    – Andrej Bauer
    Dec 29, 2013 at 9:36
  • 3
    $\begingroup$ I do intend to follow S. Carnahan's suggestion to make entries in the list into individual answers, and encourage elaboration, and people are free to do this for me. The primary reason that I asked this question is that some of the libraries I'm most familiar with are hard to find on google, so I'm not at all confident that I actually got all of them. My hope was that if other people are familiar with other libraries that are hard to find on google, they'll mention them for me. (And, thank Rui, I'm about to add that one to the list in the question.) $\endgroup$
    – Jason Gross
    Jan 1, 2014 at 17:44

36 Answers 36

Reset to default
1
2
0
$\begingroup$

The Coq ConCaT contribution, Constructive Category Theory, http://coq.inria.fr/pylons/pylons/contribs/view/ConCaT/v8.4, by Amokrane Saïbi. Presented in "Constructive Category Theory" (1998), by Gérard Huet and Amokrane Saïbi

According to Greg O'Keefe on fa.isabelle,

Objects are types, arrows are "setiods". Odd.

Gets to Cartesian Closed Categories.

Based on earlier work in Lego by Aczel.

Additions by Carvalho 1998.

Improve this answer
$\endgroup$
0
$\begingroup$

"A mechanically assisted constructive proof in category theory" by James Altucher and Prakash Panangaden in NuPRL

According to Greg O'Keefe on fa.isabelle,

No work since 1990 it seems. I haven't seen the sources, but [3] claims that adjunctions, triples and Cartesian closed categories were all defined. Adjoint functor theorem proved.

Improve this answer
$\endgroup$
0
$\begingroup$

According to Greg O'Keefe

Lockwood Morris has used HOL [29] to formalise most of [15, I,II,III], including Yoneda's lemma. There are no publications yet, nor has there been a public distribution of the HOL code. My sources are an unpublished manuscript [17] and email correspondence with the primary author.

Improve this answer
$\endgroup$
0
$\begingroup$

mathink's Category Theory in Coq repo, https://github.com/mathink/Cat_on_Coq

Improve this answer
$\endgroup$
0
$\begingroup$

Jacques Carette's agda-categories.

Improve this answer
$\endgroup$
1
2

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.