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