Hint Extern 1 => apply MonoidalCat_all_central.
Coercion MonoidalCat_is_PreMonoidal : MonoidalCat >-> PreMonoidalCat.
-(*Lemma CommutativePreMonoidalCategoriesAreMonoidal `(pm:PreMonoidalCat)(cc:CommutativeCat pm) : MonoidalCat pm.*)
(* Later: generalized to premonoidal categories *)
Class DiagonalCat `(mc:MonoidalCat(F:=F)) :=
-{ copy_nt : forall a, functor_id _ ~~~> func_rlecnac a >>>> F
+{ copy_nt : forall a, functor_id _ ~~~> func_diagonal >>>> F
; 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 *)
case g as [ [g11 g12] g2];
intros; reflexivity).
Defined.
+ Definition func_diagonal : Functor C (C ×× C) (fun c => (pair_obj c c)).
+ refine {| fmor := fun a b f => @pair_mor _ _ C _ _ C (pair_obj a a) (pair_obj b b) f f |}.
+ abstract (intros; simpl; repeat split; simpl; auto).
+ abstract (intros; simpl; repeat split; simpl; auto).
+ abstract (intros; simpl; repeat split; simpl; auto).
+ Defined.
End ProductCategoryFunctors.
Section func_prod.