- Lemma MonoidalCat_all_central : forall a b (f:a~~{M}~~>b), CentralMorphism f.
- intros;
- set (@fmor_preserves_comp _ _ _ _ _ _ _ M) as fc.
- apply Build_CentralMorphism;
- intros; simpl in *.
- etransitivity.
- apply fc.
- symmetry.
- etransitivity.
- apply fc.
- apply (fmor_respects M).
- simpl.
- setoid_rewrite left_identity;
- setoid_rewrite right_identity;
- split; reflexivity.
- etransitivity.
- apply fc.
- symmetry.
- etransitivity.
- apply fc.
- apply (fmor_respects M).
- simpl.
- setoid_rewrite left_identity;
- setoid_rewrite right_identity;
- split; reflexivity.
- Qed.
-
-End MonoidalCat_is_PreMonoidal.
-
-Hint Extern 1 => apply MonoidalCat_all_central.
-Coercion MonoidalCat_is_PreMonoidal : MonoidalCat >-> PreMonoidalCat.
-
-(* Later: generalize to premonoidal categories *)
-Class DiagonalCat `(mc:MonoidalCat(F:=F)) :=
-{ copy_nt : forall a, functor_id _ ~~~> func_diagonal >>>> F
-; copy : forall (a:mc), a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
- := fun a => nt_component _ _ (copy_nt a) a
+ Instance Bifunctor_from_MonoidalCat : Functor (M ×× M) M Bifunctor_from_MonoidalCat_fobj :=
+ { fmor := fun x y f => Bifunctor_from_MonoidalCat_fmor f }.
+ intros; simpl.
+ destruct a; destruct b; destruct f; destruct f'; simpl in *.
+ destruct H.
+ apply comp_respects.
+ apply (fmor_respects (-⋉o0)); auto.
+ apply (fmor_respects (o1⋊-)); auto.
+ intros; destruct a; simpl in *.
+ setoid_rewrite (fmor_preserves_id (-⋉o0)).
+ setoid_rewrite left_identity.
+ apply fmor_preserves_id.
+ intros; destruct a; destruct b; destruct c; destruct f; destruct g; simpl in *.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite juggle3 at 1.
+ assert (CentralMorphism h1).
+ apply mon_commutative.
+ setoid_rewrite <- (centralmor_first(CentralMorphism:=H)).
+ setoid_rewrite <- juggle3.
+ reflexivity.
+ Defined.
+
+End Bifunctor_from_MonoidalCat.
+
+
+Class DiagonalCat `(mc:MonoidalCat) :=
+{ copy : forall (a:mc), a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
+; copy_natural1 : forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> f ⋉ a >>> b ⋊ f ~~ f >>> copy _
+; copy_natural2 : forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> a ⋊ f >>> f ⋉ b ~~ f >>> copy _