Commit 2024-02-12 14:11 998cfc8b
View on Github →feat(CategoryTheory/Functor): pointwise left Kan extensions (#10413)
In this PR, we introduce pointwise left Kan extensions: a criteria IsPointwiseLeftKanExtension, a typeclass HasPointwiseLeftKanExtension (which asserts the existence of certain colimits) and a construction of a pointwise left Kan extension when HasPointwiseLeftKanExtension holds. We also show that pointwise left Kan extensions are left Kan extensions.