Ktheory The files on formalization of theorems of higher algebraic K-theory that used to be here are now in UniMath.