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

View the Project on GitHub UniMath/UniMath


Author: Daniel R. Grayson dan@math.uiuc.edu

This package aims to formalize theorems of higher algebraic K-theory.

There used to be a lot more files here, but we moved them into other packages.

Overview of contents


Definition of the Grothendieck group of an exact category.