Hint Extern 1 => apply MonoidalCat_all_central.
Coercion MonoidalCat_is_PreMonoidal : MonoidalCat >-> PreMonoidalCat.
Hint Extern 1 => apply MonoidalCat_all_central.
Coercion MonoidalCat_is_PreMonoidal : MonoidalCat >-> PreMonoidalCat.
; copy : forall (a:mc), a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
:= fun a => nt_component _ _ (copy_nt a) a
(* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)
; copy : forall (a:mc), a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
:= fun a => nt_component _ _ (copy_nt a) a
(* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)