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