fact: Definition left_kan_extension_adjunction : left_kan_extension_functor -| pullback_along D p := adjunction__of__initial_morphism has_left_kan_extensions.
imports: Category.Core Functor.Core KanExtensions.Core Adjoint.UniversalMorphisms.Core FunctorCategory.Core Adjoint.Core