Commit 2024-07-20 19:54 5d260610

View on Github →

feat(CategoryTheory/Localization): induction principles for (co)structured arrows (#14717) In this file, we obtain a induction principles which allow to prove properties of (co)structured arrows for a localization functor. (This shall be used in the formalization of derived functors.)

Estimated changes