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 *)
{ mf_id := id_comp (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
; mf_coherence := mf_compose_coherence
}.
{ mf_id := id_comp (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
; mf_coherence := mf_compose_coherence
}.