fact: Definition right_kan_extension_adjunction : pullback_along D p -| right_kan_extension_functor := adjunction__of__terminal_morphism has_right_kan_extensions.
imports: Category.Core Functor.Core KanExtensions.Core Adjoint.UniversalMorphisms.Core FunctorCategory.Core Adjoint.Core