+
+Class CartesianCat `(mc:MonoidalCat) :=
+{ car_terminal : Terminal mc
+; car_one : (@one _ _ _ car_terminal) ≅ (mon_i mc)
+; car_diagonal : DiagonalCat mc
+; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell mc _))
+; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr mc _))
+; car_mn := mc
+}.
+Coercion car_diagonal : CartesianCat >-> DiagonalCat.
+Coercion car_terminal : CartesianCat >-> Terminal.
+Coercion car_mn : CartesianCat >-> MonoidalCat.
+
+Section CenterMonoidal.
+
+ Context `(mc:PreMonoidalCat(I:=pI)).
+
+ Definition CenterMonoidal_Fobj : (Center mc) ×× (Center mc) -> Center mc.
+ intro.
+ destruct X as [a b].
+ destruct a as [a apf].
+ destruct b as [b bpf].
+ exists (a ⊗ b); auto.
+ Defined.
+
+ Definition CenterMonoidal_F : Functor _ _ CenterMonoidal_Fobj.
+ admit.
+ Defined.
+
+ Definition CenterMonoidal : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I).
+ admit.
+ Defined.
+
+End CenterMonoidal.
+