From 06467b1762fe54767eb1d64e7b7f1798eea8cc27 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 16:41:07 -0700 Subject: [PATCH] add func_diagonal, fix naturality for DiagonalCat --- src/MonoidalCategories_ch7_8.v | 3 +-- src/ProductCategories_ch1_6_1.v | 6 ++++++ 2 files changed, 7 insertions(+), 2 deletions(-) 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. -- 1.7.10.4