- 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.
+(*
+ * Unlike Awodey, I define a monoidal category to be a premonoidal
+ * category in which all morphisms are central. This is partly to
+ * have a clean inheritance hierarchy, but also because Coq bogs down
+ * on product categories for some inexplicable reason.
+ *)
+Class MonoidalCat `(pm:PreMonoidalCat) :=
+{ mon_pm := pm
+; mon_commutative :> CommutativeCat pm
+}.
+Coercion mon_pm : MonoidalCat >-> PreMonoidalCat.
+Coercion mon_commutative : MonoidalCat >-> CommutativeCat.
+
+(* a monoidal functor is just a premonoidal functor between premonoidal categories which happen to be monoidal *)
+Definition MonoidalFunctor `(m1:MonoidalCat) `(m2:MonoidalCat) {fobj}(F:Functor m1 m2 fobj) := PreMonoidalFunctor m1 m2 F.
+
+Definition MonoidalFunctorsCompose
+ `{PM1 :MonoidalCat(C:=C1)}
+ `{PM2 :MonoidalCat(C:=C2)}
+ {fobj12:C1 -> C2 }
+ {PMFF12:Functor C1 C2 fobj12 }
+ (PMF12 :MonoidalFunctor PM1 PM2 PMFF12)
+ `{PM3 :MonoidalCat(C:=C3)}
+ {fobj23:C2 -> C3 }
+ {PMFF23:Functor C2 C3 fobj23 }
+ (PMF23 :MonoidalFunctor PM2 PM3 PMFF23)
+ := PreMonoidalFunctorsCompose PMF12 PMF23.
+
+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) ].