X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FMonoidalCategories_ch7_8.v;h=733dc5f6c7df364e68c3b59e4eb5610dcb8779f1;hp=27a7fe7a934f91fe18403b9d739652f4272f551e;hb=0ecd73c172f67634fa956fb52b332e6effb5a04d;hpb=fd14c25703d15bd78088c67ff3d417d435b6b136

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 _