(p : Functor C C') (h : Functor C D) := @IsInitialMorphism (_ -> _) _ h (pullback_along p).
Require Import Category.Core Functor.Core. Require Import FunctorCategory.Core. Require Import Functor.Composition.Functorial.Core. Require Import UniversalProperties.