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

  • Community Wiki at OP's request. – Todd Trimble Dec 21 '13 at 3:12
  • 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. – S. Carnahan Dec 21 '13 at 5:23
  • 2
    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. – Philippe Gaucher Dec 21 '13 at 8:42
  • 1
    The problem with the question is that OP listed all existing libraries. There is nothing to answer. – Andrej Bauer Dec 29 '13 at 9:36
  • 3
    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.) – Jason Gross Jan 1 '14 at 17:44

35 Answers 35

HoTT/HoTT Categories

Links: https://github.com/HoTT/HoTT/tree/master/theories/Categories (current), https://github.com/JasonGross/HoTT-categories (old), https://bitbucket.org/JasonGross/catdb (oldest). Interactive index, non-interactive index, top-level wiki

Language: Coq 8.6; will compile with 8.7 when it comes out; the oldest version compiled with Coq 8.4)

Author: Jason Gross

Active Development: No, but actively maintained in its present form (as of June 2017)

Concepts Formalized:

  • 1-precategories (in the sense of the HoTT Book)

  • univalent/saturated categories (or just categories, in the HoTT Book)

  • functor precategories $\mathcal C \to \mathcal D$

  • dual functor isomorphisms $\text{Cat} \to \text{Cat}$; and $(\mathcal{C} \to \mathcal{D})^{\text{op}} \to (\mathcal{C}^{\text{op}} \to \mathcal{D}^{\text{op}})$

  • the category Prop of ($U$-small) hProps

  • the category Set of ($U$-small) hSets

  • the category Cat of ($U$-small) strict (pre)categories (strict in the sense of the objects being hSets)

  • pseudofunctors

  • profunctors

    • identity profunction (the hom functor $\mathcal C^\text{op} \times \mathcal C \to \text{Set}$)
  • adjoints

    • equivalences between a number of definitions:
      • unit-counit + zig-zag definition
      • unit + UMP definition
      • counit + UMP definition
      • universal morphism definition
      • hom-set definition (porting from old version in progress)
    • composition, identity, dual
    • pointwise adjunctions in the library, $G^\mathcal{E} \dashv F^\mathcal{C}$ and $\mathcal{E}^F \dashv \mathcal{C}^G$ from an adjunction $F \dashv G$ for functors $F : \mathcal C \leftrightarrows \mathcal D : G$ and $\mathcal E$ a precategory (still too slow to be merged into the library proper; code here)
  • Yoneda lemma

  • Exponential laws

    • $\mathcal C^0 \cong 1$; $0^{\mathcal C} \cong 0$ given an object in $\mathcal C$
    • $\mathcal C^1 \cong \mathcal C$; $1^{\mathcal C} \cong 1$
    • $\mathcal C^{\mathcal A + \mathcal B} \cong \mathcal C^{\mathcal A} \times \mathcal C^{\mathcal B}$
    • $(\mathcal A \times \mathcal B)^{\mathcal C} \cong \mathcal A^{\mathcal C} \times \mathcal B^{\mathcal C}$
    • $(\mathcal A^{\mathcal B})^{\mathcal C} \cong \mathcal A^{\mathcal B \times \mathcal C}$
  • Product laws
    • $\mathcal C \times \mathcal D \cong \mathcal D \times \mathcal C$
    • $\mathcal C \times 0 \cong 0 \times \mathcal C \cong 0$
    • $\mathcal C \times 1 \cong 1 \times \mathcal C \cong \mathcal C$
  • Grothendieck construction (oplax colimit) of a pseudofunctor to Cat
  • Category of sections (gives rise to oplax limit of a pseudofunctor to Cat when applied to Grothendieck construction
  • functor composition is functorial (there's a functor $\Delta : (\mathcal C \to \mathcal D) \to (\mathcal D \to \mathcal E) \to (\mathcal C \to \mathcal E)$, where each $\mathcal A \to \mathcal B$ is a functor category)
  • Kan extensions are adjoints to the functorial composition functor
  • (co)limits defined as Kan extensions when one of the categories is terminal
  • The comma functor $\left(\mathcal C^{\mathcal A}\right)^{\text{op}} \times \mathcal C^{\mathcal B} \to \text{Cat}_{/ \mathcal A \times \mathcal B}$ which sends $\mathcal A \xrightarrow{f} \mathcal C \xleftarrow{g} \mathcal B$ to the comma category $(f / g)$ and it's projection functor to $\mathcal A \times \mathcal B$
  • monoidal categories (porting from the oldest version still in progress)
  • enriched categories (porting from the oldest version still in progress)

Concepts currently under construction:

  • pseudonatural transformations
  • (op)lax comma categories
  • pointwise Kan extensions
  • Cartesian closed categories

Construction Choices:

  • Morphisms are dependently typed $\text{Hom}_{\mathcal C} : \text{Ob}_{\mathcal C} \to \text{Ob}_{\mathcal C} \to \text{Type}$
  • Morphisms land in Type; propositional equality is used; higher inductive types are used for quotients
  • Categories are records with no parameters and all fields
  • Based on homotopy type theory; morphisms are hSets (0-truncated; satisfy UIP)

The article Univalent categories and the Rezk completion by Benedikt Ahrens, Chris Kapulkin, Michael Shulman has two versions:

The code is a part of the UniMath library, the original repository being now considered as obsolete.

The library includes:

  • precategories
  • isomorphisms in precategories
  • functors and natural transformations
  • various properties of functors
  • sub-precategories
  • image factorization of a functor
  • a full subprecategory of a category is a category
  • definition of adjunction
  • adjoint equivalence of precategories
  • proof that an adjoint equivalence of categories yields a weak equivalence of objects
  • a fully faithful and essentially surjective functor induces equivalence of precategories if its source is a category
  • definition of the precategory of sets
  • proof that it is a category
  • definition of Yoneda embedding
  • proof that it is fully faithful
  • definition of whiskering
  • precomposition with a fully faithful and essentially surjective functor yields a fully faithful functor
  • precomposition with a fully faithful and essentially surjective functor yields an essentially surjective functor
  • Rezk completion

There is a development of univalent categories (categories in which the type of isomorphisms is equivalent to the path-equalities) in Homotopy Type Theory in Lean 2.

It contains, among other things

  • Adjoint functors
  • Equivalences and isomorphisms of categories, including exponential laws.
  • The Yoneda embedding and Yoneda Lemma
  • limits and colimits in a category
    • The Yoneda embedding preserves limits
    • (co)limits exist in a functor category
    • The limit functor is right adjoint to the diagonal
    • The category of sets is complete and cocomplete
  • Various constructions of categories, including the comma category, functor category, (2-)pushout of categories, fundamental groupoid, Rezk completion

The development is by Jakob von Raumer and Floris van Doorn and can be found here.

http://afp.sourceforge.net/entries/Category2.shtml

"... a development of Category Theory in Isabelle/HOL. A Category is defined using records and locales. Functors and Natural Transformations are also defined. The main result that has been formalized is that the Yoneda functor is a full and faithful embedding. We also formalize the completeness of many sorted monadic equational logic." by Alexander Katovsky

According to an archived email thread,

Category theory has been formalized in MIZAR in the following verified articles.

Category theory has been formalized in MIZAR in the following verified articles.

Ingo Dahn
55. CAT_1
Introduction to Categories and Functors
by Czes{\l}aw Byli\'nski
Received October 25, 1989

102. CAT_2
Subcategories and Products of Categories
by Czes{\l}aw Byli\'nski
Received May 31, 1990

217. OPPCAT_1
Opposite Categories and Contravariant Functors
by Czes\l aw Byli\'nski
Received February 13, 1991

225. NATTRA_1
Natural Transformations. Discrete Categories
by Andrzej Trybulec
Received May 15, 1991

236. ENS_1
Category Ens
by Czes{\l}aw Byli\'nski
Received August 1, 1991

241. GRCAT_1
Categories of Groups
by Michal Muzalewski
Received October 3, 1991

252. ISOCAT_1
Isomorphisms of Categories
by Andrzej Trybulec
Received November 22, 1991

254. RINGCAT1
Category of Rings
by Micha{\l} Muzalewski
Received December 5, 1991

255. MODCAT_1
Category of Left Modules
by Micha{\l} Muzalewski
Received December 12, 1991

265. COMMACAT
Comma Category
by Grzegorz Bancerek and Agata Darmochwa\l
Received February 20, 1992

269. CAT_3
Products and Coproducts in Categories
by Czes{\l}aw Byli\'nski
Received May 11, 1992

276. ISOCAT_2
Some Isomorphisms Between Functor Categories
by Andrzej Trybulec
Received June 5, 1992

295. CAT_4
Cartesian Categories
by Czes{\l}aw Byli\'nski
Received October 27, 1992

363. CAT_5
Categorial Categories and Slice Categories
by Grzegorz Bancerek
Received October 24, 1994

379. ALTCAT_1
Categories without Uniqueness of { \bf cod } and { \bf dom } 
by Andrzej Trybulec
Received February 28, 1995

390. INDEX_1
Indexed Category
by Grzegorz Bancerek
Received June 8, 1995

Wolfram Kahl's RATH-Agda formalisation :: http://relmics.mcmaster.ca/RATH-Agda/

" The basic category and allegory theory library of the RATH-Agda project, containing (only sporadically truly) literate theories ranging from semigroupoids, which are “categories without identities”, to “action lattice categories”, which are division allegories that are at the same time Kleene categories (i.e., typed Kleene algebras), including also monoidal categories. These theories are intended as interfaces for high-level programming; this current collection includes implementations in particular using concrete relations, and a number of constructions, including quotients by (abstractions of) partial equivalence relations. "

There is an implementation of category theory in Coq by Amin Timany, hosted at github and before that bitbucket (apparently no longer updated).

Last updated: 2015-05-01 Require: Coq 8.5

It was presented at the 2015 Coq Workshop, the article, Category Theory in Coq 8.5. can be found at arXiv.

  • basic constructions:
    • terminal/initial object
    • products/sums
    • equalizers/coequalizers
    • pullbacks/pushouts
    • exponentials
      • ⊣ ∆ ⊣ × and (− × a) ⊣ a−
  • external constructions:
    • comma categories
    • product category
  • for Cat: (Obj := Category, Hom := Functor)
    • cartesian closure
    • initial object
  • for Set: (Obj := Type, Hom := fun A B ⇒ A → B)
    • initial object
    • sums
    • equalizers
    • coequalizers†
    • pullbacks
    • cartesian closure
    • local cartesian closure†
    • completeness
    • co-completeness†
    • sub-object classifier (Prop : Type)†
    • topos†
  • the Yoneda lemma
  • adjunction
    • hom-functor adjunction, unit-counit adjunction, universal morphism adjunction and their conver- sions
    • duality : F ⊣ G ⇒ Gop ⊣ F op
    • uniqueness up to natural isomorphism
  • kan extensions
    • global definition
    • local definition with both hom-functor and cones (along a functor)
    • uniqueness
    • preservation by adjoint functors
    • pointwise kan extensions (preserved by repre- sentable functors)
  • (co)limits
    • as (left)right local kan extensions along the unique functor to the terminal category
    • (sum)product-(co)equalizer (co)limits
    • pointwise (as kan extensions)
  • T − (co)algebras (for an endofunctor T )

† indicates the uses of axioms of propositional extensionality and constructive indefinite description (axiom of choice).

Alexandra Carvalho and Paulo Mateus. "Category theory in Coq." Technical report, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 1998

pdf available from Experience Implementing a Performant Category-Theory Library in Coq: Complete List of References

Adam Megacz's repo "Category Theory in Coq" based on Awodey's "Category Theory", http://www.cs.berkeley.edu/~megacz/coq-categories/

James Chapman's repo "A formalisation of Restriction Categories in Agda", https://github.com/jmchapman/restriction-categories, also contributed to by niccoloveltri

The MathClasses Coq contribution, http://coq.inria.fr/pylons/pylons/contribs/view/MathClasses/v8.4, by Robbert Krebbers, Bas Spitters, and Eelis van der Weegen

The Coq Coalgebra's contribution on "Coalgebras, bisimulation and lambda-coiteration", http://coq.inria.fr/pylons/pylons/contribs/view/Coalgebras/v8.4, by Milad Niqui

The Coq Algebra contribution (basics notions of algebra), http://coq.inria.fr/pylons/pylons/contribs/view/Algebra/v8.4, by Loïc Pottier

A subfolder of the crypto-agda Cryptographic Constructions in the Type Theory of Agda repo, https://github.com/crypto-agda/crypto-agda/tree/master/FunUniverse, by Nicolas Pouillard

The Category theory in ZFC Coq contribution, http://coq.inria.fr/pylons/pylons/contribs/view/CatsInZFC/v8.4, by Carlos Simpson

Nick Benton's Coq formalization of domain theory and ultrametric spaces is built on a basic formalization of concrete categories. Paper and code. In private correspondence, Nick said that the main interesting feature is the use of the "packed classes" pattern.

James Chapman's repo on relative monads in Agda: https://github.com/jmchapman/Relative-Monads.

James said in private correspondence that it "has lots of monad related stuff and relative monad equivalents - categories, functors, natural transformations, functor categories, monads, adjunctions, Kleisli and EM adjunctions, category of adjunctions for a monad, proof that Kleisli and EM are initial and final, + some lambda calculus related examples." It's based on a paper, and there's a draft paper about the formalization.

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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