Commit 2025-04-28 07:13 82734e7a
View on Github →feat(CategoryTheory): left derivability structures (#22450) Using the duality result from #22447, we dualise the notion of right derivability structure introduced in #12633 in order to formalize left derivability structures. This shall be used in order to construct left derived functors.