fact: Definition functor : object (cat^op -> (cat -> cat)) := ExponentialLaws.Law4.Functors.inverse _ _ _ functor_uncurried.
imports: Category.Core Functor.Core FunctorCategory.Core Functor.Pointwise.Core Functor.Pointwise.Properties Category.Dual Category.Prod Cat.Core ExponentialLaws.Law4.Functors