object ((cat^op * cat) -> cat) := Eval cbv zeta in let object_of := (fun CD => (((fst CD).
Require Import Category.Core Functor.Core FunctorCategory.Core Functor.Pointwise.Core Functor.Pointwise.Properties Category.Dual Category.Prod Cat.Core ExponentialLaws.Law4.Functors.