From 0ecd73c172f67634fa956fb52b332e6effb5a04d Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 11 Apr 2011 04:26:55 +0000 Subject: [PATCH] add MonoidalFullSubcategory_Monoidal --- src/MonoidalCategories_ch7_8.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v index 27a7fe7..733dc5f 100644 --- a/src/MonoidalCategories_ch7_8.v +++ b/src/MonoidalCategories_ch7_8.v @@ -178,6 +178,28 @@ Section Bifunctor_from_MonoidalCat. End Bifunctor_from_MonoidalCat. +Instance MonoidalFullSubcategory_Monoidal `(mc:MonoidalCat) {Pobj} Pobj_unit Pobj_closed V + : MonoidalCat (PreMonoidalFullSubcategory_PreMonoidal(Pobj:=Pobj) mc V Pobj_unit Pobj_closed). + apply Build_MonoidalCat. + apply Build_CommutativeCat. + intros. + idtac. + apply Build_CentralMorphism; intros. + destruct a. + destruct b. + destruct c. + destruct d. + simpl. + apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=mon_commutative(MonoidalCat:=mc)) f)). + + destruct a. + destruct b. + destruct c. + destruct d. + simpl. + apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=mon_commutative(MonoidalCat:=mc)) g)). + Defined. + Class DiagonalCat `(mc:MonoidalCat) := { copy : forall (a:mc), a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a) ; copy_natural1 : forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> f ⋉ a >>> b ⋊ f ~~ f >>> copy _ -- 1.7.10.4