Experience Implementing a Performant Category-Theory Library in Coq.

Jason Gross, Adam Chlipala, David I. Spivak

Browse the full ITP paper archive.