+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import InitialTerminal_ch2_2.
+Require Import Subcategories_ch7_1.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import Coherence_ch7_8.
+
+(******************************************************************************)
+(* Chapter 7.8: (Pre)Monoidal Categories *)
+(******************************************************************************)
+
+Class BinoidalCat
+`( C : Category )
+( bin_obj' : C -> C -> C ) :=
+{ bin_obj := bin_obj' where "a ⊗ b" := (bin_obj a b)
+; bin_first : forall a:C, Functor C C (fun x => x⊗a)
+; bin_second : forall a:C, Functor C C (fun x => a⊗x)
+; bin_c := C
+}.
+Coercion bin_c : BinoidalCat >-> Category.
+Notation "a ⊗ b" := (@bin_obj _ _ _ _ _ a b) : category_scope.
+Notation "C ⋊ f" := (@fmor _ _ _ _ _ _ _ (@bin_second _ _ _ _ _ C) _ _ f) : category_scope.
+Notation "g ⋉ C" := (@fmor _ _ _ _ _ _ _ (@bin_first _ _ _ _ _ C) _ _ g) : category_scope.
+Notation "C ⋊ -" := (@bin_second _ _ _ _ _ C) : category_scope.
+Notation "- ⋉ C" := (@bin_first _ _ _ _ _ C) : category_scope.
+
+Class CentralMorphism `{BinoidalCat}`(f:a~>b) : Prop :=
+{ centralmor_first : forall `(g:c~>d), (f ⋉ _ >>> _ ⋊ g) ~~ (_ ⋊ g >>> f ⋉ _)
+; centralmor_second : forall `(g:c~>d), (g ⋉ _ >>> _ ⋊ f) ~~ (_ ⋊ f >>> g ⋉ _)
+}.
+
+(* the central morphisms of a category constitute a subcategory *)
+Definition Center `(bc:BinoidalCat) : SubCategory bc (fun _ => True) (fun _ _ _ _ f => CentralMorphism f).
+ apply Build_SubCategory; intros; apply Build_CentralMorphism; intros.
+ abstract (setoid_rewrite (fmor_preserves_id(bin_first c));
+ setoid_rewrite (fmor_preserves_id(bin_first d));
+ setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
+ abstract (setoid_rewrite (fmor_preserves_id(bin_second c));
+ setoid_rewrite (fmor_preserves_id(bin_second d));
+ setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
+ abstract (setoid_rewrite <- (fmor_preserves_comp(bin_first c0));
+ setoid_rewrite associativity;
+ setoid_rewrite centralmor_first;
+ setoid_rewrite <- associativity;
+ setoid_rewrite centralmor_first;
+ setoid_rewrite associativity;
+ setoid_rewrite <- (fmor_preserves_comp(bin_first d));
+ reflexivity).
+ abstract (setoid_rewrite <- (fmor_preserves_comp(bin_second d));
+ setoid_rewrite <- associativity;
+ setoid_rewrite centralmor_second;
+ setoid_rewrite associativity;
+ setoid_rewrite centralmor_second;
+ setoid_rewrite <- associativity;
+ setoid_rewrite <- (fmor_preserves_comp(bin_second c0));
+ reflexivity).
+ Qed.
+
+Class CommutativeCat `(BinoidalCat) :=
+{ commutative_central : forall `(f:a~>b), CentralMorphism f
+; commutative_morprod := fun `(f:a~>b)`(g:a~>b) => f ⋉ _ >>> _ ⋊ g
+}.
+Notation "f × g" := (commutative_morprod f g).
+
+Section BinoidalCat_from_Bifunctor.
+ Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).
+ Definition BinoidalCat_from_Bifunctor_first (a:C) : Functor C C (fun b => Fobj (pair_obj b a)).
+ apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
+ @fmor _ _ _ _ _ _ _ F (pair_obj a0 a) (pair_obj b a) (pair_mor (pair_obj a0 a) (pair_obj b a) f (id a)))); intros; simpl;
+ [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
+ | abstract (set (fmor_preserves_id(F)) as q; apply q)
+ | abstract (etransitivity;
+ [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
+ | set (fmor_respects(F)) as q; apply q ];
+ split; simpl; auto) ].
+ Defined.
+ Definition BinoidalCat_from_Bifunctor_second (a:C) : Functor C C (fun b => Fobj (pair_obj a b)).
+ apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
+ @fmor _ _ _ _ _ _ _ F (pair_obj a a0) (pair_obj a b) (pair_mor (pair_obj a a0) (pair_obj a b) (id a) f))); intros;
+ [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
+ | abstract (set (fmor_preserves_id(F)) as q; apply q)
+ | abstract (etransitivity;
+ [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
+ | set (fmor_respects(F)) as q; apply q ];
+ split; simpl; auto) ].
+ Defined.
+
+ Definition BinoidalCat_from_Bifunctor : BinoidalCat C (fun a b => Fobj (pair_obj a b)).
+ refine {| bin_first := BinoidalCat_from_Bifunctor_first
+ ; bin_second := BinoidalCat_from_Bifunctor_second
+ |}.
+ Defined.
+
+ (*
+ Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat (BinoidalCat_from_Bifunctor F).
+ abstract (intros; apply Build_CommutativeCat; intros; apply Build_CentralMorphism; intros; simpl; (
+ etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ]; symmetry;
+ etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ];
+ apply (fmor_respects(F));
+ split;
+ [ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
+ | etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
+ Defined.
+ *)
+End BinoidalCat_from_Bifunctor.
+
+(* not in Awodey *)
+Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
+{ pmon_I := I
+; pmon_bin := bc
+; pmon_cat := C
+; pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
+; pmon_cancelr : (bin_first I) <~~~> functor_id C
+; pmon_cancell : (bin_second I) <~~~> functor_id C
+; pmon_pentagon : Pentagon (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b))
+; pmon_triangle : Triangle (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b))
+ (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
+; pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b)
+; pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
+; pmon_coherent_r : forall a c d:C, #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
+; pmon_coherent_l : forall a c d:C, #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
+}.
+(*
+ * Premonoidal categories actually have three associators (the "f"
+ * indicates the position in which the operation is natural:
+ *
+ * assoc : (A ⋊ f) ⋉ C <-> A ⋊ (f ⋉ C)
+ * assoc_rr : (f ⋉ B) ⋉ C <-> f ⋉ (B ⊗ C)
+ * assoc_ll : (A ⋊ B) ⋊ f <-> (A ⊗ B) ⋊ f
+ *
+ * Fortunately, in a monoidal category these are all the same natural
+ * isomorphism (and in any case -- monoidal or not -- the objects in
+ * the left column are all the same and the objects in the right
+ * column are all the same). This formalization assumes that is the
+ * case even for premonoidal categories with non-central maps, in
+ * order to keep the complexity manageable. I don't know much about
+ * the consequences of having them and letting them be different; you
+ * might need extra versions of the triangle/pentagon diagrams.
+ *)
+
+Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I ].
+Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I ].
+Implicit Arguments pmon_assoc [ Ob Hom C bin_obj' bc I ].
+Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
+
+(* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
+Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b
+ : #((pmon_cancelr mn) (a ⊗ b)) ~~ #((pmon_assoc mn a EI) b) >>> (a ⋊-) \ #((pmon_cancelr mn) b).
+ set (pmon_pentagon EI EI a b) as penta. unfold pmon_pentagon in penta.
+ set (pmon_triangle a b) as tria. unfold pmon_triangle in tria.
+ apply (fmor_respects(bin_second EI)) in tria.
+ set (@fmor_preserves_comp) as fpc.
+ setoid_rewrite <- fpc in tria.
+ set (ni_commutes (pmon_assoc mn a b)) as xx.
+ (* FIXME *)
+ Admitted.
+
+(* Formalized Definition 3.10 *)
+Class PreMonoidalFunctor
+`(PM1:PreMonoidalCat(C:=C1)(I:=I1))
+`(PM2:PreMonoidalCat(C:=C2)(I:=I2))
+ (fobj : C1 -> C2 ) :=
+{ mf_F :> Functor C1 C2 fobj
+; mf_preserves_i : mf_F I1 ≅ I2
+; mf_preserves_first : forall a, bin_first a >>>> mf_F <~~~> mf_F >>>> bin_first (mf_F a)
+; mf_preserves_second : forall a, bin_second a >>>> mf_F <~~~> mf_F >>>> bin_second (mf_F a)
+; mf_preserves_center : forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
+}.
+Coercion mf_F : PreMonoidalFunctor >-> Functor.
+
+(*******************************************************************************)
+(* Braided and Symmetric Categories *)
+
+Class BraidedCat `(mc:PreMonoidalCat) :=
+{ br_swap : forall a b, a⊗b ≅ b⊗a
+; triangleb : forall a:C, #(pmon_cancelr mc a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell mc a)
+; hexagon1 : forall {a b c}, #(pmon_assoc mc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc mc _ _ _)
+ ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc mc _ _ _) >>> b ⋊ #(br_swap _ _)
+; hexagon2 : forall {a b c}, #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc mc _ _ _)⁻¹
+ ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
+}.
+
+Class SymmetricCat `(bc:BraidedCat) :=
+{ symcat_swap : forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
+}.
+
+Class DiagonalCat `(BinoidalCat) :=
+{ copy : forall a, a ~> (a⊗a)
+(* copy >> swap == copy -- only necessary for non-cartesian braided diagonal categories *)
+}.
+
+Class CartesianCat `(mc:PreMonoidalCat(C:=C)) :=
+{ car_terminal : Terminal C
+; car_one : 1 ≅ pmon_I
+; car_diagonal : DiagonalCat mc
+; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) _) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell mc _))
+; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) _) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr mc _))
+; car_cat := C
+; car_mn := mc
+}.
+Coercion car_diagonal : CartesianCat >-> DiagonalCat.
+Coercion car_terminal : CartesianCat >-> Terminal.
+Coercion car_mn : CartesianCat >-> PreMonoidalCat.
+
+(* Definition 7.23 *)
+Class MonoidalCat `{C:Category}{Fobj:prod_obj C C -> C}{F:Functor (C ×× C) C Fobj}(I:C) :=
+{ mon_f := F
+; mon_i := I
+; mon_c := C
+(*; mon_bin := BinoidalCat_from_Bifunctor mon_f*)
+; mon_first := fun a b c (f:a~>b) => F \ pair_mor (pair_obj a c) (pair_obj b c) f (id c)
+; mon_second := fun a b c (f:a~>b) => F \ pair_mor (pair_obj c a) (pair_obj c b) (id c) f
+; mon_cancelr : (func_rlecnac I >>>> F) <~~~> functor_id C
+; mon_cancell : (func_llecnac I >>>> F) <~~~> functor_id C
+; mon_assoc : ((F **** (functor_id C)) >>>> F) <~~~> func_cossa >>>> ((((functor_id C) **** F) >>>> F))
+; mon_pentagon : Pentagon mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
+; mon_triangle : Triangle mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
+ (fun a => #(mon_cancell a)) (fun a => #(mon_cancelr a))
+}.
+
+(* FIXME: show that the endofunctors on any given category form a monoidal category *)
+
+(* Coq manual on coercions: ... only the oldest one is valid and the
+ * others are ignored. So the order of declaration of coercions is
+ * important. *)
+Coercion mon_c : MonoidalCat >-> Category.
+(*Coercion mon_bin : MonoidalCat >-> BinoidalCat.*)
+Coercion mon_f : MonoidalCat >-> Functor.
+Implicit Arguments mon_f [Ob Hom C Fobj F I].
+Implicit Arguments mon_i [Ob Hom C Fobj F I].
+Implicit Arguments mon_c [Ob Hom C Fobj F I].
+(*Implicit Arguments mon_bin [Ob Hom C Fobj F I].*)
+Implicit Arguments MonoidalCat [Ob Hom ].
+
+Section MonoidalCat_is_PreMonoidal.
+ Context `(M:MonoidalCat).
+ Definition mon_bin_M := BinoidalCat_from_Bifunctor (mon_f M).
+ Existing Instance mon_bin_M.
+ Lemma mon_pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a).
+ intros.
+ set (fun c => mon_assoc (pair_obj (pair_obj a c) b)) as qq.
+ simpl in qq.
+ apply Build_NaturalIsomorphism with (ni_iso:=qq).
+ abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
+ (pair_mor (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
+ (pair_mor (pair_obj a A) (pair_obj a B) (id a) f) (id b))) as qr;
+ apply qr).
+ Defined.
+
+ Lemma mon_pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b).
+ intros.
+ set (fun c:C => mon_assoc (pair_obj (pair_obj c a) b)) as qq.
+ simpl in qq.
+ apply ni_inv.
+ apply Build_NaturalIsomorphism with (ni_iso:=qq).
+ abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
+ (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
+ (pair_mor (pair_obj _ _) (pair_obj _ _) f (id a)) (id b))) as qr;
+ etransitivity; [ idtac | apply qr ];
+ apply comp_respects; try reflexivity;
+ unfold mon_f;
+ simpl;
+ apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
+ split; try reflexivity;
+ symmetry;
+ simpl;
+ set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
+ simpl in qqqq;
+ apply qqqq).
+ Defined.
+
+ Lemma mon_pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a).
+ intros.
+ set (fun c:C => mon_assoc (pair_obj (pair_obj a b) c)) as qq.
+ simpl in qq.
+ set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (Fobj (pair_obj a b) ⋊-) (b ⋊- >>>> a ⋊-)) as qqq.
+ set (qqq qq) as q'.
+ apply q'.
+ clear q'.
+ clear qqq.
+ abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
+ (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
+ (pair_mor (pair_obj _ _) (pair_obj _ _) (id a) (id b)) f)) as qr;
+ etransitivity; [ apply qr | idtac ];
+ apply comp_respects; try reflexivity;
+ unfold mon_f;
+ simpl;
+ apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
+ split; try reflexivity;
+ simpl;
+ set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
+ simpl in qqqq;
+ apply qqqq).
+ Defined.
+
+ Lemma mon_pmon_cancelr : (bin_first I0) <~~~> functor_id C.
+ set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_first I0) (functor_id C)) as qq.
+ set (mon_cancelr) as z.
+ simpl in z.
+ simpl in qq.
+ set (qq z) as zz.
+ apply zz.
+ abstract (intros;
+ set (ni_commutes mon_cancelr) as q; simpl in *;
+ apply q).
+ Defined.
+
+ Lemma mon_pmon_cancell : (bin_second I0) <~~~> functor_id C.
+ set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_second I0) (functor_id C)) as qq.
+ set (mon_cancell) as z.
+ simpl in z.
+ simpl in qq.
+ set (qq z) as zz.
+ apply zz.
+ abstract (intros;
+ set (ni_commutes mon_cancell) as q; simpl in *;
+ apply q).
+ Defined.
+
+ Lemma mon_pmon_triangle : forall a b, #(mon_pmon_cancelr a) ⋉ b ~~ #(mon_pmon_assoc _ _ _) >>> a ⋊ #(mon_pmon_cancell b).
+ intros.
+ set mon_triangle as q.
+ simpl in q.
+ apply q.
+ Qed.
+
+ Lemma mon_pmon_pentagon a b c d : (#(mon_pmon_assoc a c b ) ⋉ d) >>>
+ #(mon_pmon_assoc a d _ ) >>>
+ (a ⋊ #(mon_pmon_assoc b d c))
+ ~~ #(mon_pmon_assoc _ d c ) >>>
+ #(mon_pmon_assoc a _ b ).
+ set (@pentagon _ _ _ _ _ _ _ mon_pentagon) as x.
+ simpl in x.
+ unfold bin_obj.
+ unfold mon_first in x.
+ simpl in *.
+ apply x.
+ Qed.
+
+ Definition MonoidalCat_is_PreMonoidal : PreMonoidalCat (BinoidalCat_from_Bifunctor (mon_f M)) (mon_i M).
+ refine {| pmon_assoc := mon_pmon_assoc
+ ; pmon_cancell := mon_pmon_cancell
+ ; pmon_cancelr := mon_pmon_cancelr
+ ; pmon_triangle := {| triangle := mon_pmon_triangle |}
+ ; pmon_pentagon := {| pentagon := mon_pmon_pentagon |}
+ ; pmon_assoc_ll := mon_pmon_assoc_ll
+ ; pmon_assoc_rr := mon_pmon_assoc_rr
+ |}.
+ abstract (set (coincide mon_triangle) as qq; simpl in *; apply qq).
+ abstract (intros; simpl; reflexivity).
+ abstract (intros; simpl; reflexivity).
+ Defined.
+
+ 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.
+(*Lemma CommutativePreMonoidalCategoriesAreMonoidal `(pm:PreMonoidalCat)(cc:CommutativeCat pm) : MonoidalCat pm.*)
+
+Section MonoidalFunctor.
+ Context `(m1:MonoidalCat(C:=C1)) `(m2:MonoidalCat(C:=C2)).
+ Class MonoidalFunctor {Mobj:C1->C2} (mf_F:Functor C1 C2 Mobj) :=
+ { mf_f := mf_F where "f ⊕⊕ g" := (@fmor _ _ _ _ _ _ _ m2 _ _ (pair_mor (pair_obj _ _) (pair_obj _ _) f g))
+ ; mf_coherence : (mf_F **** mf_F) >>>> (mon_f m2) <~~~> (mon_f m1) >>>> mf_F
+ ; mf_phi := fun a b => #(mf_coherence (pair_obj a b))
+ ; mf_id : (mon_i m2) ≅ (mf_F (mon_i m1))
+ ; mf_cancelr : forall a, #(mon_cancelr(MonoidalCat:=m2) (mf_F a)) ~~
+ (id (mf_F a)) ⊕⊕ #mf_id >>> mf_phi a (mon_i _) >>> mf_F \ #(mon_cancelr a)
+ ; mf_cancell : forall b, #(mon_cancell (mf_F b)) ~~
+ #mf_id ⊕⊕ (id (mf_F b)) >>> mf_phi (mon_i _) b >>> mf_F \ #(mon_cancell b)
+ ; mf_assoc : forall a b c, (mf_phi a b) ⊕⊕ (id (mf_F c)) >>> (mf_phi _ c) >>>
+ (mf_F \ #(mon_assoc (pair_obj (pair_obj a b) c) )) ~~
+ #(mon_assoc (pair_obj (pair_obj _ _) _) ) >>>
+ (id (mf_F a)) ⊕⊕ (mf_phi b c) >>> (mf_phi a _)
+ }.
+End MonoidalFunctor.
+Coercion mf_f : MonoidalFunctor >-> Functor.
+Implicit Arguments mf_coherence [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
+Implicit Arguments mf_id [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
+
+Section MonoidalFunctorsCompose.
+ Context `(m1:MonoidalCat).
+ Context `(m2:MonoidalCat).
+ Context `(m3:MonoidalCat).
+ Context {f1obj}(f1:@Functor _ _ m1 _ _ m2 f1obj).
+ Context {f2obj}(f2:@Functor _ _ m2 _ _ m3 f2obj).
+ Context (mf1:MonoidalFunctor m1 m2 f1).
+ Context (mf2:MonoidalFunctor m2 m3 f2).
+
+ Lemma mf_compose_coherence : (f1 >>>> f2) **** (f1 >>>> f2) >>>> m3 <~~~> m1 >>>> (f1 >>>> f2).
+ set (mf_coherence mf1) as mc1.
+ set (mf_coherence mf2) as mc2.
+ set (@ni_comp) as q.
+ set (q _ _ _ _ _ _ _ ((f1 >>>> f2) **** (f1 >>>> f2) >>>> m3) _ ((f1 **** f1 >>>> m2) >>>> f2) _ (m1 >>>> (f1 >>>> f2))) as qq.
+ apply qq; clear qq; clear q.
+ apply (@ni_comp _ _ _ _ _ _ _ _ _ (f1 **** f1 >>>> (f2 **** f2 >>>> m3)) _ _).
+ apply (@ni_comp _ _ _ _ _ _ _ _ _ ((f1 **** f1 >>>> f2 **** f2) >>>> m3) _ _).
+ eapply ni_respects.
+ apply ni_prod_comp.
+ apply ni_id.
+ apply ni_associativity.
+ apply ni_inv.
+ eapply ni_comp.
+ apply (ni_associativity (f1 **** f1) m2 f2).
+ apply (ni_respects (F0:=f1 **** f1)(F1:=f1 **** f1)(G0:=(m2 >>>> f2))(G1:=(f2 **** f2 >>>> m3))).
+ apply ni_id.
+ apply ni_inv.
+ apply mc2.
+ apply ni_inv.
+ eapply ni_comp.
+ eapply ni_inv.
+ apply (ni_associativity m1 f1 f2).
+ apply ni_respects.
+ apply ni_inv.
+ apply mc1.
+ apply ni_id.
+ Qed.
+
+ Instance MonoidalFunctorsCompose : MonoidalFunctor m1 m3 (f1 >>>> f2) :=
+ { mf_id := id_comp (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
+ ; mf_coherence := mf_compose_coherence
+ }.
+ admit.
+ admit.
+ admit.
+ Defined.
+
+End MonoidalFunctorsCompose.