compose_functor' : object ((D -> E) -> ((C -> D) -> (C -> E))) := ExponentialLaws.
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.