fact: Definition compose_functor' : object ((D -> E) -> ((C -> D) -> (C -> E))) := ExponentialLaws.Law4.Functors.inverse _ _ _ (compose_functor_uncurried o ProductLaws.Swap.functor _ _)%functor.
imports: Category.Core Functor.Core NaturalTransformation.Core Functor.Composition.Core NaturalTransformation.Composition.Core Category.Prod FunctorCategory.Core NaturalTransformation.Composition.Functorial NaturalTransformation.Composition.Laws ExponentialLaws.Law4.Functors NaturalTransformation.Paths