+
+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_fmor (a b:(Center mc) ×× (Center mc)) :
+ (a~~{(Center mc) ×× (Center mc)}~~>b) ->
+ ((CenterMonoidal_Fobj a)~~{Center mc}~~>(CenterMonoidal_Fobj b)).
+ destruct a as [[a1 a1'] [a2 a2']].
+ destruct b as [[b1 b1'] [b2 b2']].
+ intro f.
+ destruct f as [[f1 f1'] [f2 f2']].
+ simpl in *.
+ unfold hom.
+ simpl.
+ exists (f1 ⋉ a2 >>> b1 ⋊ f2).
+ apply central_morphisms_compose.
+ admit.
+ admit.
+ Defined.
+
+ Definition CenterMonoidal_F : Functor _ _ CenterMonoidal_Fobj.
+ refine {| fmor := CenterMonoidal_F_fmor |}.
+ intros.
+ destruct a as [[a1 a1'] [a2 a2']].
+ destruct b as [[b1 b1'] [b2 b2']].
+ destruct f as [[f1 f1'] [f2 f2']].
+ destruct f' as [[g1 g1'] [g2 g2']].
+ simpl in *.
+ destruct H.
+ apply comp_respects.
+ set (fmor_respects(-⋉a2)) as q; apply q; auto.
+ set (fmor_respects(b1⋊-)) as q; apply q; auto.
+ intros.
+ destruct a as [[a1 a1'] [a2 a2']].
+ simpl in *.
+ setoid_rewrite (fmor_preserves_id (-⋉a2)).
+ setoid_rewrite (fmor_preserves_id (a1⋊-)).
+ apply left_identity.
+ intros.
+ destruct a as [[a1 a1'] [a2 a2']].
+ destruct b as [[b1 b1'] [b2 b2']].
+ destruct c as [[c1 c1'] [c2 c2']].
+ destruct f as [[f1 f1'] [f2 f2']].
+ destruct g as [[g1 g1'] [g2 g2']].
+ simpl in *.
+ setoid_rewrite juggle3.
+ setoid_rewrite <- (centralmor_first(CentralMorphism:=g1')).
+ setoid_rewrite <- juggle3.
+ setoid_rewrite <- fmor_preserves_comp.
+ reflexivity.
+ Defined.
+
+ Definition CenterMonoidal : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I).
+ admit.
+ Defined.
+
+End CenterMonoidal.
+