X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FMonoidalCategories_ch7_8.v;h=e07d03501bcefd716498fabea645a344a26f116e;hp=56bfab3cdf7d53122a6db7b8e1deefa198b1ea61;hb=cc0b4696c2cfc23bdff6ded347478510ccf014c9;hpb=a570e264518d2509e608f830897d9908b23eb653

diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v
index 56bfab3..e07d035 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 *)
@@ -437,7 +436,10 @@ Section MonoidalFunctorsCompose.
   { mf_id        := id_comp         (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
   ; mf_coherence := mf_compose_coherence
   }.
-  Admitted.
+  admit.
+  admit.
+  admit.
+  Defined.
 
 End MonoidalFunctorsCompose.