fact: Definition right_kan_extension_functor : Functor (C -> D) (C' -> D) := functor__of__terminal_morphism has_right_kan_extensions.
imports: Category.Core Functor.Core KanExtensions.Core Adjoint.UniversalMorphisms.Core FunctorCategory.Core Adjoint.Core