X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FMonoidalCategories_ch7_8.v;fp=src%2FMonoidalCategories_ch7_8.v;h=27a7fe7a934f91fe18403b9d739652f4272f551e;hp=9033f4ca84883048c0d359c9d3f15d3d2e2812d7;hb=2594faf30b5d3e44380460c937023556322324c7;hpb=105a7461c7531f8b4e49f34e7242021ac6bb5ebe

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