A category theory library built on top of Homotopy Type Theory, based primarily on https://bitbucket.org/JasonGross/catdb, with some inspiration from https://github.com/benediktahrens/Foundations/tree/typesystems.
Documentation generated by coqdoc can be found at http://jasongross.github.io/HoTT-categories/coqdoc-html/; you probably want to start with the documentation for Categories.