Commit 2024-02-08 08:31 a1d9afe7
View on Github →feat(CategoryTheory/Functor): definition of Kan extensions (#10195)
This PR introduces basic definitions for Kan extensions of functors. It prepares for future development of derived functors and a refactor of the file CategoryTheory.Limits.KanExtension
.