What are the existing formalizations of category theory in proof assistants?

I'm primarily interested in public-domain code implementing category theory in a proof assistant (Coq, Agda, Isabelle/HOL, Mizar, NuPRL, Twelf, Lego, Idris, Matita, etc.), though I'm also interested in papers about formalizations of category theory in proof assistants.

I've added answers to this question for all of the papers and formalizations that I know about, and details about the constructions in my own repository as of the date of adding. In addition to adding formalizations that you don't see on here, you should feel free to add details and improve the formatting of the other entries (especially including what language the formalization is in, what category theory it covers, links to papers presenting it and/or publicly available source code, whether or not it's under active development, what the newest version of the proof assistant it compiles with is, etc.).