fact: Definition left_kan_extension_functor : Functor (C -> D) (C' -> D) := functor__of__initial_morphism has_left_kan_extensions.
imports: Category.Core Functor.Core KanExtensions.Core Adjoint.UniversalMorphisms.Core FunctorCategory.Core Adjoint.Core