-(* TO DO: show that the endofunctors on any given category form a monoidal category *)
-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
- }.
- Admitted.
-
-End MonoidalFunctorsCompose.
-