[Merged by Bors] - feat(CategoryTheory/Limits/KanExtension): generalize assumptions

[yuma-mizuno]

---

[joelriou]

I am obviously ok with these changes, but I think that a more significant refactor of Kan extensions should be done someday. In order to develop derived functors in the mathlib branch jriou_localization, I have sketched some API for left Kan extension in the files CategoryTheory.Functor.KanExtension and CategoryTheory.Functor.KanExtension.Pointwise in that branch https://github.com/leanprover-community/mathlib4/tree/jriou_localization . (Part of the basic definitions there are related to the definitions you introduced for bicategories; but because of universe heterogeneity, we cannot use these directly.)

[yuma-mizuno]

@joelriou Thank you for sharing your project. I'm excited to see Kan extensions and derived functors stuff in mathlib.

Should we expect the content in the current Kan extension file to be completely rewritten in some way?

[joelriou]

Should we expect the content in the current Kan extension file to be completely rewritten in some way?

I would think so, but I would try to keep a certain API compatibility...

[joelriou]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style