-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).
+(*
+ * 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.
+
+Class MonoidalNaturalIsomorphism
+ `{C1:MonoidalCat}`{C2:MonoidalCat}
+ `(F1:!MonoidalFunctor(fobj:=fobj1) C1 C2 Func1)
+ `(F2:!MonoidalFunctor(fobj:=fobj2) C1 C2 Func2) :=
+{ mni_ni : NaturalIsomorphism F1 F2
+; mni_commutes1 : forall A B,
+ #(ni_iso (mf_first(PreMonoidalFunctor:=F1) B) A) >>> #(ni_iso mni_ni (A⊗B)) ~~
+ #(ni_iso mni_ni _) ⋉ _ >>> _ ⋊ #(ni_iso mni_ni _) >>> #(ni_iso (mf_first(PreMonoidalFunctor:=F2) B) A)
+; mni_commutes2 : forall A B,
+ #(ni_iso (mf_second(PreMonoidalFunctor:=F1) A) B) >>> #(ni_iso mni_ni (A⊗B)) ~~
+ #(ni_iso mni_ni _) ⋉ _ >>> _ ⋊ #(ni_iso mni_ni _) >>> #(ni_iso (mf_second(PreMonoidalFunctor:=F2) A) B)
+}.
+Notation "F <~~⊗~~> G" := (@MonoidalNaturalIsomorphism _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ F _ _ G) : category_scope.
+
+(* an equivalence of categories via monoidal functors, but the natural iso isn't necessarily a monoidal natural iso *)
+Structure MonoidalEquivalence `{C1:MonoidalCat} `{C2:MonoidalCat} :=
+{ meqv_forward_fobj : C1 -> C2
+; meqv_forward : Functor C1 C2 meqv_forward_fobj
+; meqv_forward_mon : PreMonoidalFunctor _ _ meqv_forward
+; meqv_backward_fobj : C2 -> C1
+; meqv_backward : Functor C2 C1 meqv_backward_fobj
+; meqv_backward_mon : PreMonoidalFunctor _ _ meqv_backward
+; meqv_comp1 : meqv_forward >>>> meqv_backward ≃ functor_id _
+; meqv_comp2 : meqv_backward >>>> meqv_forward ≃ functor_id _
+}.