finish implementation of PreMonoidalFullsubcategory

[coq-categories.git] / src / MonoidalCategories_ch7_8.v

diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v
index 9033f4c..27a7fe7 100644 (file)
--- a/src/MonoidalCategories_ch7_8.v
+++ b/src/MonoidalCategories_ch7_8.v
@@ -186,7 +186,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 _))