# Formalizations of category theory in proof assistants

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
• 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
• 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
• 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

# HoTT/HoTT Categories

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}$)

• 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
• 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

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

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

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

102. CAT_2
Subcategories and Products of Categories
by Czes{\l}aw Byli\'nski

217. OPPCAT_1
Opposite Categories and Contravariant Functors
by Czes\l aw Byli\'nski

225. NATTRA_1
Natural Transformations. Discrete Categories
by Andrzej Trybulec

236. ENS_1
Category Ens
by Czes{\l}aw Byli\'nski

241. GRCAT_1
Categories of Groups
by Michal Muzalewski

252. ISOCAT_1
Isomorphisms of Categories
by Andrzej Trybulec

254. RINGCAT1
Category of Rings
by Micha{\l} Muzalewski

255. MODCAT_1
Category of Left Modules
by Micha{\l} Muzalewski

265. COMMACAT
Comma Category
by Grzegorz Bancerek and Agata Darmochwa\l

269. CAT_3
Products and Coproducts in Categories
by Czes{\l}aw Byli\'nski

276. ISOCAT_2
Some Isomorphisms Between Functor Categories
by Andrzej Trybulec

295. CAT_4
Cartesian Categories
by Czes{\l}aw Byli\'nski

363. CAT_5
Categorial Categories and Slice Categories
by Grzegorz Bancerek

379. ALTCAT_1
Categories without Uniqueness of { \bf cod } and { \bf dom }
by Andrzej Trybulec

390. INDEX_1
Indexed Category
by Grzegorz Bancerek


Daniel Peebles' Agda repo (Categories parametrized by morphism equality, in Agda), https://github.com/copumpkin/categories, also contributed to by James Deikun, Andrea Vezzosi, James Cook, Jason Gross, Darius Jahandarie, and Ulf Norell

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

John Wiegley's Category Theory in Coq repo, https://github.com/jwiegley/category-theory

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

Paolo Capriotti's repo "Category theory and algebra", https://github.com/pcapriotti/agda-categories/, also contributed to by Ambrus Kaposi

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

Hiromi Ishii's Category Theory in Agda repo, https://github.com/konn/category-agda

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

Matthieu Sozeau's category theory in Coq repo http://mattam.org/repos/coq/cat/

Benedikt Ahrens and Régis Spadotti's work on coinductives, available at https://github.com/benediktahrens/coinductives, with source-code at https://github.com/rs-/Triangles.

Benedikt Ahrens' PhD, available on arxiv, with code at https://benedikt-ahrens.de/cgi-bin/r.cgi/coq, and a pretty-print index here.

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.