(p : Functor C C') : object ((C' -> D) -> (C -> D)) := Eval hnf in pullback_along_functor p.
Require Import Category.Core Functor.Core. Require Import FunctorCategory.Core. Require Import Functor.Composition.Functorial.Core. Require Import UniversalProperties.