For some reason, category theory is often a target for formalization efforts, in particular in Coq.

This is an ongoing effort to document the growing collection of Coq category theory libraries and libraries that contain fragments of category theory. Relevant papers are also listed.

### UniMath

### HoTT

Experience Implementing a Performant Category-Theory Library in Coq (ITP '14, arXiv version, Springer version)

### Categories

### Category theory

### Category theory in Coq

http://www.megacz.com/berkeley/coq-categories/

http://git.megacz.com/coq-categories.git

### Constructive category theory

### Category theory in ZFC

### Coalgebras in Coq

### Math Classes

### Other proof assistants

https://www.isa-afp.org/entries/Category2.html