+ assert ( (#((pmon_assoc (fobj23 (fobj12 a)) (fobj23 (fobj12 c)))
+ (fobj23 (fobj12 b))) >>>
+ fobj23 (fobj12 a)
+ ⋊ (
+ (#(ni_iso (fobj12 b)) >>> ( (PMF23 \ #((mf_first c) b) ))))) >>>
+ (
+ (#(ni_iso0 (fobj12 (b ⊗ c))) >>>
+ ((PMF23 \ #((mf_second a) (b ⊗ c)))))) ~~
+ ((
+ (#(ni_iso0 (fobj12 b)) >>> ( (PMF23 \ #((mf_second a) b) ))))
+ ⋉ fobj23 (fobj12 c) >>>
+ (
+ (#(ni_iso (fobj12 (a ⊗ b))) >>>
+ ( (PMF23 \ #((mf_first c) (a ⊗ b))))))) >>>
+ PMF23 \ (PMF12 \ #((pmon_assoc a c) b))
+ ).
+
+ repeat setoid_rewrite associativity.
+ setoid_rewrite (fmor_preserves_comp PMF23).
+ unfold functor_comp in *.
+ unfold functor_fobj in *.
+ simpl in *.
+ rename ni_commutes into ni_commutes7.
+ set (mf_assoc(PreMonoidalFunctor:=PMF12)) as q.
+ set (ni_commutes7 _ _ (#((mf_second a) b))) as q'.
+ simpl in q'.
+ repeat setoid_rewrite associativity.
+ symmetry.
+ setoid_rewrite <- (fmor_preserves_comp (-⋉ fobj23 (fobj12 c))).
+ repeat setoid_rewrite <- associativity.
+ setoid_rewrite juggle1.
+ setoid_rewrite <- q'.
+ repeat setoid_rewrite associativity.
+ setoid_rewrite fmor_preserves_comp.
+ idtac.
+ unfold functor_fobj in *.
+ simpl in *.
+ repeat setoid_rewrite <- associativity.
+ setoid_rewrite <- q.
+ clear q.
+ repeat setoid_rewrite <- fmor_preserves_comp.
+ repeat setoid_rewrite <- associativity.
+ apply comp_respects; try reflexivity.
+
+ set (mf_assoc(PreMonoidalFunctor:=PMF23) (fobj12 a) (fobj12 b) (fobj12 c)) as q.
+ unfold functor_fobj in *.
+ simpl in *.
+
+ rewrite H in q.
+ rewrite H0 in q.
+ simpl in q.
+ repeat setoid_rewrite <- associativity.
+ repeat setoid_rewrite <- associativity in q.
+ setoid_rewrite <- q.
+ clear q.
+ unfold functor_fobj; simpl.
+
+ repeat setoid_rewrite associativity.
+ apply comp_respects; try reflexivity.
+ apply comp_respects; try reflexivity.
+ auto.
+
+ repeat setoid_rewrite associativity.
+ repeat setoid_rewrite associativity in H1.
+ repeat setoid_rewrite <- fmor_preserves_comp in H1.
+ repeat setoid_rewrite associativity in H1.
+ apply H1.
+ Qed.
+ Implicit Arguments id [[Ob][Hom][Category]].
+
+ (* this proof is really gross; I will write a better one some other day *)
+ Instance PreMonoidalFunctorsCompose : PreMonoidalFunctor PM1 PM3 compose_mf :=