X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FMonoidalCategories_ch7_8.v;h=9033f4ca84883048c0d359c9d3f15d3d2e2812d7;hp=494e7585a1fe2bc5143ae2119918785cf0b5bd4d;hb=758d0e02ca239fb9d9de3810a27290c2d5159294;hpb=77fb38900253b1bc9c4552d474f8564fda398d09 diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v index 494e758..9033f4c 100644 --- a/src/MonoidalCategories_ch7_8.v +++ b/src/MonoidalCategories_ch7_8.v @@ -1,71 +1,90 @@ Generalizable All Variables. -Require Import Preamble. +Require Import Notations. 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 ProductCategories_ch1_6_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. Require Import Coherence_ch7_8. +Require Import BinoidalCategories. +Require Import PreMonoidalCategories. (******************************************************************************) -(* Chapter 7.8: (Pre)Monoidal Categories *) +(* Chapter 7.8: 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. +(* TO DO: show that the endofunctors on any given category form a monoidal category *) -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 ⋉ _) +(* + * 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 _ }. -(* 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 +(* a monoidally-natural equivalence of categories *) +(* +Structure MonoidalNaturalEquivalence `{C1:MonoidalCat} `{C2:MonoidalCat} := +{ mneqv_forward_fobj : C1 -> C2 +; mneqv_forward : Functor C1 C2 mneqv_forward_fobj +; mneqv_forward_mon : PreMonoidalFunctor _ _ mneqv_forward +; mneqv_backward_fobj : C2 -> C1 +; mneqv_backward : Functor C2 C1 mneqv_backward_fobj +; mneqv_backward_mon : PreMonoidalFunctor _ _ mneqv_backward +; mneqv_comp1 : mneqv_forward_mon >>⊗>> mneqv_backward_mon <~~⊗~~> premonoidal_id _ +; mneqv_comp2 : mneqv_backward_mon >>⊗>> mneqv_forward_mon <~~⊗~~> premonoidal_id _ }. -Notation "f × g" := (commutative_morprod f g). +*) Section BinoidalCat_from_Bifunctor. Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj). @@ -96,8 +115,7 @@ Section BinoidalCat_from_Bifunctor. |}. Defined. - (* - Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat (BinoidalCat_from_Bifunctor F). + Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat BinoidalCat_from_Bifunctor. 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 ]; @@ -106,351 +124,74 @@ Section BinoidalCat_from_Bifunctor. [ 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 *) + (* if this binoidal structure has all of the natural isomorphisms of a premonoidal category, then it's monoidal *) + Context {pmI}(pm:PreMonoidalCat BinoidalCat_from_Bifunctor pmI). -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 *) -}. - -(* 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)) -}. + Instance PreMonoidalCat_from_bifunctor_is_Monoidal : MonoidalCat pm := + { mon_commutative := Bifunctors_Create_Commutative_Binoidal_Categories + }. -(* FIXME: show that the endofunctors on any given category form a monoidal category *) +End BinoidalCat_from_Bifunctor. -(* 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. +(* we can go the other way: given a monoidal category, its left/right functors can be combined into a bifunctor *) +Section Bifunctor_from_MonoidalCat. 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). + Definition Bifunctor_from_MonoidalCat_fobj : M ×× M -> M. + intro x. + destruct x. + exact (bin_obj' o o0). 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. + Definition Bifunctor_from_MonoidalCat_fmor {a}{b}(f:a~~{M××M}~~>b) + : (Bifunctor_from_MonoidalCat_fobj a)~~{M}~~>(Bifunctor_from_MonoidalCat_fobj b). + destruct a; destruct b; destruct f. 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). + apply (h ⋉ _ >>> _ ⋊ h0). 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 - }. - Admitted. - -End MonoidalFunctorsCompose. + Instance Bifunctor_from_MonoidalCat : Functor (M ×× M) M Bifunctor_from_MonoidalCat_fobj := + { fmor := fun x y f => Bifunctor_from_MonoidalCat_fmor f }. + intros; simpl. + destruct a; destruct b; destruct f; destruct f'; simpl in *. + destruct H. + apply comp_respects. + apply (fmor_respects (-⋉o0)); auto. + apply (fmor_respects (o1⋊-)); auto. + intros; destruct a; simpl in *. + setoid_rewrite (fmor_preserves_id (-⋉o0)). + setoid_rewrite left_identity. + apply fmor_preserves_id. + intros; destruct a; destruct b; destruct c; destruct f; destruct g; simpl in *. + setoid_rewrite <- fmor_preserves_comp. + setoid_rewrite juggle3 at 1. + assert (CentralMorphism h1). + apply mon_commutative. + setoid_rewrite <- (centralmor_first(CentralMorphism:=H)). + setoid_rewrite <- juggle3. + reflexivity. + Defined. + +End Bifunctor_from_MonoidalCat. + + +Class DiagonalCat `(mc:MonoidalCat) := +{ copy : forall (a:mc), a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a) +; copy_natural1 : forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> f ⋉ a >>> b ⋊ f ~~ f >>> copy _ +; copy_natural2 : forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> a ⋊ f >>> f ⋉ b ~~ f >>> copy _ +(* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *) +}. Class CartesianCat `(mc:MonoidalCat) := -{ car_terminal : Terminal mc -; car_one : (@one _ _ _ car_terminal) ≅ (mon_i mc) -; 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_terminal :> TerminalObject mc pmon_I +; car_diagonal : DiagonalCat mc +; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (drop a ⋉ a) >>> (#(pmon_cancell _)) +; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ drop a) >>> (#(pmon_cancelr _)) ; car_mn := mc }. Coercion car_diagonal : CartesianCat >-> DiagonalCat. -Coercion car_terminal : CartesianCat >-> Terminal. +Coercion car_terminal : CartesianCat >-> TerminalObject. Coercion car_mn : CartesianCat >-> MonoidalCat.