X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FPreMonoidalCategories.v;h=2764abde0e733059e9cec15cdbabf35fa6d5007a;hp=e56c72750ef96123175d40ce6fdfe84fe5f81965;hb=fd14c25703d15bd78088c67ff3d417d435b6b136;hpb=bce224f0a9ddd24cfe16a710b4f7d5be64b32929 diff --git a/src/PreMonoidalCategories.v b/src/PreMonoidalCategories.v index e56c727..2764abd 100644 --- a/src/PreMonoidalCategories.v +++ b/src/PreMonoidalCategories.v @@ -1,5 +1,5 @@ Generalizable All Variables. -Require Import Preamble. +Require Import Notations. Require Import Categories_ch1_3. Require Import Functors_ch1_4. Require Import Isomorphisms_ch1_5. @@ -48,6 +48,7 @@ Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) := * might need extra versions of the triangle/pentagon diagrams. *) +Implicit Arguments pmon_I [ Ob Hom C bin_obj' bc I ]. Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I PreMonoidalCat ]. Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I PreMonoidalCat ]. Implicit Arguments pmon_assoc [ Ob Hom C bin_obj' bc I PreMonoidalCat ]. @@ -145,10 +146,11 @@ Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} b a Qed. Class PreMonoidalFunctor -`(PM1:PreMonoidalCat(C:=C1)(I:=I1)) -`(PM2:PreMonoidalCat(C:=C2)(I:=I2)) - (fobj : C1 -> C2 ) := -{ mf_F :> Functor C1 C2 fobj +`(PM1 : PreMonoidalCat(C:=C1)(I:=I1)) +`(PM2 : PreMonoidalCat(C:=C2)(I:=I2)) + {fobj : C1 -> C2 } + (F : Functor C1 C2 fobj ) := +{ mf_F := F ; mf_i : I2 ≅ mf_F I1 ; mf_first : ∀ a, mf_F >>>> bin_first (mf_F a) <~~~> bin_first a >>>> mf_F ; mf_second : ∀ a, mf_F >>>> bin_second (mf_F a) <~~~> bin_second a >>>> mf_F @@ -156,8 +158,8 @@ Class PreMonoidalFunctor ; mf_center : forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f) ; mf_cancell : ∀ b, #(pmon_cancell _) ~~ #mf_i ⋉ _ >>> #(mf_first b I1) >>> mf_F \ #(pmon_cancell b) ; mf_cancelr : ∀ a, #(pmon_cancelr _) ~~ _ ⋊ #mf_i >>> #(mf_second a I1) >>> mf_F \ #(pmon_cancelr a) -; mf_assoc : ∀ a b c, #(pmon_assoc _ _ _) >>> _ ⋊ #(mf_second _ _) >>> #(mf_second _ _) ~~ - #(mf_second _ _) ⋉ _ >>> #(mf_second _ _) >>> mf_F \ #(pmon_assoc a c b) +; mf_assoc : ∀ a b c, #(pmon_assoc _ _ _) >>> _ ⋊ #(mf_first _ _) >>> #(mf_second _ _) ~~ + #(mf_second _ _) ⋉ _ >>> #(mf_first _ _) >>> mf_F \ #(pmon_assoc a c b) }. Coercion mf_F : PreMonoidalFunctor >-> Functor. @@ -166,10 +168,12 @@ Section PreMonoidalFunctorsCompose. `{PM1 :PreMonoidalCat(C:=C1)(I:=I1)} `{PM2 :PreMonoidalCat(C:=C2)(I:=I2)} {fobj12:C1 -> C2 } - (PMF12 :PreMonoidalFunctor PM1 PM2 fobj12) + {PMFF12:Functor C1 C2 fobj12 } + (PMF12 :PreMonoidalFunctor PM1 PM2 PMFF12) `{PM3 :PreMonoidalCat(C:=C3)(I:=I3)} {fobj23:C2 -> C3 } - (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23). + {PMFF23:Functor C2 C3 fobj23 } + (PMF23 :PreMonoidalFunctor PM2 PM3 PMFF23). Definition compose_mf := PMF12 >>>> PMF23. @@ -188,8 +192,7 @@ Section PreMonoidalFunctorsCompose. eapply ni_comp. apply (ni_associativity PMF12 PMF23 (- ⋉fobj23 (fobj12 a))). eapply ni_comp. - apply (ni_respects PMF12 PMF12 (PMF23 >>>> - ⋉fobj23 (fobj12 a)) (- ⋉fobj12 a >>>> PMF23)). - apply ni_id. + apply (ni_respects1 PMF12 (PMF23 >>>> - ⋉fobj23 (fobj12 a)) (- ⋉fobj12 a >>>> PMF23)). apply mf_first23. clear mf_first23. @@ -202,7 +205,7 @@ Section PreMonoidalFunctorsCompose. eapply ni_inv. eapply (ni_associativity _ PMF12 PMF23). - apply ni_respects; [ idtac | apply ni_id ]. + apply ni_respects2. apply ni_inv. apply mf_first12. Defined. @@ -215,8 +218,7 @@ Section PreMonoidalFunctorsCompose. eapply ni_comp. apply (ni_associativity PMF12 PMF23 (fobj23 (fobj12 a) ⋊-)). eapply ni_comp. - apply (ni_respects PMF12 PMF12 (PMF23 >>>> fobj23 (fobj12 a) ⋊-) (fobj12 a ⋊- >>>> PMF23)). - apply ni_id. + apply (ni_respects1 PMF12 (PMF23 >>>> fobj23 (fobj12 a) ⋊-) (fobj12 a ⋊- >>>> PMF23)). apply mf_second23. clear mf_second23. @@ -229,124 +231,128 @@ Section PreMonoidalFunctorsCompose. eapply ni_inv. eapply (ni_associativity (a ⋊-) PMF12 PMF23). - apply ni_respects; [ idtac | apply ni_id ]. + apply ni_respects2. apply ni_inv. apply mf_second12. Defined. - Lemma compose_assoc_coherence a b c : - (#((pmon_assoc (compose_mf a) (fobj23 (fobj12 c))) (compose_mf b)) >>> - compose_mf a ⋊ #((compose_mf_second b) c)) >>> + (* this proof is really gross; I will write a better one some other day *) + Lemma mf_associativity_comp : + ∀a b c : C1, + (#((pmon_assoc (compose_mf a) (compose_mf c)) (fobj23 (fobj12 b))) >>> + compose_mf a ⋊ #((compose_mf_first c) b)) >>> #((compose_mf_second a) (b ⊗ c)) ~~ - (#((compose_mf_second a) b) ⋉ fobj23 (fobj12 c) >>> - #((compose_mf_second (a ⊗ b)) c)) >>> compose_mf \ #((pmon_assoc a c) b). -(* - set (mf_assoc a b c) as x. - set (mf_assoc (fobj12 a) (fobj12 b) (fobj12 c)) as x'. - unfold functor_fobj in *. - simpl in *. - etransitivity. - etransitivity. - etransitivity. - Focus 3. - apply x'. - - apply iso_shift_left' in x'. - + (#((compose_mf_second a) b) ⋉ compose_mf c >>> + #((compose_mf_first c) (a ⊗ b))) >>> compose_mf \ #((pmon_assoc a c) b). + intros; intros. unfold compose_mf_second; simpl. + unfold compose_mf_first; simpl. + unfold functor_comp; simpl. + unfold ni_respects1. unfold functor_fobj; simpl. - set (mf_second (fobj12 b)) as m. - assert (mf_second (fobj12 b)=m). reflexivity. + + set (mf_first (fobj12 c)) as m'. + assert (mf_first (fobj12 c)=m'). reflexivity. + destruct m'; simpl. + + set (mf_second (fobj12 a)) as m. + assert (mf_second (fobj12 a)=m). reflexivity. destruct m; simpl. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite fmor_preserves_id. - setoid_rewrite fmor_preserves_id. - setoid_rewrite fmor_preserves_id. - setoid_rewrite right_identity. - setoid_rewrite left_identity. - setoid_rewrite left_identity. - setoid_rewrite left_identity. - set (mf_second (fobj12 (a ⊗ b))) as m''. - assert (mf_second (fobj12 (a ⊗ b))=m''). reflexivity. - destruct m''; simpl. - unfold functor_fobj; simpl. - setoid_rewrite fmor_preserves_id. - setoid_rewrite fmor_preserves_id. - setoid_rewrite right_identity. - setoid_rewrite left_identity. - setoid_rewrite left_identity. - setoid_rewrite left_identity. + Implicit Arguments id [[Ob][Hom][Category][a]]. + idtac. - set (mf_second (fobj12 a)) as m'. - assert (mf_second (fobj12 a)=m'). reflexivity. - destruct m'; simpl. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite left_identity. - setoid_rewrite left_identity. - setoid_rewrite left_identity. - setoid_rewrite right_identity. - assert (fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 (b ⊗ c)) ~~ id _). - (* *) - setoid_rewrite H2. - setoid_rewrite left_identity. - assert ((id (fobj23 (fobj12 a) ⊗ fobj23 (fobj12 b)) ⋉ fobj23 (fobj12 c)) ~~ id _). - (* *) - setoid_rewrite H3. - setoid_rewrite left_identity. - assert (id (fobj23 (fobj12 a ⊗ fobj12 b)) ⋉ fobj23 (fobj12 c) ~~ id _). - (* *) - setoid_rewrite H4. - setoid_rewrite left_identity. - clear H4. - setoid_rewrite left_identity. - assert (id (fobj23 (fobj12 (a ⊗ b))) ⋉ fobj23 (fobj12 c) ~~ id _). - (* *) - setoid_rewrite H4. - setoid_rewrite right_identity. - clear H4. - assert ((fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 b)) ⋉ fobj23 (fobj12 c) ~~ id _). - (* *) - setoid_rewrite H4. - setoid_rewrite left_identity. - clear H4. - unfold functor_comp in ni_commutes0; simpl in ni_commutes0. - unfold functor_comp in ni_commutes; simpl in ni_commutes. - unfold functor_comp in ni_commutes1; simpl in ni_commutes1. + symmetry. + etransitivity. + repeat setoid_rewrite <- fmor_preserves_comp. + repeat setoid_rewrite fmor_preserves_id. + repeat setoid_rewrite left_identity. + repeat setoid_rewrite right_identity. + reflexivity. + symmetry. + etransitivity. + repeat setoid_rewrite <- fmor_preserves_comp. + repeat setoid_rewrite fmor_preserves_id. + repeat setoid_rewrite left_identity. + repeat setoid_rewrite right_identity. + reflexivity. + assert ( (#((pmon_assoc (fobj23 (fobj12 a)) (fobj23 (fobj12 c))) + (fobj23 (fobj12 b))) >>> + fobj23 (fobj12 a) + ⋊ ( + (#(ni_iso (fobj12 b)) >>> ( (PMF23 \ #((mf_first c) b) ))))) >>> + ( + (#(ni_iso0 (fobj12 (b ⊗ c))) >>> + ((PMF23 \ #((mf_second a) (b ⊗ c)))))) ~~ + (( + (#(ni_iso0 (fobj12 b)) >>> ( (PMF23 \ #((mf_second a) b) )))) + ⋉ fobj23 (fobj12 c) >>> + ( + (#(ni_iso (fobj12 (a ⊗ b))) >>> + ( (PMF23 \ #((mf_first c) (a ⊗ b))))))) >>> + PMF23 \ (PMF12 \ #((pmon_assoc a c) b)) + ). + repeat setoid_rewrite associativity. + setoid_rewrite (fmor_preserves_comp PMF23). + unfold functor_comp in *. + unfold functor_fobj in *. + simpl in *. + rename ni_commutes into ni_commutes7. + set (mf_assoc(PreMonoidalFunctor:=PMF12)) as q. + set (ni_commutes7 _ _ (#((mf_second a) b))) as q'. + simpl in q'. + repeat setoid_rewrite associativity. + symmetry. + setoid_rewrite <- (fmor_preserves_comp (-⋉ fobj23 (fobj12 c))). + repeat setoid_rewrite <- associativity. + setoid_rewrite juggle1. + setoid_rewrite <- q'. + repeat setoid_rewrite associativity. + setoid_rewrite fmor_preserves_comp. + idtac. unfold functor_fobj in *. simpl in *. - setoid_rewrite x in x'. - rewrite H1. - set (ni_commutes0 (a ) - setoid_rewrite fmor_preserves_id. - etransitivity. - eapply comp_respects. - reflexivity. - eapply comp_respects. - eapply comp_respects. - apply - Focus 2. - eapply fmor_preserves_id. - setoid_rewrite (fmor_preserves_id PMF23). -*) - admit. - Qed. - - Instance PreMonoidalFunctorsCompose : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12) := + repeat setoid_rewrite <- associativity. + setoid_rewrite <- q. + clear q. + repeat setoid_rewrite <- fmor_preserves_comp. + repeat setoid_rewrite <- associativity. + apply comp_respects; try reflexivity. + + set (mf_assoc(PreMonoidalFunctor:=PMF23) (fobj12 a) (fobj12 b) (fobj12 c)) as q. + unfold functor_fobj in *. + simpl in *. + + rewrite H in q. + rewrite H0 in q. + simpl in q. + repeat setoid_rewrite <- associativity. + repeat setoid_rewrite <- associativity in q. + setoid_rewrite <- q. + clear q. + unfold functor_fobj; simpl. + + repeat setoid_rewrite associativity. + apply comp_respects; try reflexivity. + apply comp_respects; try reflexivity. + auto. + + repeat setoid_rewrite associativity. + repeat setoid_rewrite associativity in H1. + repeat setoid_rewrite <- fmor_preserves_comp in H1. + repeat setoid_rewrite associativity in H1. + apply H1. + Qed. + Implicit Arguments id [[Ob][Hom][Category]]. + + (* this proof is really gross; I will write a better one some other day *) + Instance PreMonoidalFunctorsCompose : PreMonoidalFunctor PM1 PM3 compose_mf := { mf_i := compose_mf_i - ; mf_F := compose_mf ; mf_first := compose_mf_first ; mf_second := compose_mf_second }. + intros; unfold compose_mf_first; unfold compose_mf_second. set (mf_first (PMF12 a)) as x in *. set (mf_second (PMF12 b)) as y in *. @@ -359,31 +365,12 @@ Section PreMonoidalFunctorsCompose. repeat setoid_rewrite right_identity. set (mf_consistent (PMF12 a) (PMF12 b)) as later. apply comp_respects; try reflexivity. - unfold functor_comp. - unfold functor_fobj; simpl. - set (ni_commutes _ _ (id (fobj12 b))) as x. - unfold functor_comp in x. - simpl in x. - unfold functor_fobj in x. - symmetry in x. - etransitivity. - apply x. - clear x. - set (ni_commutes0 _ _ (id (fobj12 a))) as x'. - unfold functor_comp in x'. - simpl in x'. - unfold functor_fobj in x'. - etransitivity; [ idtac | apply x' ]. - clear x'. - setoid_rewrite fmor_preserves_id. - setoid_rewrite fmor_preserves_id. - setoid_rewrite right_identity. rewrite <- H in later. rewrite <- H0 in later. simpl in later. apply later. apply fmor_respects. - apply (mf_consistent a b). + apply mf_consistent. intros. simpl. @@ -419,22 +406,13 @@ Section PreMonoidalFunctorsCompose. repeat setoid_rewrite associativity. apply comp_respects; try reflexivity. - set (ni_commutes _ _ (id (fobj12 I1))) as x. + set (ni_commutes _ _ #mf_i) as x. unfold functor_comp in x. unfold functor_fobj in x. simpl in x. - setoid_rewrite <- x. - clear x. - setoid_rewrite fmor_preserves_id. - setoid_rewrite fmor_preserves_id. - setoid_rewrite right_identity. - rewrite H. simpl. - clear H. - unfold functor_comp in ni_commutes. - simpl in ni_commutes. - apply ni_commutes. + apply x. intros. unfold compose_mf_second; simpl. @@ -464,27 +442,20 @@ Section PreMonoidalFunctorsCompose. repeat setoid_rewrite associativity. apply comp_respects; try reflexivity. - set (ni_commutes _ _ (id (fobj12 I1))) as x. + set (ni_commutes _ _ #mf_i) as x. unfold functor_comp in x. unfold functor_fobj in x. simpl in x. - setoid_rewrite <- x. - clear x. - setoid_rewrite fmor_preserves_id. - setoid_rewrite fmor_preserves_id. - setoid_rewrite right_identity. - rewrite H. simpl. - clear H. - unfold functor_comp in ni_commutes. - simpl in ni_commutes. - apply ni_commutes. + apply x. + + apply mf_associativity_comp. - apply compose_assoc_coherence. Defined. End PreMonoidalFunctorsCompose. +Notation "a >>⊗>> b" := (PreMonoidalFunctorsCompose a b). (*******************************************************************************) @@ -493,7 +464,7 @@ End PreMonoidalFunctorsCompose. 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 a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell a) +; triangleb : forall a:C, #(pmon_cancelr a) ~~ #(br_swap a (pmon_I mc)) >>> #(pmon_cancell a) ; hexagon1 : forall {a b c}, #(pmon_assoc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc _ _ _) ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc _ _ _) >>> b ⋊ #(br_swap _ _) ; hexagon2 : forall {a b c}, #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc _ _ _)⁻¹ @@ -704,13 +675,27 @@ Section PreMonoidalWideSubcategory. End PreMonoidalWideSubcategory. +Section IsoFullSubCategory. + Context `{C:Category}. + Context {Pobj}(S:FullSubcategory C Pobj). + + Definition iso_full {a b:C}(i:a≅b)(pa:Pobj a)(pb:Pobj b) : (existT _ _ pa) ≅ (existT _ _ pb). + set (#i : existT Pobj a pa ~~{S}~~> existT Pobj b pb) as i1. + set (iso_backward i : existT Pobj b pb ~~{S}~~> existT Pobj a pa) as i2. + refine {| iso_forward := i1 ; iso_backward := i2 |}. + unfold i1; unfold i2; unfold hom; simpl. + apply iso_comp1. + unfold i1; unfold i2; unfold hom; simpl. + apply iso_comp2. + Defined. +End IsoFullSubCategory. (* a full subcategory inherits the premonoidal structure if it includes the unit object and is closed under object-pairing *) -(* Section PreMonoidalFullSubcategory. Context `(pm:PreMonoidalCat(I:=pmI)). Context {Pobj}(S:FullSubcategory pm Pobj). + Context (Pobj_unit:Pobj pmI). Context (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)). Implicit Arguments Pobj_closed [[a][b]]. @@ -766,44 +751,239 @@ Section PreMonoidalFullSubcategory. { bin_first := PreMonoidalFullSubcategory_first ; bin_second := PreMonoidalFullSubcategory_second }. + Definition central_full {a b}(f:a~~{S}~~>b) + : @CentralMorphism _ _ _ _ pm (projT1 a) (projT1 b) f -> CentralMorphism f. + intro cm. + apply Build_CentralMorphism; simpl. + intros. + destruct a as [a apf]. + destruct b as [b bpf]. + destruct c as [c cpf]. + destruct d as [d dpf]. + simpl. + apply cm. + intros. + destruct a as [a apf]. + destruct b as [b bpf]. + destruct c as [c cpf]. + destruct d as [d dpf]. + simpl. + apply cm. + Defined. + + Notation "a ⊕ b" := (Pobj_closed a b). Definition PreMonoidalFullSubcategory_assoc : forall a b, (PreMonoidalFullSubcategory_second a >>>> PreMonoidalFullSubcategory_first b) <~~~> (PreMonoidalFullSubcategory_first b >>>> PreMonoidalFullSubcategory_second a). - Defined. + intros. + refine {| ni_iso := (fun (c:S) => iso_full S (pmon_assoc(PreMonoidalCat:=pm) _ _ _) + ((projT2 a⊕projT2 c)⊕projT2 b) + (projT2 a⊕(projT2 c⊕projT2 b))) |}. + intros; simpl. + destruct a as [a apf]. + destruct b as [b bpf]. + destruct A as [A Apf]. + destruct B as [B Bpf]. + apply (ni_commutes (pmon_assoc(PreMonoidalCat:=pm) a b) f). + Defined. Definition PreMonoidalFullSubcategory_assoc_ll : forall a b, PreMonoidalFullSubcategory_second (a⊗b) <~~~> PreMonoidalFullSubcategory_second b >>>> PreMonoidalFullSubcategory_second a. - intros. - Defined. + intros. + refine {| ni_iso := (fun (c:S) => iso_full S (pmon_assoc_ll(PreMonoidalCat:=pm) _ _ _) + ((projT2 a⊕projT2 b)⊕projT2 c) + (projT2 a⊕(projT2 b⊕projT2 c)) + ) |}. + intros; simpl. + destruct a as [a apf]. + destruct b as [b bpf]. + destruct A as [A Apf]. + destruct B as [B Bpf]. + apply (ni_commutes (pmon_assoc_ll(PreMonoidalCat:=pm) a b) f). + Defined. Definition PreMonoidalFullSubcategory_assoc_rr : forall a b, PreMonoidalFullSubcategory_first (a⊗b) <~~~> PreMonoidalFullSubcategory_first a >>>> PreMonoidalFullSubcategory_first b. - intros. - Defined. + intros. + refine {| ni_iso := (fun (c:S) => iso_full S (pmon_assoc_rr(PreMonoidalCat:=pm) _ _ _) + (projT2 c⊕(projT2 a⊕projT2 b)) + ((projT2 c⊕projT2 a)⊕projT2 b) + ) |}. + intros; simpl. + destruct a as [a apf]. + destruct b as [b bpf]. + destruct A as [A Apf]. + destruct B as [B Bpf]. + apply (ni_commutes (pmon_assoc_rr(PreMonoidalCat:=pm) a b) f). + Defined. Definition PreMonoidalFullSubcategory_I := existT _ pmI Pobj_unit. + Definition PreMonoidalFullSubcategory_cancelr_iso A + : (fun x : S => PreMonoidalFullSubcategory_bobj x (existT Pobj pmI Pobj_unit)) A ≅ (fun x : S => x) A. + destruct A. + apply (iso_full S). + apply pmon_cancelr. + Defined. + Definition PreMonoidalFullSubcategory_cancelr : PreMonoidalFullSubcategory_first PreMonoidalFullSubcategory_I <~~~> functor_id _. + intros. + refine {| ni_iso := PreMonoidalFullSubcategory_cancelr_iso |}. + intros. + destruct A as [A Apf]. + destruct B as [B Bpf]. + simpl. + apply (ni_commutes (pmon_cancelr(PreMonoidalCat:=pm)) f). + Defined. + + Definition PreMonoidalFullSubcategory_cancell_iso A + : (fun x : S => PreMonoidalFullSubcategory_bobj (existT Pobj pmI Pobj_unit) x) A ≅ (fun x : S => x) A. + destruct A. + apply (iso_full S). + apply pmon_cancell. Defined. Definition PreMonoidalFullSubcategory_cancell : PreMonoidalFullSubcategory_second PreMonoidalFullSubcategory_I <~~~> functor_id _. + intros. + refine {| ni_iso := PreMonoidalFullSubcategory_cancell_iso |}. + intros. + destruct A as [A Apf]. + destruct B as [B Bpf]. + simpl. + apply (ni_commutes (pmon_cancell(PreMonoidalCat:=pm)) f). Defined. Instance PreMonoidalFullSubcategory_PreMonoidal : PreMonoidalCat PreMonoidalFullSubcategory_is_Binoidal PreMonoidalFullSubcategory_I := - { pmon_assoc := PreMonoidalFullSubcategory_assoc - ; pmon_assoc_rr := PreMonoidalFullSubcategory_assoc_rr - ; pmon_assoc_ll := PreMonoidalFullSubcategory_assoc_ll - ; pmon_cancelr := PreMonoidalFullSubcategory_cancelr - ; pmon_cancell := PreMonoidalFullSubcategory_cancell - }. - Defined. + { pmon_assoc := PreMonoidalFullSubcategory_assoc + ; pmon_assoc_rr := PreMonoidalFullSubcategory_assoc_rr + ; pmon_assoc_ll := PreMonoidalFullSubcategory_assoc_ll + ; pmon_cancelr := PreMonoidalFullSubcategory_cancelr + ; pmon_cancell := PreMonoidalFullSubcategory_cancell + }. + apply Build_Pentagon. + intros. + destruct a as [a apf]. + destruct b as [b bpf]. + destruct c as [c cpf]. + destruct d as [d dpf]. + simpl. + apply (pmon_pentagon(PreMonoidalCat:=pm)). + + apply Build_Triangle. + intros. + destruct a as [a apf]. + destruct b as [b bpf]. + simpl. + apply (pmon_triangle(PreMonoidalCat:=pm)). + simpl. + apply (pmon_triangle(PreMonoidalCat:=pm)). + + intros. + destruct a as [a apf]. + destruct c as [c cpf]. + destruct d as [d dpf]. + simpl. + apply (pmon_coherent_r(PreMonoidalCat:=pm)). + + intros. + destruct a as [a apf]. + destruct c as [c cpf]. + destruct d as [d dpf]. + simpl. + apply (pmon_coherent_l(PreMonoidalCat:=pm)). + + intros. + destruct a as [a apf]. + destruct b as [b bpf]. + destruct c as [c cpf]. + simpl. + apply central_full. + simpl. + apply (pmon_assoc_central(PreMonoidalCat:=pm)). + + intros. + destruct a as [a apf]. + simpl. + apply central_full. + simpl. + apply (pmon_cancelr_central(PreMonoidalCat:=pm)). + + intros. + destruct a as [a apf]. + simpl. + apply central_full. + simpl. + apply (pmon_cancell_central(PreMonoidalCat:=pm)). + Defined. + + Instance inclusion_first : ∀a : S, + FullSubcategoryInclusionFunctor S >>>> + - ⋉(FullSubcategoryInclusionFunctor S) a <~~~> + - ⋉a >>>> FullSubcategoryInclusionFunctor S + := { ni_iso := fun A => iso_id ((projT1 A)⊗(projT1 a)) }. + intros; simpl. + symmetry. + setoid_rewrite right_identity. + setoid_rewrite left_identity. + destruct A. + destruct B. + destruct a. + simpl. + reflexivity. + Defined. + + Instance inclusion_second : ∀a : S, + FullSubcategoryInclusionFunctor S >>>> + (FullSubcategoryInclusionFunctor S) a ⋊- <~~~> + a ⋊- >>>> FullSubcategoryInclusionFunctor S + := { ni_iso := fun A => iso_id ((projT1 a)⊗(projT1 A)) }. + intros; simpl. + symmetry. + setoid_rewrite right_identity. + setoid_rewrite left_identity. + destruct A. + destruct B. + destruct a. + simpl. + reflexivity. + Defined. + + (* Curiously, the inclusion functor for a PREmonoidal category isn't necessarily premonoidal (it might fail to preserve + * the center. But in the monoidal case we're okay *) + Instance PreMonoidalFullSubcategoryInclusionFunctor_PreMonoidal (mc:CommutativeCat pm) + : PreMonoidalFunctor PreMonoidalFullSubcategory_PreMonoidal pm (FullSubcategoryInclusionFunctor S) := + { mf_i := iso_id _ + ; mf_first := inclusion_first + ; mf_first := inclusion_second + }. + intros; destruct a; destruct b; reflexivity. + intros; destruct a; destruct b; simpl in *. + apply mc. + intros; destruct b; simpl. + setoid_rewrite right_identity. + setoid_rewrite fmor_preserves_id. + setoid_rewrite left_identity. + reflexivity. + intros; destruct a; simpl. + setoid_rewrite right_identity. + setoid_rewrite fmor_preserves_id. + setoid_rewrite left_identity. + reflexivity. + intros; destruct a; destruct b; destruct c; simpl. + setoid_rewrite right_identity. + setoid_rewrite fmor_preserves_id. + setoid_rewrite left_identity. + setoid_rewrite right_identity. + reflexivity. + Defined. + End PreMonoidalFullSubcategory. -*) \ No newline at end of file +