+ 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.
+