object ((C -> D) -> ((D -> E) -> (C -> E))). Proof. refine (Build_Functor (C -> D) ((D -> E) -> (C -> E)) (@whiskerR_functor _ _ _ _) compose_functor_morphism_of _ _); abstract ( path_natural_transformation; rewrite ?composition_of, ?identity_of; reflexivity ). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Composition.Core NaturalTransformation.Composition.Core. Require Import Category.Prod FunctorCategory.Core NaturalTransformation.Composition.Functorial NaturalTransformation.Composition.Laws ExponentialLaws.Law4.Functors. Require Import NaturalTransformation.Paths.