This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

View the Project on GitHub UniMath/UniMath

Category Theory

This evolved from the package “Rezk Completion” whose authors are: Benedikt Ahrens, Chris Kapulkin, Mike Shulman

Hence, this Coq library in particular mechanizes the Rezk completion as described in http://arxiv.org/abs/1303.0584. It was written by Benedikt Ahrens, Chris Kapulkin and Mike Shulman.

It builds upon V. Voevodsky’s Foundations library, available on http://arxiv.org/abs/1401.0053.

For any question about this library, send an email to Benedikt Ahrens.


The terminology in this package differs from that of the HoTT book. The following table offers a comparison.

UniMath HoTT Book Ob C Hom_C Univalence
Precategory n/a Type Type No
Category Precategory Type Set No
Univalent/saturated category Category Type Set Yes
Set category Strict category Set Set No


The files containing the formalization of the Rezk Completion:

many more files that were not needed for the Rezk completion and that go beyond the former package “Rezk Completion”; they have various authors (see the files individually that are given in alphabetic order):

The subdirectories