From: Adam Megacz Date: Sat, 2 Apr 2011 22:48:40 +0000 (-0700) Subject: split MonoidalCategories into Binoidal and PreMonoidal X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=commitdiff_plain;h=21607813788d83fb58ce128df442a4ee3edfbdaf;hp=84949606d80f30b1a7ada10f46ae13bdf17cacc2 split MonoidalCategories into Binoidal and PreMonoidal --- diff --git a/src/BinoidalCategories.v b/src/BinoidalCategories.v new file mode 100644 index 0000000..ff08c3d --- /dev/null +++ b/src/BinoidalCategories.v @@ -0,0 +1,78 @@ +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 Subcategories_ch7_1. + +(******************************************************************************) +(* Binoidal Categories (not in Awodey) *) +(******************************************************************************) + +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 ⋉ _) +}. + +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. + 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. diff --git a/src/Enrichment_ch2_8.v b/src/Enrichment_ch2_8.v index b821599..84cc674 100644 --- a/src/Enrichment_ch2_8.v +++ b/src/Enrichment_ch2_8.v @@ -10,6 +10,8 @@ Require Import Subcategories_ch7_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. Require Import Coherence_ch7_8. +Require Import BinoidalCategories. +Require Import PreMonoidalCategories. Require Import MonoidalCategories_ch7_8. (******************************************************************************) diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v index 2872b1f..d30346e 100644 --- a/src/MonoidalCategories_ch7_8.v +++ b/src/MonoidalCategories_ch7_8.v @@ -9,194 +9,13 @@ Require Import Subcategories_ch7_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. - -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 ⋉ _) -}. - -Lemma central_morphisms_compose `{bc:BinoidalCat}{a b c}(f:a~>b)(g:b~>c) - : CentralMorphism f -> CentralMorphism g -> CentralMorphism (f >>> g). - intros. - apply Build_CentralMorphism; intros. - 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. - -(* 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). - apply central_morphisms_compose; auto. - 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. - 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. - -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_niso : forall a, bin_first a <~~~> bin_second a -; br_swap := fun a b => ni_iso (br_niso 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 _ _)⁻¹ -}. - -(* 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 @@ -220,10 +39,82 @@ Implicit Arguments mon_i [Ob Hom C Fobj F I]. Implicit Arguments mon_c [Ob Hom C Fobj F I]. Implicit Arguments MonoidalCat [Ob Hom ]. +(* 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. + Defined. + + 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. + 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. @@ -379,77 +270,6 @@ Class DiagonalCat `(mc:MonoidalCat(F:=F)) := (* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *) }. -(* 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. - Defined. - - 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. - Class CartesianCat `(mc:MonoidalCat) := { car_terminal : Terminal mc ; car_one : (@one _ _ _ car_terminal) ≅ (mon_i mc) @@ -461,70 +281,3 @@ Class CartesianCat `(mc:MonoidalCat) := Coercion car_diagonal : CartesianCat >-> DiagonalCat. Coercion car_terminal : CartesianCat >-> Terminal. Coercion car_mn : CartesianCat >-> MonoidalCat. - -Section CenterMonoidal. - - Context `(mc:PreMonoidalCat(I:=pI)). - - Definition CenterMonoidal_Fobj : (Center mc) ×× (Center mc) -> Center mc. - intro. - destruct X as [a b]. - destruct a as [a apf]. - destruct b as [b bpf]. - exists (a ⊗ b); auto. - Defined. - - Definition CenterMonoidal_F_fmor (a b:(Center mc) ×× (Center mc)) : - (a~~{(Center mc) ×× (Center mc)}~~>b) -> - ((CenterMonoidal_Fobj a)~~{Center mc}~~>(CenterMonoidal_Fobj b)). - destruct a as [[a1 a1'] [a2 a2']]. - destruct b as [[b1 b1'] [b2 b2']]. - intro f. - destruct f as [[f1 f1'] [f2 f2']]. - simpl in *. - unfold hom. - simpl. - exists (f1 ⋉ a2 >>> b1 ⋊ f2). - apply central_morphisms_compose. - admit. - admit. - Defined. - - Definition CenterMonoidal_F : Functor _ _ CenterMonoidal_Fobj. - refine {| fmor := CenterMonoidal_F_fmor |}. - intros. - destruct a as [[a1 a1'] [a2 a2']]. - destruct b as [[b1 b1'] [b2 b2']]. - destruct f as [[f1 f1'] [f2 f2']]. - destruct f' as [[g1 g1'] [g2 g2']]. - simpl in *. - destruct H. - apply comp_respects. - set (fmor_respects(-⋉a2)) as q; apply q; auto. - set (fmor_respects(b1⋊-)) as q; apply q; auto. - intros. - destruct a as [[a1 a1'] [a2 a2']]. - simpl in *. - setoid_rewrite (fmor_preserves_id (-⋉a2)). - setoid_rewrite (fmor_preserves_id (a1⋊-)). - apply left_identity. - intros. - destruct a as [[a1 a1'] [a2 a2']]. - destruct b as [[b1 b1'] [b2 b2']]. - destruct c as [[c1 c1'] [c2 c2']]. - destruct f as [[f1 f1'] [f2 f2']]. - destruct g as [[g1 g1'] [g2 g2']]. - simpl in *. - setoid_rewrite juggle3. - setoid_rewrite <- (centralmor_first(CentralMorphism:=g1')). - setoid_rewrite <- juggle3. - setoid_rewrite <- fmor_preserves_comp. - reflexivity. - Defined. - - Definition CenterMonoidal : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I). - admit. - Defined. - -End CenterMonoidal. - diff --git a/src/PreMonoidalCategories.v b/src/PreMonoidalCategories.v new file mode 100644 index 0000000..7d9699b --- /dev/null +++ b/src/PreMonoidalCategories.v @@ -0,0 +1,92 @@ +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. +Require Import BinoidalCategories. + +(* 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. + +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_niso : forall a, bin_first a <~~~> bin_second a +; br_swap := fun a b => ni_iso (br_niso 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 _ _)⁻¹ +}. diff --git a/src/PreMonoidalCenter.v b/src/PreMonoidalCenter.v new file mode 100644 index 0000000..61b9372 --- /dev/null +++ b/src/PreMonoidalCenter.v @@ -0,0 +1,417 @@ +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. +Require Import BinoidalCategories. +Require Import PreMonoidalCategories. +Require Import MonoidalCategories_ch_7_8. + +(******************************************************************************) +(* Facts about the center of a Binoidal or PreMonoidal Category *) +(******************************************************************************) + +Lemma central_morphisms_compose `{bc:BinoidalCat}{a b c}(f:a~>b)(g:b~>c) + : CentralMorphism f -> CentralMorphism g -> CentralMorphism (f >>> g). + intros. + apply Build_CentralMorphism; intros. + 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. + +(* 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). + apply central_morphisms_compose; auto. + Qed. + + +Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (f ⋉ c). + intro cm. + apply Build_CentralMorphism; simpl; intros. + + set (ni_commutes (pmon_assoc_rr c c0) f) as q. + apply iso_shift_right' in q. + unfold fmor in q at 1; simpl in q. + rewrite q. + clear q. + + set (ni_commutes (pmon_assoc_rr c d) f) as q. + apply iso_shift_right' in q. + unfold fmor in q at 1; simpl in q. + rewrite q. + clear q. + + set (ni_commutes (pmon_assoc_ll b c) g) as q. + apply symmetry in q. + apply iso_shift_left' in q. + rewrite q. + clear q. + + setoid_rewrite pmon_coherent_r at 1. + setoid_rewrite pmon_coherent_l at 1. + setoid_rewrite juggle3. + setoid_rewrite juggle3. + set (@iso_comp2 _ _ _ _ _ ((pmon_assoc C b c0) c)) as q. + setoid_rewrite q. + clear q. + setoid_rewrite right_identity. + unfold fmor at 2. + simpl. + setoid_rewrite (centralmor_first(CentralMorphism:=cm)). + + repeat setoid_rewrite <- associativity. + apply comp_respects. + apply comp_respects; [ idtac | reflexivity ]. + set (ni_commutes (pmon_assoc_ll a c) g) as q. + apply symmetry in q. + apply iso_shift_left' in q. + setoid_rewrite q. + clear q. + repeat setoid_rewrite associativity. + setoid_rewrite pmon_coherent_l. + set (pmon_coherent_l(PreMonoidalCat:=C) c a d) as q. + apply isos_forward_equal_then_backward_equal in q. + setoid_rewrite q. + clear q. + setoid_rewrite <- pmon_coherent_r. + setoid_rewrite iso_comp1. + setoid_rewrite right_identity. + unfold fmor at 3; simpl. + apply comp_respects; [ idtac | reflexivity ]. + + set (pmon_coherent_r a c c0) as q. + apply isos_forward_equal_then_backward_equal in q. + setoid_rewrite iso_inv_inv in q. + apply q. + + setoid_rewrite pmon_coherent_r. + unfold iso_inv. + simpl. + set (@isos_forward_equal_then_backward_equal) as q. + unfold iso_inv in q; simpl in q. + apply q. + apply pmon_coherent_l. + + (* *) + + set (ni_commutes (pmon_assoc_rr a c) g) as q. + symmetry in q. + apply iso_shift_left' in q. + unfold fmor in q at 2. + simpl in q. + setoid_rewrite q. + clear q. + + set (ni_commutes (pmon_assoc _ d c) f) as q. + apply iso_shift_right' in q. + unfold fmor in q at 1; simpl in q. + rewrite q. + clear q. + + set (pmon_coherent_r d a c) as q. + apply isos_forward_equal_then_backward_equal in q. + rewrite iso_inv_inv in q. + unfold iso_inv in q; simpl in q. + rewrite q. + clear q. + + setoid_rewrite juggle3. + setoid_rewrite (iso_comp1 ((pmon_assoc C d c) a)). + setoid_rewrite right_identity. + + set (ni_commutes (pmon_assoc_rr b c) g) as q. + symmetry in q. + apply iso_shift_left' in q. + unfold fmor in q at 2. + simpl in q. + setoid_rewrite q. + clear q. + + set (ni_commutes (pmon_assoc _ c0 c) f) as q. + unfold fmor in q; simpl in q. + apply iso_shift_right' in q. + rewrite q. + clear q. + + set (pmon_coherent_r c0 b c) as q. + rewrite q. + clear q. + + setoid_rewrite juggle3. + setoid_rewrite juggle3. + setoid_rewrite (iso_comp1 ((pmon_assoc C c0 c) b)). + setoid_rewrite right_identity. + + setoid_rewrite pmon_coherent_r. + repeat setoid_rewrite associativity. + apply comp_respects; [ reflexivity | idtac ]. + repeat setoid_rewrite <- associativity. + apply comp_respects. + setoid_rewrite (fmor_preserves_comp (-⋉c)). + apply (fmor_respects (-⋉c)). + apply centralmor_second. + set (pmon_coherent_r d b c) as q. + apply isos_forward_equal_then_backward_equal in q. + rewrite iso_inv_inv in q. + symmetry. + apply q. + Qed. + +Lemma second_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (c ⋊ f). + intro cm. + apply Build_CentralMorphism; simpl; intros. + + set (ni_commutes (pmon_assoc_ll c a) g) as q. + symmetry in q. + apply iso_shift_left' in q. + unfold fmor in q at 2. + simpl in q. + setoid_rewrite q. + clear q. + + set (ni_commutes (pmon_assoc _ c d) f) as q. + apply symmetry in q. + apply iso_shift_left' in q. + unfold fmor in q at 1; simpl in q. + rewrite q. + clear q. + + rewrite <- pmon_coherent_l. + setoid_rewrite <- associativity. + setoid_rewrite juggle3. + set (iso_comp2 ((pmon_assoc_ll c a) d)) as q. + setoid_rewrite q. + setoid_rewrite right_identity. + clear q. + + set (ni_commutes (pmon_assoc_ll c b) g) as q. + apply symmetry in q. + apply iso_shift_left' in q. + unfold fmor in q at 1; simpl in q. + setoid_rewrite q. + clear q. + + set (ni_commutes (pmon_assoc _ c c0) f) as q. + unfold fmor in q; simpl in q. + symmetry in q. + apply iso_shift_left' in q. + rewrite q. + clear q. + + rewrite pmon_coherent_l. + setoid_rewrite <- associativity. + setoid_rewrite juggle3. + set (iso_comp2 ((pmon_assoc _ c c0) b)) as q. + setoid_rewrite q. + setoid_rewrite right_identity. + clear q. + setoid_rewrite pmon_coherent_l. + + repeat setoid_rewrite associativity. + apply comp_respects; [ reflexivity | idtac ]. + repeat setoid_rewrite <- associativity. + apply comp_respects. + setoid_rewrite (fmor_preserves_comp (c⋊-)). + apply (fmor_respects (c⋊-)). + apply centralmor_first. + set (pmon_coherent_l b c d) as q. + apply isos_forward_equal_then_backward_equal in q. + apply q. + + (* *) + set (ni_commutes (pmon_assoc_ll d c) f) as q. + apply iso_shift_right' in q. + unfold fmor in q at 1; simpl in q. + rewrite q. + clear q. + + set (ni_commutes (pmon_assoc_rr c a) g) as q. + apply symmetry in q. + unfold fmor in q at 2; simpl in q. + apply iso_shift_left' in q. + rewrite q. + clear q. + + setoid_rewrite juggle3. + set (pmon_coherent_r d c a) as q. + apply isos_forward_equal_then_backward_equal in q. + setoid_rewrite iso_inv_inv in q. + setoid_rewrite q. + clear q. + setoid_rewrite <- pmon_coherent_l. + set (iso_comp1 (((pmon_assoc_ll d c) a))) as q. + setoid_rewrite q. + clear q. + setoid_rewrite right_identity. + setoid_rewrite juggle3. + setoid_rewrite (centralmor_second(CentralMorphism:=cm)). + symmetry. + apply iso_shift_left. + setoid_rewrite pmon_coherent_r. + set (pmon_coherent_l c d b) as q. + apply isos_forward_equal_then_backward_equal in q. + setoid_rewrite q. + clear q. + apply iso_shift_right. + setoid_rewrite iso_inv_inv. + repeat setoid_rewrite <- associativity. + + set (ni_commutes (pmon_assoc_ll c0 c) f) as x. + setoid_rewrite <- pmon_coherent_l. + symmetry in x. + unfold fmor in x at 2; simpl in x. + setoid_rewrite <- x. + clear x. + + set (ni_commutes (pmon_assoc_rr c b) g) as x. + symmetry in x. + unfold fmor in x at 2; simpl in x. + setoid_rewrite pmon_coherent_l. + setoid_rewrite <- pmon_coherent_r. + repeat setoid_rewrite associativity. + setoid_rewrite x. + clear x. + setoid_rewrite <- associativity. + setoid_rewrite juggle3. + setoid_rewrite pmon_coherent_r. + set (iso_comp1 ((pmon_assoc C c0 b) c)) as x. + setoid_rewrite x. + clear x. + setoid_rewrite right_identity. + reflexivity. + Qed. + +Section CenterMonoidal. + + Context `(mc:PreMonoidalCat(I:=pI)). + + Definition CenterMonoidal_Fobj : (Center mc) ×× (Center mc) -> Center mc. + intro. + destruct X as [a b]. + destruct a as [a apf]. + destruct b as [b bpf]. + exists (a ⊗ b); auto. + Defined. + + Definition CenterMonoidal_F_fmor (a b:(Center mc) ×× (Center mc)) : + (a~~{(Center mc) ×× (Center mc)}~~>b) -> + ((CenterMonoidal_Fobj a)~~{Center mc}~~>(CenterMonoidal_Fobj b)). + destruct a as [[a1 a1'] [a2 a2']]. + destruct b as [[b1 b1'] [b2 b2']]. + intro f. + destruct f as [[f1 f1'] [f2 f2']]. + simpl in *. + unfold hom. + simpl. + exists (f1 ⋉ a2 >>> b1 ⋊ f2). + apply central_morphisms_compose. + apply first_preserves_centrality; auto. + apply second_preserves_centrality; auto. + Defined. + + Definition CenterMonoidal_F : Functor _ _ CenterMonoidal_Fobj. + refine {| fmor := CenterMonoidal_F_fmor |}. + intros. + destruct a as [[a1 a1'] [a2 a2']]. + destruct b as [[b1 b1'] [b2 b2']]. + destruct f as [[f1 f1'] [f2 f2']]. + destruct f' as [[g1 g1'] [g2 g2']]. + simpl in *. + destruct H. + apply comp_respects. + set (fmor_respects(-⋉a2)) as q; apply q; auto. + set (fmor_respects(b1⋊-)) as q; apply q; auto. + intros. + destruct a as [[a1 a1'] [a2 a2']]. + simpl in *. + setoid_rewrite (fmor_preserves_id (-⋉a2)). + setoid_rewrite (fmor_preserves_id (a1⋊-)). + apply left_identity. + intros. + destruct a as [[a1 a1'] [a2 a2']]. + destruct b as [[b1 b1'] [b2 b2']]. + destruct c as [[c1 c1'] [c2 c2']]. + destruct f as [[f1 f1'] [f2 f2']]. + destruct g as [[g1 g1'] [g2 g2']]. + simpl in *. + setoid_rewrite juggle3. + setoid_rewrite <- (centralmor_first(CentralMorphism:=g1')). + setoid_rewrite <- juggle3. + setoid_rewrite <- fmor_preserves_comp. + reflexivity. + Defined. + + Definition center_I : Center mc := exist _ pI I. + + Definition center_cancelr : (func_rlecnac center_I >>>> CenterMonoidal_F) <~~~> functor_id (Center mc). + Definition center_cancelr_niso : ∀A : Center mc, CenterMonoidal_Fobj (pair_obj A center_I) ≅ A. + intros. + destruct A; simpl. + set (ni_iso (pmon_cancelr mc) x) as q. + (*refine {| iso_forward := #q ; iso_backward := iso_backward q |}.*) + admit. + Defined. + refine {| ni_iso := center_cancelr_niso |}. + admit. + Defined. + + Definition center_cancell : (func_llecnac center_I >>>> CenterMonoidal_F) <~~~> functor_id (Center mc). + Definition center_cancell_niso : ∀A : Center mc, CenterMonoidal_Fobj (pair_obj center_I A) ≅ A. + admit. + Defined. + refine {| ni_iso := center_cancell_niso |}. + admit. + Defined. + + Definition center_assoc : + ((CenterMonoidal_F **** (functor_id _)) >>>> CenterMonoidal_F) + <~~~> func_cossa >>>> ((((functor_id _) **** CenterMonoidal_F) >>>> CenterMonoidal_F)). + + Definition center_assoc_niso : ∀A : (Center mc ×× Center mc) ×× Center mc, + ((((CenterMonoidal_F **** (functor_id _)) >>>> CenterMonoidal_F) A)) + ≅ ((func_cossa >>>> ((((functor_id _) **** CenterMonoidal_F) >>>> CenterMonoidal_F))) A). + admit. + Defined. + + refine {| ni_iso := center_assoc_niso |}. + admit. + Defined. + + Instance CenterMonoidal : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I) := + { mon_cancelr := center_cancelr + ; mon_cancell := center_cancell + ; mon_assoc := center_assoc + }. + admit. + admit. + Defined. + +End CenterMonoidal. diff --git a/src/RepresentableStructure_ch7_2.v b/src/RepresentableStructure_ch7_2.v index dfd04b5..f318c7c 100644 --- a/src/RepresentableStructure_ch7_2.v +++ b/src/RepresentableStructure_ch7_2.v @@ -16,6 +16,9 @@ Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. +Require Import BinoidalCategories. +Require Import PreMonoidalCategories. +Require Import MonoidalCategories_ch7_8. Section RepresentableStructure. Context `(ec:ECategory(mn:=mn)(V:=V)).