1 Generalizable All Variables.
2 Require Import Preamble.
3 Require Import Categories_ch1_3.
4 Require Import Functors_ch1_4.
5 Require Import Isomorphisms_ch1_5.
6 Require Import InitialTerminal_ch2_2.
7 Require Import Subcategories_ch7_1.
8 Require Import NaturalTransformations_ch7_4.
9 Require Import NaturalIsomorphisms_ch7_5.
10 Require Import Coherence_ch7_8.
11 Require Import BinoidalCategories.
14 Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
18 ; pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
19 ; pmon_cancelr : (bin_first I) <~~~> functor_id C
20 ; pmon_cancell : (bin_second I) <~~~> functor_id C
21 ; 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))
22 ; 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))
23 (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
24 ; pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b)
25 ; pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
26 ; pmon_coherent_r : forall a c d:C, #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
27 ; pmon_coherent_l : forall a c d:C, #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
28 ; pmon_assoc_central : forall a b c, CentralMorphism #(pmon_assoc a b c)
29 ; pmon_cancelr_central : forall a , CentralMorphism #(pmon_cancelr a)
30 ; pmon_cancell_central : forall a , CentralMorphism #(pmon_cancell a)
33 * Premonoidal categories actually have three associators (the "f"
34 * indicates the position in which the operation is natural:
36 * assoc : (A ⋊ f) ⋉ C <-> A ⋊ (f ⋉ C)
37 * assoc_rr : (f ⋉ B) ⋉ C <-> f ⋉ (B ⊗ C)
38 * assoc_ll : (A ⋊ B) ⋊ f <-> (A ⊗ B) ⋊ f
40 * Fortunately, in a monoidal category these are all the same natural
41 * isomorphism (and in any case -- monoidal or not -- the objects in
42 * the left column are all the same and the objects in the right
43 * column are all the same). This formalization assumes that is the
44 * case even for premonoidal categories with non-central maps, in
45 * order to keep the complexity manageable. I don't know much about
46 * the consequences of having them and letting them be different; you
47 * might need extra versions of the triangle/pentagon diagrams.
50 Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
51 Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
52 Implicit Arguments pmon_assoc [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
53 Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
55 (* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
56 Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b
57 : #(pmon_cancelr (a ⊗ b)) ~~ #((pmon_assoc a EI) b) >>> (a ⋊-) \ #(pmon_cancelr b).
58 set (pmon_pentagon EI EI a b) as penta. unfold pmon_pentagon in penta.
59 set (pmon_triangle a b) as tria. unfold pmon_triangle in tria.
60 apply (fmor_respects(bin_second EI)) in tria.
61 set (@fmor_preserves_comp) as fpc.
62 setoid_rewrite <- fpc in tria.
63 set (ni_commutes (pmon_assoc a b)) as xx.
67 Class PreMonoidalFunctor
68 `(PM1:PreMonoidalCat(C:=C1)(I:=I1))
69 `(PM2:PreMonoidalCat(C:=C2)(I:=I2))
71 { mf_F :> Functor C1 C2 fobj
73 ; mf_first : ∀ a, mf_F >>>> bin_first (mf_F a) <~~~> bin_first a >>>> mf_F
74 ; mf_second : ∀ a, mf_F >>>> bin_second (mf_F a) <~~~> bin_second a >>>> mf_F
75 ; mf_consistent : ∀ a b, #(mf_first a b) ~~ #(mf_second b a)
76 ; mf_center : forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
77 ; mf_cancell : ∀ b, #(pmon_cancell _) ~~ #mf_i ⋉ _ >>> #(mf_first b I1) >>> mf_F \ #(pmon_cancell b)
78 ; mf_cancelr : ∀ a, #(pmon_cancelr _) ~~ _ ⋊ #mf_i >>> #(mf_second a I1) >>> mf_F \ #(pmon_cancelr a)
79 ; mf_assoc : ∀ a b c, #(pmon_assoc _ _ _) >>> _ ⋊ #(mf_second _ _) >>> #(mf_second _ _) ~~
80 #(mf_second _ _) ⋉ _ >>> #(mf_second _ _) >>> mf_F \ #(pmon_assoc a c b)
82 Coercion mf_F : PreMonoidalFunctor >-> Functor.
84 Section PreMonoidalFunctorsCompose.
86 `{PM1 :PreMonoidalCat(C:=C1)(I:=I1)}
87 `{PM2 :PreMonoidalCat(C:=C2)(I:=I2)}
89 (PMF12 :PreMonoidalFunctor PM1 PM2 fobj12)
90 `{PM3 :PreMonoidalCat(C:=C3)(I:=I3)}
92 (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23).
94 Definition compose_mf := PMF12 >>>> PMF23.
96 Definition compose_mf_i : I3 ≅ PMF23 (PMF12 I1).
98 apply (mf_i(PreMonoidalFunctor:=PMF23)).
99 apply functors_preserve_isos.
100 apply (mf_i(PreMonoidalFunctor:=PMF12)).
103 Definition compose_mf_first a : compose_mf >>>> bin_first (compose_mf a) <~~~> bin_first a >>>> compose_mf.
104 set (mf_first(PreMonoidalFunctor:=PMF12) a) as mf_first12.
105 set (mf_first(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_first23.
106 unfold functor_fobj in *; simpl in *.
109 apply (ni_associativity PMF12 PMF23 (- ⋉fobj23 (fobj12 a))).
111 apply (ni_respects PMF12 PMF12 (PMF23 >>>> - ⋉fobj23 (fobj12 a)) (- ⋉fobj12 a >>>> PMF23)).
118 apply (ni_associativity PMF12 (- ⋉fobj12 a) PMF23).
123 eapply (ni_associativity _ PMF12 PMF23).
125 apply ni_respects; [ idtac | apply ni_id ].
130 Definition compose_mf_second a : compose_mf >>>> bin_second (compose_mf a) <~~~> bin_second a >>>> compose_mf.
131 set (mf_second(PreMonoidalFunctor:=PMF12) a) as mf_second12.
132 set (mf_second(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_second23.
133 unfold functor_fobj in *; simpl in *.
136 apply (ni_associativity PMF12 PMF23 (fobj23 (fobj12 a) ⋊-)).
138 apply (ni_respects PMF12 PMF12 (PMF23 >>>> fobj23 (fobj12 a) ⋊-) (fobj12 a ⋊- >>>> PMF23)).
145 apply (ni_associativity PMF12 (fobj12 a ⋊ -) PMF23).
150 eapply (ni_associativity (a ⋊-) PMF12 PMF23).
152 apply ni_respects; [ idtac | apply ni_id ].
157 Lemma compose_assoc_coherence a b c :
158 (#((pmon_assoc (compose_mf a) (fobj23 (fobj12 c))) (compose_mf b)) >>>
159 compose_mf a ⋊ #((compose_mf_second b) c)) >>>
160 #((compose_mf_second a) (b ⊗ c)) ~~
161 (#((compose_mf_second a) b) ⋉ fobj23 (fobj12 c) >>>
162 #((compose_mf_second (a ⊗ b)) c)) >>> compose_mf \ #((pmon_assoc a c) b).
164 set (mf_assoc a b c) as x.
165 set (mf_assoc (fobj12 a) (fobj12 b) (fobj12 c)) as x'.
166 unfold functor_fobj in *.
174 apply iso_shift_left' in x'.
176 unfold compose_mf_second; simpl.
177 unfold functor_fobj; simpl.
178 set (mf_second (fobj12 b)) as m.
179 assert (mf_second (fobj12 b)=m). reflexivity.
181 setoid_rewrite <- fmor_preserves_comp.
182 setoid_rewrite <- fmor_preserves_comp.
183 setoid_rewrite <- fmor_preserves_comp.
184 setoid_rewrite <- fmor_preserves_comp.
185 setoid_rewrite <- fmor_preserves_comp.
186 setoid_rewrite fmor_preserves_id.
187 setoid_rewrite fmor_preserves_id.
188 setoid_rewrite fmor_preserves_id.
189 setoid_rewrite right_identity.
190 setoid_rewrite left_identity.
191 setoid_rewrite left_identity.
192 setoid_rewrite left_identity.
194 set (mf_second (fobj12 (a ⊗ b))) as m''.
195 assert (mf_second (fobj12 (a ⊗ b))=m''). reflexivity.
197 unfold functor_fobj; simpl.
198 setoid_rewrite fmor_preserves_id.
199 setoid_rewrite fmor_preserves_id.
200 setoid_rewrite right_identity.
201 setoid_rewrite left_identity.
202 setoid_rewrite left_identity.
203 setoid_rewrite left_identity.
205 set (mf_second (fobj12 a)) as m'.
206 assert (mf_second (fobj12 a)=m'). reflexivity.
208 setoid_rewrite <- fmor_preserves_comp.
209 setoid_rewrite <- fmor_preserves_comp.
210 setoid_rewrite <- fmor_preserves_comp.
211 setoid_rewrite <- fmor_preserves_comp.
212 setoid_rewrite <- fmor_preserves_comp.
213 setoid_rewrite left_identity.
214 setoid_rewrite left_identity.
215 setoid_rewrite left_identity.
216 setoid_rewrite right_identity.
217 assert (fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 (b ⊗ c)) ~~ id _).
220 setoid_rewrite left_identity.
221 assert ((id (fobj23 (fobj12 a) ⊗ fobj23 (fobj12 b)) ⋉ fobj23 (fobj12 c)) ~~ id _).
224 setoid_rewrite left_identity.
225 assert (id (fobj23 (fobj12 a ⊗ fobj12 b)) ⋉ fobj23 (fobj12 c) ~~ id _).
228 setoid_rewrite left_identity.
230 setoid_rewrite left_identity.
231 assert (id (fobj23 (fobj12 (a ⊗ b))) ⋉ fobj23 (fobj12 c) ~~ id _).
234 setoid_rewrite right_identity.
236 assert ((fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 b)) ⋉ fobj23 (fobj12 c) ~~ id _).
239 setoid_rewrite left_identity.
241 unfold functor_comp in ni_commutes0; simpl in ni_commutes0.
242 unfold functor_comp in ni_commutes; simpl in ni_commutes.
243 unfold functor_comp in ni_commutes1; simpl in ni_commutes1.
246 unfold functor_fobj in *.
248 setoid_rewrite x in x'.
250 set (ni_commutes0 (a )
251 setoid_rewrite fmor_preserves_id.
253 eapply comp_respects.
255 eapply comp_respects.
256 eapply comp_respects.
259 eapply fmor_preserves_id.
260 setoid_rewrite (fmor_preserves_id PMF23).
265 Instance PreMonoidalFunctorsCompose : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12) :=
266 { mf_i := compose_mf_i
268 ; mf_first := compose_mf_first
269 ; mf_second := compose_mf_second }.
270 intros; unfold compose_mf_first; unfold compose_mf_second.
271 set (mf_first (PMF12 a)) as x in *.
272 set (mf_second (PMF12 b)) as y in *.
273 assert (x=mf_first (PMF12 a)). reflexivity.
274 assert (y=mf_second (PMF12 b)). reflexivity.
278 repeat setoid_rewrite left_identity.
279 repeat setoid_rewrite right_identity.
280 set (mf_consistent (PMF12 a) (PMF12 b)) as later.
281 apply comp_respects; try reflexivity.
283 unfold functor_fobj; simpl.
284 set (ni_commutes _ _ (id (fobj12 b))) as x.
285 unfold functor_comp in x.
287 unfold functor_fobj in x.
292 set (ni_commutes0 _ _ (id (fobj12 a))) as x'.
293 unfold functor_comp in x'.
295 unfold functor_fobj in x'.
296 etransitivity; [ idtac | apply x' ].
298 setoid_rewrite fmor_preserves_id.
299 setoid_rewrite fmor_preserves_id.
300 setoid_rewrite right_identity.
301 rewrite <- H in later.
302 rewrite <- H0 in later.
306 apply (mf_consistent a b).
315 unfold compose_mf_first; simpl.
316 set (mf_first (PMF12 b)) as m.
317 assert (mf_first (PMF12 b)=m). reflexivity.
320 unfold functor_fobj; simpl.
321 repeat setoid_rewrite <- fmor_preserves_comp.
322 repeat setoid_rewrite left_identity.
323 repeat setoid_rewrite right_identity.
325 set (mf_cancell b) as y.
326 set (mf_cancell (fobj12 b)) as y'.
327 unfold functor_fobj in *.
328 setoid_rewrite y in y'.
330 setoid_rewrite <- fmor_preserves_comp in y'.
331 setoid_rewrite <- fmor_preserves_comp in y'.
336 repeat setoid_rewrite <- associativity.
337 apply comp_respects; try reflexivity.
338 apply comp_respects; try reflexivity.
339 repeat setoid_rewrite associativity.
340 apply comp_respects; try reflexivity.
342 set (ni_commutes _ _ (id (fobj12 I1))) as x.
343 unfold functor_comp in x.
344 unfold functor_fobj in x.
348 setoid_rewrite fmor_preserves_id.
349 setoid_rewrite fmor_preserves_id.
350 setoid_rewrite right_identity.
355 unfold functor_comp in ni_commutes.
356 simpl in ni_commutes.
360 unfold compose_mf_second; simpl.
361 set (mf_second (PMF12 a)) as m.
362 assert (mf_second (PMF12 a)=m). reflexivity.
365 unfold functor_fobj; simpl.
366 repeat setoid_rewrite <- fmor_preserves_comp.
367 repeat setoid_rewrite left_identity.
368 repeat setoid_rewrite right_identity.
370 set (mf_cancelr a) as y.
371 set (mf_cancelr (fobj12 a)) as y'.
372 unfold functor_fobj in *.
373 setoid_rewrite y in y'.
375 setoid_rewrite <- fmor_preserves_comp in y'.
376 setoid_rewrite <- fmor_preserves_comp in y'.
381 repeat setoid_rewrite <- associativity.
382 apply comp_respects; try reflexivity.
383 apply comp_respects; try reflexivity.
384 repeat setoid_rewrite associativity.
385 apply comp_respects; try reflexivity.
387 set (ni_commutes _ _ (id (fobj12 I1))) as x.
388 unfold functor_comp in x.
389 unfold functor_fobj in x.
393 setoid_rewrite fmor_preserves_id.
394 setoid_rewrite fmor_preserves_id.
395 setoid_rewrite right_identity.
400 unfold functor_comp in ni_commutes.
401 simpl in ni_commutes.
404 apply compose_assoc_coherence.
407 End PreMonoidalFunctorsCompose.
410 (*******************************************************************************)
411 (* Braided and Symmetric Categories *)
413 Class BraidedCat `(mc:PreMonoidalCat) :=
414 { br_niso : forall a, bin_first a <~~~> bin_second a
415 ; br_swap := fun a b => ni_iso (br_niso b) a
416 ; triangleb : forall a:C, #(pmon_cancelr a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell a)
417 ; hexagon1 : forall {a b c}, #(pmon_assoc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc _ _ _)
418 ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc _ _ _) >>> b ⋊ #(br_swap _ _)
419 ; hexagon2 : forall {a b c}, #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc _ _ _)⁻¹
420 ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
423 Class SymmetricCat `(bc:BraidedCat) :=
424 { symcat_swap : forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
428 (* a wide subcategory inherits the premonoidal structure if it includes all of the coherence maps *)
429 Section PreMonoidalWideSubcategory.
431 Context `(pm:PreMonoidalCat(I:=pmI)).
432 Context {Pmor}(S:WideSubcategory pm Pmor).
433 Context (Pmor_first : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (f ⋉ c)).
434 Context (Pmor_second : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (c ⋊ f)).
435 Context (Pmor_assoc : forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)).
436 Context (Pmor_unassoc: forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)⁻¹).
437 Context (Pmor_cancell: forall {a}, Pmor _ _ #(pmon_cancell a)).
438 Context (Pmor_uncancell: forall {a}, Pmor _ _ #(pmon_cancell a)⁻¹).
439 Context (Pmor_cancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)).
440 Context (Pmor_uncancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)⁻¹).
441 Implicit Arguments Pmor_first [[a][b][c][f]].
442 Implicit Arguments Pmor_second [[a][b][c][f]].
444 Definition PreMonoidalWideSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' x a)~~{S}~~>(bin_obj' y a).
445 unfold hom; simpl; intros.
448 exists (bin_first(BinoidalCat:=pm) a \ x0).
449 apply Pmor_first; auto.
452 Definition PreMonoidalWideSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' a x)~~{S}~~>(bin_obj' a y).
453 unfold hom; simpl; intros.
456 exists (bin_second(BinoidalCat:=pm) a \ x0).
457 apply Pmor_second; auto.
460 Instance PreMonoidalWideSubcategory_first (a:S) : Functor S S (fun x => bin_obj' x a) :=
461 { fmor := fun x y f => PreMonoidalWideSubcategory_first_fmor a f }.
462 unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct f'; simpl in *.
463 apply (fmor_respects (bin_first(BinoidalCat:=pm) a)); auto.
464 unfold PreMonoidalWideSubcategory_first_fmor; intros; simpl in *.
465 apply (fmor_preserves_id (bin_first(BinoidalCat:=pm) a)); auto.
466 unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct g; simpl in *.
467 apply (fmor_preserves_comp (bin_first(BinoidalCat:=pm) a)); auto.
470 Instance PreMonoidalWideSubcategory_second (a:S) : Functor S S (fun x => bin_obj' a x) :=
471 { fmor := fun x y f => PreMonoidalWideSubcategory_second_fmor a f }.
472 unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct f'; simpl in *.
473 apply (fmor_respects (bin_second(BinoidalCat:=pm) a)); auto.
474 unfold PreMonoidalWideSubcategory_second_fmor; intros; simpl in *.
475 apply (fmor_preserves_id (bin_second(BinoidalCat:=pm) a)); auto.
476 unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct g; simpl in *.
477 apply (fmor_preserves_comp (bin_second(BinoidalCat:=pm) a)); auto.
480 Instance PreMonoidalWideSubcategory_is_Binoidal : BinoidalCat S bin_obj' :=
481 { bin_first := PreMonoidalWideSubcategory_first
482 ; bin_second := PreMonoidalWideSubcategory_second }.
484 Definition PreMonoidalWideSubcategory_assoc_iso
485 : forall a b c, Isomorphic(C:=S) (bin_obj' (bin_obj' a b) c) (bin_obj' a (bin_obj' b c)).
487 refine {| iso_forward := existT _ _ (Pmor_assoc a b c) ; iso_backward := existT _ _ (Pmor_unassoc a b c) |}.
488 simpl; apply iso_comp1.
489 simpl; apply iso_comp2.
492 Definition PreMonoidalWideSubcategory_assoc
494 (PreMonoidalWideSubcategory_second a >>>> PreMonoidalWideSubcategory_first b) <~~~>
495 (PreMonoidalWideSubcategory_first b >>>> PreMonoidalWideSubcategory_second a).
497 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (PreMonoidalWideSubcategory_second a >>>>
498 PreMonoidalWideSubcategory_first b) (PreMonoidalWideSubcategory_first b >>>>
499 PreMonoidalWideSubcategory_second a) (fun c => PreMonoidalWideSubcategory_assoc_iso a c b)).
501 unfold PreMonoidalWideSubcategory_second_fmor; simpl.
503 set (ni_commutes (pmon_assoc(PreMonoidalCat:=pm) a b) x) as q.
507 Definition PreMonoidalWideSubcategory_assoc_ll
509 PreMonoidalWideSubcategory_second (a⊗b) <~~~>
510 PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a.
512 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
513 (PreMonoidalWideSubcategory_second (a⊗b))
514 (PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a)
515 (fun c => PreMonoidalWideSubcategory_assoc_iso a b c)).
517 unfold PreMonoidalWideSubcategory_second_fmor; simpl.
519 set (ni_commutes (pmon_assoc_ll(PreMonoidalCat:=pm) a b) x) as q.
520 unfold functor_comp in q; simpl in q.
521 set (pmon_coherent_l(PreMonoidalCat:=pm)) as q'.
522 setoid_rewrite q' in q.
526 Definition PreMonoidalWideSubcategory_assoc_rr
528 PreMonoidalWideSubcategory_first (a⊗b) <~~~>
529 PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b.
532 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
533 (PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b)
534 (PreMonoidalWideSubcategory_first (a⊗b))
535 (fun c => PreMonoidalWideSubcategory_assoc_iso c a b)).
537 unfold PreMonoidalWideSubcategory_second_fmor; simpl.
539 set (ni_commutes (pmon_assoc_rr(PreMonoidalCat:=pm) a b) x) as q.
540 unfold functor_comp in q; simpl in q.
541 set (pmon_coherent_r(PreMonoidalCat:=pm)) as q'.
542 setoid_rewrite q' in q.
543 apply iso_shift_right' in q.
544 apply iso_shift_left.
546 setoid_rewrite iso_inv_inv in q.
547 setoid_rewrite associativity.
551 Definition PreMonoidalWideSubcategory_cancelr_iso : forall a, Isomorphic(C:=S) (bin_obj' a pmI) a.
553 refine {| iso_forward := existT _ _ (Pmor_cancelr a) ; iso_backward := existT _ _ (Pmor_uncancelr a) |}.
554 simpl; apply iso_comp1.
555 simpl; apply iso_comp2.
558 Definition PreMonoidalWideSubcategory_cancell_iso : forall a, Isomorphic(C:=S) (bin_obj' pmI a) a.
560 refine {| iso_forward := existT _ _ (Pmor_cancell a) ; iso_backward := existT _ _ (Pmor_uncancell a) |}.
561 simpl; apply iso_comp1.
562 simpl; apply iso_comp2.
565 Definition PreMonoidalWideSubcategory_cancelr : PreMonoidalWideSubcategory_first pmI <~~~> functor_id _.
566 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
567 (PreMonoidalWideSubcategory_first pmI) (functor_id _) PreMonoidalWideSubcategory_cancelr_iso).
569 unfold PreMonoidalWideSubcategory_first_fmor; simpl.
571 apply (ni_commutes (pmon_cancelr(PreMonoidalCat:=pm)) x).
574 Definition PreMonoidalWideSubcategory_cancell : PreMonoidalWideSubcategory_second pmI <~~~> functor_id _.
575 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
576 (PreMonoidalWideSubcategory_second pmI) (functor_id _) PreMonoidalWideSubcategory_cancell_iso).
578 unfold PreMonoidalWideSubcategory_second_fmor; simpl.
580 apply (ni_commutes (pmon_cancell(PreMonoidalCat:=pm)) x).
583 Instance PreMonoidalWideSubcategory_PreMonoidal : PreMonoidalCat PreMonoidalWideSubcategory_is_Binoidal pmI :=
584 { pmon_assoc := PreMonoidalWideSubcategory_assoc
585 ; pmon_assoc_rr := PreMonoidalWideSubcategory_assoc_rr
586 ; pmon_assoc_ll := PreMonoidalWideSubcategory_assoc_ll
587 ; pmon_cancelr := PreMonoidalWideSubcategory_cancelr
588 ; pmon_cancell := PreMonoidalWideSubcategory_cancell
590 apply Build_Pentagon.
591 intros; unfold PreMonoidalWideSubcategory_assoc; simpl.
592 set (pmon_pentagon(PreMonoidalCat:=pm) a b c) as q.
595 apply Build_Triangle.
596 intros; unfold PreMonoidalWideSubcategory_assoc;
597 unfold PreMonoidalWideSubcategory_cancelr; unfold PreMonoidalWideSubcategory_cancell; simpl.
598 set (pmon_triangle(PreMonoidalCat:=pm) a b) as q.
603 set (pmon_triangle(PreMonoidalCat:=pm)) as q.
606 intros; simpl; reflexivity.
607 intros; simpl; reflexivity.
610 apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
611 apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c).
612 apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c).
615 apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
616 apply (pmon_cancelr_central(PreMonoidalCat:=pm) a).
617 apply (pmon_cancelr_central(PreMonoidalCat:=pm) a).
620 apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
621 apply (pmon_cancell_central(PreMonoidalCat:=pm) a).
622 apply (pmon_cancell_central(PreMonoidalCat:=pm) a).
625 End PreMonoidalWideSubcategory.
628 (* a full subcategory inherits the premonoidal structure if it includes the unit object and is closed under object-pairing *)
630 Section PreMonoidalFullSubcategory.
632 Context `(pm:PreMonoidalCat(I:=pmI)).
633 Context {Pobj}(S:FullSubcategory pm Pobj).
634 Context (Pobj_unit:Pobj pmI).
635 Context (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)).
636 Implicit Arguments Pobj_closed [[a][b]].
638 Definition PreMonoidalFullSubcategory_bobj (x y:S) :=
639 existT Pobj _ (Pobj_closed (projT2 x) (projT2 y)).
641 Definition PreMonoidalFullSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
642 (PreMonoidalFullSubcategory_bobj x a)~~{S}~~>(PreMonoidalFullSubcategory_bobj y a).
643 unfold hom; simpl; intros.
644 destruct a as [a apf].
645 destruct x as [x xpf].
646 destruct y as [y ypf].
651 Definition PreMonoidalFullSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
652 (PreMonoidalFullSubcategory_bobj a x)~~{S}~~>(PreMonoidalFullSubcategory_bobj a y).
653 unfold hom; simpl; intros.
654 destruct a as [a apf].
655 destruct x as [x xpf].
656 destruct y as [y ypf].
661 Instance PreMonoidalFullSubcategory_first (a:S)
662 : Functor S S (fun x => PreMonoidalFullSubcategory_bobj x a) :=
663 { fmor := fun x y f => PreMonoidalFullSubcategory_first_fmor a f }.
664 unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0; destruct b; simpl in *.
665 apply (fmor_respects (-⋉x)); auto.
666 unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0; simpl in *.
667 apply (fmor_preserves_id (-⋉x)); auto.
668 unfold PreMonoidalFullSubcategory_first_fmor; intros;
669 destruct a; destruct a0; destruct b; destruct c; simpl in *.
670 apply (fmor_preserves_comp (-⋉x)); auto.
673 Instance PreMonoidalFullSubcategory_second (a:S)
674 : Functor S S (fun x => PreMonoidalFullSubcategory_bobj a x) :=
675 { fmor := fun x y f => PreMonoidalFullSubcategory_second_fmor a f }.
676 unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0; destruct b; simpl in *.
677 apply (fmor_respects (x⋊-)); auto.
678 unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0; simpl in *.
679 apply (fmor_preserves_id (x⋊-)); auto.
680 unfold PreMonoidalFullSubcategory_second_fmor; intros;
681 destruct a; destruct a0; destruct b; destruct c; simpl in *.
682 apply (fmor_preserves_comp (x⋊-)); auto.
685 Instance PreMonoidalFullSubcategory_is_Binoidal : BinoidalCat S PreMonoidalFullSubcategory_bobj :=
686 { bin_first := PreMonoidalFullSubcategory_first
687 ; bin_second := PreMonoidalFullSubcategory_second }.
689 Definition PreMonoidalFullSubcategory_assoc
691 (PreMonoidalFullSubcategory_second a >>>> PreMonoidalFullSubcategory_first b) <~~~>
692 (PreMonoidalFullSubcategory_first b >>>> PreMonoidalFullSubcategory_second a).
695 Definition PreMonoidalFullSubcategory_assoc_ll
697 PreMonoidalFullSubcategory_second (a⊗b) <~~~>
698 PreMonoidalFullSubcategory_second b >>>> PreMonoidalFullSubcategory_second a.
702 Definition PreMonoidalFullSubcategory_assoc_rr
704 PreMonoidalFullSubcategory_first (a⊗b) <~~~>
705 PreMonoidalFullSubcategory_first a >>>> PreMonoidalFullSubcategory_first b.
709 Definition PreMonoidalFullSubcategory_I := existT _ pmI Pobj_unit.
711 Definition PreMonoidalFullSubcategory_cancelr
712 : PreMonoidalFullSubcategory_first PreMonoidalFullSubcategory_I <~~~> functor_id _.
715 Definition PreMonoidalFullSubcategory_cancell
716 : PreMonoidalFullSubcategory_second PreMonoidalFullSubcategory_I <~~~> functor_id _.
719 Instance PreMonoidalFullSubcategory_PreMonoidal
720 : PreMonoidalCat PreMonoidalFullSubcategory_is_Binoidal PreMonoidalFullSubcategory_I :=
721 { pmon_assoc := PreMonoidalFullSubcategory_assoc
722 ; pmon_assoc_rr := PreMonoidalFullSubcategory_assoc_rr
723 ; pmon_assoc_ll := PreMonoidalFullSubcategory_assoc_ll
724 ; pmon_cancelr := PreMonoidalFullSubcategory_cancelr
725 ; pmon_cancell := PreMonoidalFullSubcategory_cancell
728 End PreMonoidalFullSubcategory.