Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
* 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 ].
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
; 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.
`{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.
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.
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.
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.
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 *.
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.
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.
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).
(*******************************************************************************)
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 _ _ _)⁻¹
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]].
{ 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
+
projects / coq-categories.git / blobdiff