This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
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.
Definition of the Grothendieck group of an exact category.