X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FMonoidalCategories_ch7_8.v;h=733dc5f6c7df364e68c3b59e4eb5610dcb8779f1;hp=9033f4ca84883048c0d359c9d3f15d3d2e2812d7;hb=refs%2Fheads%2Fmaster;hpb=758d0e02ca239fb9d9de3810a27290c2d5159294

diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v
index 9033f4c..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 _
@@ -186,7 +208,7 @@ Class DiagonalCat `(mc:MonoidalCat) :=
 }.
 
 Class CartesianCat `(mc:MonoidalCat) :=
-{ car_terminal  :> TerminalObject mc pmon_I
+{ car_terminal  :> TerminalObject mc (pmon_I mc)
 ; car_diagonal  :  DiagonalCat mc
 ; car_law1      :  forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (drop a  ⋉ a) >>> (#(pmon_cancell _))
 ; car_law2      :  forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ drop  a) >>> (#(pmon_cancelr _))