+ (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23).
+
+ Definition compose_mf := PMF12 >>>> PMF23.
+
+ Definition compose_mf_i : I3 ≅ PMF23 (PMF12 I1).
+ eapply iso_comp.
+ apply (mf_i(PreMonoidalFunctor:=PMF23)).
+ apply functors_preserve_isos.
+ apply (mf_i(PreMonoidalFunctor:=PMF12)).
+ Defined.
+
+ Definition compose_mf_first a : compose_mf >>>> bin_first (compose_mf a) <~~~> bin_first a >>>> compose_mf.
+ set (mf_first(PreMonoidalFunctor:=PMF12) a) as mf_first12.
+ set (mf_first(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_first23.
+ unfold functor_fobj in *; simpl in *.
+ unfold compose_mf.
+ eapply ni_comp.
+ apply (ni_associativity PMF12 PMF23 (- ⋉fobj23 (fobj12 a))).
+ eapply ni_comp.
+ apply (ni_respects PMF12 PMF12 (PMF23 >>>> - ⋉fobj23 (fobj12 a)) (- ⋉fobj12 a >>>> PMF23)).
+ apply ni_id.
+ apply mf_first23.
+ clear mf_first23.
+
+ eapply ni_comp.
+ eapply ni_inv.
+ apply (ni_associativity PMF12 (- ⋉fobj12 a) PMF23).
+
+ apply ni_inv.
+ eapply ni_comp.
+ eapply ni_inv.
+ eapply (ni_associativity _ PMF12 PMF23).
+
+ apply ni_respects; [ idtac | apply ni_id ].
+ apply ni_inv.
+ apply mf_first12.
+ Defined.
+
+ Definition compose_mf_second a : compose_mf >>>> bin_second (compose_mf a) <~~~> bin_second a >>>> compose_mf.
+ set (mf_second(PreMonoidalFunctor:=PMF12) a) as mf_second12.
+ set (mf_second(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_second23.
+ unfold functor_fobj in *; simpl in *.
+ unfold compose_mf.
+ eapply ni_comp.
+ apply (ni_associativity PMF12 PMF23 (fobj23 (fobj12 a) ⋊-)).
+ eapply ni_comp.
+ apply (ni_respects PMF12 PMF12 (PMF23 >>>> fobj23 (fobj12 a) ⋊-) (fobj12 a ⋊- >>>> PMF23)).
+ apply ni_id.
+ apply mf_second23.
+ clear mf_second23.
+
+ eapply ni_comp.
+ eapply ni_inv.
+ apply (ni_associativity PMF12 (fobj12 a ⋊ -) PMF23).
+
+ apply ni_inv.
+ eapply ni_comp.
+ eapply ni_inv.
+ eapply (ni_associativity (a ⋊-) PMF12 PMF23).
+
+ apply ni_respects; [ idtac | apply ni_id ].
+ apply ni_inv.
+ apply mf_second12.
+ Defined.
+
+ Lemma compose_assoc_coherence a b c :
+ (#((pmon_assoc (compose_mf a) (fobj23 (fobj12 c))) (compose_mf b)) >>>
+ compose_mf a ⋊ #((compose_mf_second b) c)) >>>
+ #((compose_mf_second a) (b ⊗ c)) ~~
+ (#((compose_mf_second a) b) ⋉ fobj23 (fobj12 c) >>>
+ #((compose_mf_second (a ⊗ b)) c)) >>> compose_mf \ #((pmon_assoc a c) b).
+(*
+ set (mf_assoc a b c) as x.
+ set (mf_assoc (fobj12 a) (fobj12 b) (fobj12 c)) as x'.
+ unfold functor_fobj in *.
+ simpl in *.
+ etransitivity.
+ etransitivity.
+ etransitivity.
+ Focus 3.
+ apply x'.
+
+ apply iso_shift_left' in x'.
+
+ unfold compose_mf_second; simpl.
+ unfold functor_fobj; simpl.
+ set (mf_second (fobj12 b)) as m.
+ assert (mf_second (fobj12 b)=m). reflexivity.
+ destruct m; simpl.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite right_identity.
+ setoid_rewrite left_identity.
+ setoid_rewrite left_identity.
+ setoid_rewrite left_identity.
+
+ set (mf_second (fobj12 (a ⊗ b))) as m''.
+ assert (mf_second (fobj12 (a ⊗ b))=m''). reflexivity.
+ destruct m''; simpl.
+ unfold functor_fobj; simpl.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite right_identity.
+ setoid_rewrite left_identity.
+ setoid_rewrite left_identity.
+ setoid_rewrite left_identity.
+
+ set (mf_second (fobj12 a)) as m'.
+ assert (mf_second (fobj12 a)=m'). reflexivity.
+ destruct m'; simpl.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite left_identity.
+ setoid_rewrite left_identity.
+ setoid_rewrite left_identity.
+ setoid_rewrite right_identity.
+ assert (fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 (b ⊗ c)) ~~ id _).
+ (* *)
+ setoid_rewrite H2.
+ setoid_rewrite left_identity.
+ assert ((id (fobj23 (fobj12 a) ⊗ fobj23 (fobj12 b)) ⋉ fobj23 (fobj12 c)) ~~ id _).
+ (* *)
+ setoid_rewrite H3.
+ setoid_rewrite left_identity.
+ assert (id (fobj23 (fobj12 a ⊗ fobj12 b)) ⋉ fobj23 (fobj12 c) ~~ id _).
+ (* *)
+ setoid_rewrite H4.
+ setoid_rewrite left_identity.
+ clear H4.
+ setoid_rewrite left_identity.
+ assert (id (fobj23 (fobj12 (a ⊗ b))) ⋉ fobj23 (fobj12 c) ~~ id _).
+ (* *)
+ setoid_rewrite H4.
+ setoid_rewrite right_identity.
+ clear H4.
+ assert ((fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 b)) ⋉ fobj23 (fobj12 c) ~~ id _).
+ (* *)
+ setoid_rewrite H4.
+ setoid_rewrite left_identity.
+ clear H4.
+ unfold functor_comp in ni_commutes0; simpl in ni_commutes0.
+ unfold functor_comp in ni_commutes; simpl in ni_commutes.
+ unfold functor_comp in ni_commutes1; simpl in ni_commutes1.
+
+
+ unfold functor_fobj in *.
+ simpl in *.
+ setoid_rewrite x in x'.
+ rewrite H1.
+ set (ni_commutes0 (a )
+ setoid_rewrite fmor_preserves_id.
+ etransitivity.
+ eapply comp_respects.
+ reflexivity.
+ eapply comp_respects.
+ eapply comp_respects.
+ apply
+ Focus 2.
+ eapply fmor_preserves_id.
+ setoid_rewrite (fmor_preserves_id PMF23).
+*)
+ admit.
+ Qed.
+
+ Instance PreMonoidalFunctorsCompose : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12) :=
+ { mf_i := compose_mf_i
+ ; mf_F := compose_mf
+ ; mf_first := compose_mf_first
+ ; mf_second := compose_mf_second }.
+ intros; unfold compose_mf_first; unfold compose_mf_second.
+ set (mf_first (PMF12 a)) as x in *.
+ set (mf_second (PMF12 b)) as y in *.
+ assert (x=mf_first (PMF12 a)). reflexivity.
+ assert (y=mf_second (PMF12 b)). reflexivity.
+ destruct x.
+ destruct y.
+ simpl.
+ repeat setoid_rewrite left_identity.
+ repeat setoid_rewrite right_identity.
+ set (mf_consistent (PMF12 a) (PMF12 b)) as later.
+ apply comp_respects; try reflexivity.
+ unfold functor_comp.
+ unfold functor_fobj; simpl.
+ set (ni_commutes _ _ (id (fobj12 b))) as x.
+ unfold functor_comp in x.
+ simpl in x.
+ unfold functor_fobj in x.
+ symmetry in x.
+ etransitivity.
+ apply x.
+ clear x.
+ set (ni_commutes0 _ _ (id (fobj12 a))) as x'.
+ unfold functor_comp in x'.
+ simpl in x'.
+ unfold functor_fobj in x'.
+ etransitivity; [ idtac | apply x' ].
+ clear x'.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite right_identity.
+ rewrite <- H in later.
+ rewrite <- H0 in later.
+ simpl in later.
+ apply later.
+ apply fmor_respects.
+ apply (mf_consistent a b).
+
+ intros.
+ simpl.
+ apply mf_center.
+ apply mf_center.
+ auto.
+
+ intros.
+ unfold compose_mf_first; simpl.
+ set (mf_first (PMF12 b)) as m.
+ assert (mf_first (PMF12 b)=m). reflexivity.
+ destruct m.
+ simpl.
+ unfold functor_fobj; simpl.
+ repeat setoid_rewrite <- fmor_preserves_comp.
+ repeat setoid_rewrite left_identity.
+ repeat setoid_rewrite right_identity.
+
+ set (mf_cancell b) as y.
+ set (mf_cancell (fobj12 b)) as y'.
+ unfold functor_fobj in *.
+ setoid_rewrite y in y'.
+ clear y.
+ setoid_rewrite <- fmor_preserves_comp in y'.
+ setoid_rewrite <- fmor_preserves_comp in y'.
+ etransitivity.
+ apply y'.
+ clear y'.
+
+ repeat setoid_rewrite <- associativity.
+ apply comp_respects; try reflexivity.
+ apply comp_respects; try reflexivity.
+ repeat setoid_rewrite associativity.
+ apply comp_respects; try reflexivity.
+
+ set (ni_commutes _ _ (id (fobj12 I1))) as x.
+ unfold functor_comp in x.
+ unfold functor_fobj in x.
+ simpl in x.
+ setoid_rewrite <- x.
+ clear x.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite right_identity.
+
+ rewrite H.
+ simpl.
+ clear H.
+ unfold functor_comp in ni_commutes.
+ simpl in ni_commutes.
+ apply ni_commutes.
+
+ intros.
+ unfold compose_mf_second; simpl.
+ set (mf_second (PMF12 a)) as m.
+ assert (mf_second (PMF12 a)=m). reflexivity.
+ destruct m.
+ simpl.
+ unfold functor_fobj; simpl.
+ repeat setoid_rewrite <- fmor_preserves_comp.
+ repeat setoid_rewrite left_identity.
+ repeat setoid_rewrite right_identity.
+
+ set (mf_cancelr a) as y.
+ set (mf_cancelr (fobj12 a)) as y'.
+ unfold functor_fobj in *.
+ setoid_rewrite y in y'.
+ clear y.
+ setoid_rewrite <- fmor_preserves_comp in y'.
+ setoid_rewrite <- fmor_preserves_comp in y'.
+ etransitivity.
+ apply y'.
+ clear y'.
+
+ repeat setoid_rewrite <- associativity.
+ apply comp_respects; try reflexivity.
+ apply comp_respects; try reflexivity.
+ repeat setoid_rewrite associativity.
+ apply comp_respects; try reflexivity.
+
+ set (ni_commutes _ _ (id (fobj12 I1))) as x.
+ unfold functor_comp in x.
+ unfold functor_fobj in x.
+ simpl in x.
+ setoid_rewrite <- x.
+ clear x.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite right_identity.
+
+ rewrite H.
+ simpl.
+ clear H.
+ unfold functor_comp in ni_commutes.
+ simpl in ni_commutes.
+ apply ni_commutes.
+
+ apply compose_assoc_coherence.
+ Defined.
+
+End PreMonoidalFunctorsCompose.
+