For some reason, category theory is often a target for formalization efforts, in particular in Coq.

This is an ongoing effort to document the growing collection of Coq category theory libraries and libraries that contain fragments of category theory. Relevant papers are also listed.

Coq-HoTT actually has two â€ścategory theory librariesâ€ť. There is also the â€śWildCatâ€ť library which is based on typeclasses and makes â€ślazyâ€ť approximations to coherence. This has been quite a useful organisational principle, but when it comes to getting some actual results out of it, we have always fallen short, mostly due to lack of time and attention. I originally tried to prove that pushouts commute with pushouts in HoTT via the standard having a right adjoint preserves colimits argument, but I couldnâ€™t pull through the coherence issues. [WIP] Adjunctions, limits, colimits in wildcats + possible progress towards 3x3 lemma for pushouts by Alizter Â· Pull Request #1571 Â· HoTT/Coq-HoTT Â· GitHub