fact: Definition IsLeftKanExtensionAlong (p : Functor C C') (h : Functor C D) := @IsInitialMorphism (_ -> _) _ h (pullback_along p).
imports: Category.Core Functor.Core FunctorCategory.Core Functor.Composition.Functorial.Core UniversalProperties