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.).
 A: The article Univalent categories and the Rezk completion by Benedikt Ahrens, Chris Kapulkin, Michael Shulman has two versions:


*

*published in Mathematical Structures in Computer Science doi:10.1017/S0960129514000486,

*draft with auxiliary files,


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

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

A: 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).
A: 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
A: John Wiegley's Category Theory in Coq repo, https://github.com/jwiegley/category-theory
A: 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)

A: "Veriﬁed Computing in Homological Algebra: A Journey Exploring the Power and Limits of Dependent Type Theory" by Arnaud Spiwack
A: Paolo Capriotti's repo "Category theory and algebra", https://github.com/pcapriotti/agda-categories/, also contributed to by Ambrus Kaposi
A: Adam Megacz's repo "Category Theory in Coq" based on Awodey's "Category Theory",
http://www.cs.berkeley.edu/~megacz/coq-categories/
A: 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.
A: "Galois: a theory development project" by Peter Aczel
A: "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.

A: "Category Theory as an Extension of Martin-Lof Type Theory" by Roy Dyckhoff
A: "Automating Proofs in Category Theory" by Dexter Kozen, Christoph Kreitz, and Eva Richter, in NuPRL
A: "Towards a readable formalisation of category theory" by Greg O'Keefe in Isabelle/HOL/Isar
A: James Chapman's repo "A formalisation of Restriction Categories in Agda", 
https://github.com/jmchapman/restriction-categories, also contributed to by niccoloveltri
A: Hiromi Ishii's Category Theory in Agda repo, https://github.com/konn/category-agda
A: 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
A: 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
A: The Coq Algebra contribution (basics notions of algebra), http://coq.inria.fr/pylons/pylons/contribs/view/Algebra/v8.4, by Loïc Pottier
A: 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
A: 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.

A: The Category theory in ZFC Coq contribution, http://coq.inria.fr/pylons/pylons/contribs/view/CatsInZFC/v8.4, by Carlos Simpson
A: Matthieu Sozeau's category theory in Coq repo http://mattam.org/repos/coq/cat/
A: Benedikt Ahrens' PhD, available on arxiv, with code at https://benedikt-ahrens.de/cgi-bin/r.cgi/coq, and a pretty-print index here.
A: 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.
A: 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.
A: Ramana Kumar's "The Category of Sets in Higher-Order Logic", with source code for the HOL4 prover.
A: "Experiments in formalizing basic category theory in higher order logic and set theory" by Sten Agerholm
A: 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.

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