# Commit 2024-02-11 09:45 a7e85ccb

View on Github →feat(CategoryTheory): the typeclass Functor.HasRightKanExtension (#10384)
This PR introduces the typeclass `HasRightKanExtension L F`

which asserts the existence of a right Kan extension of a functor `F`

along `L`

. A chosen extension is obtained as `rightKanExtension L F`

.