From: Adam Megacz <adam@megacz.com>
Date: Fri, 25 Mar 2011 23:41:07 +0000 (-0700)
Subject: add func_diagonal, fix naturality for DiagonalCat
X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=commitdiff_plain;h=06467b1762fe54767eb1d64e7b7f1798eea8cc27;hp=4a45ee99fb19018cf30a34e361816c8ba960d638

add func_diagonal, fix naturality for DiagonalCat
---

diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v
index 56bfab3..8d78f33 100644
--- a/src/MonoidalCategories_ch7_8.v
+++ b/src/MonoidalCategories_ch7_8.v
@@ -363,11 +363,10 @@ End MonoidalCat_is_PreMonoidal.
 
 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 *)
diff --git a/src/ProductCategories_ch1_6_1.v b/src/ProductCategories_ch1_6_1.v
index 697641c..29d73d4 100644
--- a/src/ProductCategories_ch1_6_1.v
+++ b/src/ProductCategories_ch1_6_1.v
@@ -126,6 +126,12 @@ Section ProductCategoryFunctors.
               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.