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 EpicMonic_ch2_1.
7 Require Import InitialTerminal_ch2_2.
8 Require Import Subcategories_ch7_1.
9 Require Import NaturalTransformations_ch7_4.
10 Require Import NaturalIsomorphisms_ch7_5.
11 Require Import Coherence_ch7_8.
12 Require Import BinoidalCategories.
15 Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
19 ; pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
20 ; pmon_cancelr : (bin_first I) <~~~> functor_id C
21 ; pmon_cancell : (bin_second I) <~~~> functor_id C
22 ; 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)⁻¹)
23 ; 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)⁻¹)
24 (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
25 ; pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b)
26 ; pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
27 ; pmon_coherent_r : forall a c d:C, #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
28 ; pmon_coherent_l : forall a c d:C, #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
29 ; pmon_assoc_central : forall a b c, CentralMorphism #(pmon_assoc a b c)
30 ; pmon_cancelr_central : forall a , CentralMorphism #(pmon_cancelr a)
31 ; pmon_cancell_central : forall a , CentralMorphism #(pmon_cancell a)
34 * Premonoidal categories actually have three associators (the "f"
35 * indicates the position in which the operation is natural:
37 * assoc : (A ⋊ f) ⋉ C <-> A ⋊ (f ⋉ C)
38 * assoc_rr : (f ⋉ B) ⋉ C <-> f ⋉ (B ⊗ C)
39 * assoc_ll : (A ⋊ B) ⋊ f <-> (A ⊗ B) ⋊ f
41 * Fortunately, in a monoidal category these are all the same natural
42 * isomorphism (and in any case -- monoidal or not -- the objects in
43 * the left column are all the same and the objects in the right
44 * column are all the same). This formalization assumes that is the
45 * case even for premonoidal categories with non-central maps, in
46 * order to keep the complexity manageable. I don't know much about
47 * the consequences of having them and letting them be different; you
48 * might need extra versions of the triangle/pentagon diagrams.
51 Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
52 Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
53 Implicit Arguments pmon_assoc [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
54 Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
56 (* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
57 Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} d c
59 let α := fun a b c => #((pmon_assoc a c) b)⁻¹
60 in α EI c d >>> #(pmon_cancell _) ⋉ _ ~~ #(pmon_cancell _).
64 (* following Mac Lane's hint, we aim for (λ >>> α >>> λ×1)~~(λ >>> λ) *)
65 set (epic _ (iso_epic (pmon_cancell (EI⊗(c⊗d))))) as q.
69 (* next, we show that the hint goal above is implied by the bottom-left 1/5th of the big whiteboard diagram *)
70 set (ni_commutes pmon_cancell (α EI c d)) as q.
71 setoid_rewrite <- associativity.
74 setoid_rewrite associativity.
76 set (ni_commutes pmon_cancell (#(pmon_cancell c) ⋉ d)) as q.
81 set (ni_commutes pmon_cancell (#(pmon_cancell (c⊗d)))) as q.
86 setoid_rewrite <- associativity.
87 apply comp_respects; try reflexivity.
89 (* now we carry out the proof in the whiteboard diagram, starting from the pentagon diagram *)
92 assert (α EI EI (c⊗d) >>> α _ _ _ >>> (#(pmon_cancelr _) ⋉ _ ⋉ _) ~~ _ ⋊ #(pmon_cancell _) >>> α _ _ _).
93 set (pmon_triangle EI (c⊗d)) as tria.
95 setoid_rewrite <- tria.
98 set (ni_commutes (pmon_assoc_rr c d) #(pmon_cancelr EI)) as x.
100 setoid_rewrite pmon_coherent_r in x.
102 setoid_rewrite associativity.
108 assert (_ ⋊ α _ _ _ >>> α EI (EI⊗c) d >>> α _ _ _ ⋉ _ >>> (#(pmon_cancelr _) ⋉ _ ⋉ _) ~~
109 _ ⋊ α _ _ _ >>> _ ⋊ (#(pmon_cancell _) ⋉ _) >>> α _ _ _ ).
111 repeat setoid_rewrite associativity.
112 apply comp_respects; try reflexivity.
114 set (ni_commutes (pmon_assoc EI d) (#(pmon_cancell c) )) as x.
116 setoid_rewrite <- associativity.
117 apply iso_shift_right' in x.
119 setoid_rewrite <- associativity in x.
120 apply iso_shift_left' in x.
125 setoid_rewrite associativity.
126 apply comp_respects; try reflexivity.
127 setoid_rewrite (fmor_preserves_comp (-⋉d)).
128 apply (fmor_respects (-⋉d)).
130 set (pmon_triangle EI c) as tria.
134 set (pmon_pentagon EI EI c d) as penta. unfold pmon_pentagon in penta. simpl in penta.
136 set (@comp_respects _ _ _ _ _ _ _ _ penta (#(pmon_cancelr EI) ⋉ c ⋉ d) (#(pmon_cancelr EI) ⋉ c ⋉ d)) as qq.
138 setoid_rewrite H in qq.
140 setoid_rewrite H0 in qq.
143 assert (EI⋊(iso_backward ((pmon_assoc EI d) c) >>> #(pmon_cancell c) ⋉ d) ~~ EI⋊ #(pmon_cancell (c ⊗ d)) ).
144 apply (@monic _ _ _ _ _ _ (iso_monic (iso_inv _ _ ((pmon_assoc EI d) c)))).
147 setoid_rewrite <- fmor_preserves_comp.
148 apply qq; try reflexivity.
151 setoid_rewrite fmor_preserves_comp.
156 Class PreMonoidalFunctor
157 `(PM1:PreMonoidalCat(C:=C1)(I:=I1))
158 `(PM2:PreMonoidalCat(C:=C2)(I:=I2))
159 (fobj : C1 -> C2 ) :=
160 { mf_F :> Functor C1 C2 fobj
161 ; mf_i : I2 ≅ mf_F I1
162 ; mf_first : ∀ a, mf_F >>>> bin_first (mf_F a) <~~~> bin_first a >>>> mf_F
163 ; mf_second : ∀ a, mf_F >>>> bin_second (mf_F a) <~~~> bin_second a >>>> mf_F
164 ; mf_consistent : ∀ a b, #(mf_first a b) ~~ #(mf_second b a)
165 ; mf_center : forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
166 ; mf_cancell : ∀ b, #(pmon_cancell _) ~~ #mf_i ⋉ _ >>> #(mf_first b I1) >>> mf_F \ #(pmon_cancell b)
167 ; mf_cancelr : ∀ a, #(pmon_cancelr _) ~~ _ ⋊ #mf_i >>> #(mf_second a I1) >>> mf_F \ #(pmon_cancelr a)
168 ; mf_assoc : ∀ a b c, #(pmon_assoc _ _ _) >>> _ ⋊ #(mf_second _ _) >>> #(mf_second _ _) ~~
169 #(mf_second _ _) ⋉ _ >>> #(mf_second _ _) >>> mf_F \ #(pmon_assoc a c b)
171 Coercion mf_F : PreMonoidalFunctor >-> Functor.
173 Section PreMonoidalFunctorsCompose.
175 `{PM1 :PreMonoidalCat(C:=C1)(I:=I1)}
176 `{PM2 :PreMonoidalCat(C:=C2)(I:=I2)}
178 (PMF12 :PreMonoidalFunctor PM1 PM2 fobj12)
179 `{PM3 :PreMonoidalCat(C:=C3)(I:=I3)}
181 (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23).
183 Definition compose_mf := PMF12 >>>> PMF23.
185 Definition compose_mf_i : I3 ≅ PMF23 (PMF12 I1).
187 apply (mf_i(PreMonoidalFunctor:=PMF23)).
188 apply functors_preserve_isos.
189 apply (mf_i(PreMonoidalFunctor:=PMF12)).
192 Definition compose_mf_first a : compose_mf >>>> bin_first (compose_mf a) <~~~> bin_first a >>>> compose_mf.
193 set (mf_first(PreMonoidalFunctor:=PMF12) a) as mf_first12.
194 set (mf_first(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_first23.
195 unfold functor_fobj in *; simpl in *.
198 apply (ni_associativity PMF12 PMF23 (- ⋉fobj23 (fobj12 a))).
200 apply (ni_respects PMF12 PMF12 (PMF23 >>>> - ⋉fobj23 (fobj12 a)) (- ⋉fobj12 a >>>> PMF23)).
207 apply (ni_associativity PMF12 (- ⋉fobj12 a) PMF23).
212 eapply (ni_associativity _ PMF12 PMF23).
214 apply ni_respects; [ idtac | apply ni_id ].
219 Definition compose_mf_second a : compose_mf >>>> bin_second (compose_mf a) <~~~> bin_second a >>>> compose_mf.
220 set (mf_second(PreMonoidalFunctor:=PMF12) a) as mf_second12.
221 set (mf_second(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_second23.
222 unfold functor_fobj in *; simpl in *.
225 apply (ni_associativity PMF12 PMF23 (fobj23 (fobj12 a) ⋊-)).
227 apply (ni_respects PMF12 PMF12 (PMF23 >>>> fobj23 (fobj12 a) ⋊-) (fobj12 a ⋊- >>>> PMF23)).
234 apply (ni_associativity PMF12 (fobj12 a ⋊ -) PMF23).
239 eapply (ni_associativity (a ⋊-) PMF12 PMF23).
241 apply ni_respects; [ idtac | apply ni_id ].
246 Lemma compose_assoc_coherence a b c :
247 (#((pmon_assoc (compose_mf a) (fobj23 (fobj12 c))) (compose_mf b)) >>>
248 compose_mf a ⋊ #((compose_mf_second b) c)) >>>
249 #((compose_mf_second a) (b ⊗ c)) ~~
250 (#((compose_mf_second a) b) ⋉ fobj23 (fobj12 c) >>>
251 #((compose_mf_second (a ⊗ b)) c)) >>> compose_mf \ #((pmon_assoc a c) b).
253 set (mf_assoc a b c) as x.
254 set (mf_assoc (fobj12 a) (fobj12 b) (fobj12 c)) as x'.
255 unfold functor_fobj in *.
263 apply iso_shift_left' in x'.
265 unfold compose_mf_second; simpl.
266 unfold functor_fobj; simpl.
267 set (mf_second (fobj12 b)) as m.
268 assert (mf_second (fobj12 b)=m). reflexivity.
270 setoid_rewrite <- fmor_preserves_comp.
271 setoid_rewrite <- fmor_preserves_comp.
272 setoid_rewrite <- fmor_preserves_comp.
273 setoid_rewrite <- fmor_preserves_comp.
274 setoid_rewrite <- fmor_preserves_comp.
275 setoid_rewrite fmor_preserves_id.
276 setoid_rewrite fmor_preserves_id.
277 setoid_rewrite fmor_preserves_id.
278 setoid_rewrite right_identity.
279 setoid_rewrite left_identity.
280 setoid_rewrite left_identity.
281 setoid_rewrite left_identity.
283 set (mf_second (fobj12 (a ⊗ b))) as m''.
284 assert (mf_second (fobj12 (a ⊗ b))=m''). reflexivity.
286 unfold functor_fobj; simpl.
287 setoid_rewrite fmor_preserves_id.
288 setoid_rewrite fmor_preserves_id.
289 setoid_rewrite right_identity.
290 setoid_rewrite left_identity.
291 setoid_rewrite left_identity.
292 setoid_rewrite left_identity.
294 set (mf_second (fobj12 a)) as m'.
295 assert (mf_second (fobj12 a)=m'). reflexivity.
297 setoid_rewrite <- fmor_preserves_comp.
298 setoid_rewrite <- fmor_preserves_comp.
299 setoid_rewrite <- fmor_preserves_comp.
300 setoid_rewrite <- fmor_preserves_comp.
301 setoid_rewrite <- fmor_preserves_comp.
302 setoid_rewrite left_identity.
303 setoid_rewrite left_identity.
304 setoid_rewrite left_identity.
305 setoid_rewrite right_identity.
306 assert (fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 (b ⊗ c)) ~~ id _).
309 setoid_rewrite left_identity.
310 assert ((id (fobj23 (fobj12 a) ⊗ fobj23 (fobj12 b)) ⋉ fobj23 (fobj12 c)) ~~ id _).
313 setoid_rewrite left_identity.
314 assert (id (fobj23 (fobj12 a ⊗ fobj12 b)) ⋉ fobj23 (fobj12 c) ~~ id _).
317 setoid_rewrite left_identity.
319 setoid_rewrite left_identity.
320 assert (id (fobj23 (fobj12 (a ⊗ b))) ⋉ fobj23 (fobj12 c) ~~ id _).
323 setoid_rewrite right_identity.
325 assert ((fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 b)) ⋉ fobj23 (fobj12 c) ~~ id _).
328 setoid_rewrite left_identity.
330 unfold functor_comp in ni_commutes0; simpl in ni_commutes0.
331 unfold functor_comp in ni_commutes; simpl in ni_commutes.
332 unfold functor_comp in ni_commutes1; simpl in ni_commutes1.
335 unfold functor_fobj in *.
337 setoid_rewrite x in x'.
339 set (ni_commutes0 (a )
340 setoid_rewrite fmor_preserves_id.
342 eapply comp_respects.
344 eapply comp_respects.
345 eapply comp_respects.
348 eapply fmor_preserves_id.
349 setoid_rewrite (fmor_preserves_id PMF23).
354 Instance PreMonoidalFunctorsCompose : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12) :=
355 { mf_i := compose_mf_i
357 ; mf_first := compose_mf_first
358 ; mf_second := compose_mf_second }.
359 intros; unfold compose_mf_first; unfold compose_mf_second.
360 set (mf_first (PMF12 a)) as x in *.
361 set (mf_second (PMF12 b)) as y in *.
362 assert (x=mf_first (PMF12 a)). reflexivity.
363 assert (y=mf_second (PMF12 b)). reflexivity.
367 repeat setoid_rewrite left_identity.
368 repeat setoid_rewrite right_identity.
369 set (mf_consistent (PMF12 a) (PMF12 b)) as later.
370 apply comp_respects; try reflexivity.
372 unfold functor_fobj; simpl.
373 set (ni_commutes _ _ (id (fobj12 b))) as x.
374 unfold functor_comp in x.
376 unfold functor_fobj in x.
381 set (ni_commutes0 _ _ (id (fobj12 a))) as x'.
382 unfold functor_comp in x'.
384 unfold functor_fobj in x'.
385 etransitivity; [ idtac | apply x' ].
387 setoid_rewrite fmor_preserves_id.
388 setoid_rewrite fmor_preserves_id.
389 setoid_rewrite right_identity.
390 rewrite <- H in later.
391 rewrite <- H0 in later.
395 apply (mf_consistent a b).
404 unfold compose_mf_first; simpl.
405 set (mf_first (PMF12 b)) as m.
406 assert (mf_first (PMF12 b)=m). reflexivity.
409 unfold functor_fobj; simpl.
410 repeat setoid_rewrite <- fmor_preserves_comp.
411 repeat setoid_rewrite left_identity.
412 repeat setoid_rewrite right_identity.
414 set (mf_cancell b) as y.
415 set (mf_cancell (fobj12 b)) as y'.
416 unfold functor_fobj in *.
417 setoid_rewrite y in y'.
419 setoid_rewrite <- fmor_preserves_comp in y'.
420 setoid_rewrite <- fmor_preserves_comp in y'.
425 repeat setoid_rewrite <- associativity.
426 apply comp_respects; try reflexivity.
427 apply comp_respects; try reflexivity.
428 repeat setoid_rewrite associativity.
429 apply comp_respects; try reflexivity.
431 set (ni_commutes _ _ (id (fobj12 I1))) as x.
432 unfold functor_comp in x.
433 unfold functor_fobj in x.
437 setoid_rewrite fmor_preserves_id.
438 setoid_rewrite fmor_preserves_id.
439 setoid_rewrite right_identity.
444 unfold functor_comp in ni_commutes.
445 simpl in ni_commutes.
449 unfold compose_mf_second; simpl.
450 set (mf_second (PMF12 a)) as m.
451 assert (mf_second (PMF12 a)=m). reflexivity.
454 unfold functor_fobj; simpl.
455 repeat setoid_rewrite <- fmor_preserves_comp.
456 repeat setoid_rewrite left_identity.
457 repeat setoid_rewrite right_identity.
459 set (mf_cancelr a) as y.
460 set (mf_cancelr (fobj12 a)) as y'.
461 unfold functor_fobj in *.
462 setoid_rewrite y in y'.
464 setoid_rewrite <- fmor_preserves_comp in y'.
465 setoid_rewrite <- fmor_preserves_comp in y'.
470 repeat setoid_rewrite <- associativity.
471 apply comp_respects; try reflexivity.
472 apply comp_respects; try reflexivity.
473 repeat setoid_rewrite associativity.
474 apply comp_respects; try reflexivity.
476 set (ni_commutes _ _ (id (fobj12 I1))) as x.
477 unfold functor_comp in x.
478 unfold functor_fobj in x.
482 setoid_rewrite fmor_preserves_id.
483 setoid_rewrite fmor_preserves_id.
484 setoid_rewrite right_identity.
489 unfold functor_comp in ni_commutes.
490 simpl in ni_commutes.
493 apply compose_assoc_coherence.
496 End PreMonoidalFunctorsCompose.
499 (*******************************************************************************)
500 (* Braided and Symmetric Categories *)
502 Class BraidedCat `(mc:PreMonoidalCat) :=
503 { br_niso : forall a, bin_first a <~~~> bin_second a
504 ; br_swap := fun a b => ni_iso (br_niso b) a
505 ; triangleb : forall a:C, #(pmon_cancelr a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell a)
506 ; hexagon1 : forall {a b c}, #(pmon_assoc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc _ _ _)
507 ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc _ _ _) >>> b ⋊ #(br_swap _ _)
508 ; hexagon2 : forall {a b c}, #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc _ _ _)⁻¹
509 ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
512 Class SymmetricCat `(bc:BraidedCat) :=
513 { symcat_swap : forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
517 (* a wide subcategory inherits the premonoidal structure if it includes all of the coherence maps *)
518 Section PreMonoidalWideSubcategory.
520 Context `(pm:PreMonoidalCat(I:=pmI)).
521 Context {Pmor}(S:WideSubcategory pm Pmor).
522 Context (Pmor_first : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (f ⋉ c)).
523 Context (Pmor_second : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (c ⋊ f)).
524 Context (Pmor_assoc : forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)).
525 Context (Pmor_unassoc: forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)⁻¹).
526 Context (Pmor_cancell: forall {a}, Pmor _ _ #(pmon_cancell a)).
527 Context (Pmor_uncancell: forall {a}, Pmor _ _ #(pmon_cancell a)⁻¹).
528 Context (Pmor_cancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)).
529 Context (Pmor_uncancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)⁻¹).
530 Implicit Arguments Pmor_first [[a][b][c][f]].
531 Implicit Arguments Pmor_second [[a][b][c][f]].
533 Definition PreMonoidalWideSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' x a)~~{S}~~>(bin_obj' y a).
534 unfold hom; simpl; intros.
537 exists (bin_first(BinoidalCat:=pm) a \ x0).
538 apply Pmor_first; auto.
541 Definition PreMonoidalWideSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' a x)~~{S}~~>(bin_obj' a y).
542 unfold hom; simpl; intros.
545 exists (bin_second(BinoidalCat:=pm) a \ x0).
546 apply Pmor_second; auto.
549 Instance PreMonoidalWideSubcategory_first (a:S) : Functor S S (fun x => bin_obj' x a) :=
550 { fmor := fun x y f => PreMonoidalWideSubcategory_first_fmor a f }.
551 unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct f'; simpl in *.
552 apply (fmor_respects (bin_first(BinoidalCat:=pm) a)); auto.
553 unfold PreMonoidalWideSubcategory_first_fmor; intros; simpl in *.
554 apply (fmor_preserves_id (bin_first(BinoidalCat:=pm) a)); auto.
555 unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct g; simpl in *.
556 apply (fmor_preserves_comp (bin_first(BinoidalCat:=pm) a)); auto.
559 Instance PreMonoidalWideSubcategory_second (a:S) : Functor S S (fun x => bin_obj' a x) :=
560 { fmor := fun x y f => PreMonoidalWideSubcategory_second_fmor a f }.
561 unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct f'; simpl in *.
562 apply (fmor_respects (bin_second(BinoidalCat:=pm) a)); auto.
563 unfold PreMonoidalWideSubcategory_second_fmor; intros; simpl in *.
564 apply (fmor_preserves_id (bin_second(BinoidalCat:=pm) a)); auto.
565 unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct g; simpl in *.
566 apply (fmor_preserves_comp (bin_second(BinoidalCat:=pm) a)); auto.
569 Instance PreMonoidalWideSubcategory_is_Binoidal : BinoidalCat S bin_obj' :=
570 { bin_first := PreMonoidalWideSubcategory_first
571 ; bin_second := PreMonoidalWideSubcategory_second }.
573 Definition PreMonoidalWideSubcategory_assoc_iso
574 : forall a b c, Isomorphic(C:=S) (bin_obj' (bin_obj' a b) c) (bin_obj' a (bin_obj' b c)).
576 refine {| iso_forward := existT _ _ (Pmor_assoc a b c) ; iso_backward := existT _ _ (Pmor_unassoc a b c) |}.
577 simpl; apply iso_comp1.
578 simpl; apply iso_comp2.
581 Definition PreMonoidalWideSubcategory_assoc
583 (PreMonoidalWideSubcategory_second a >>>> PreMonoidalWideSubcategory_first b) <~~~>
584 (PreMonoidalWideSubcategory_first b >>>> PreMonoidalWideSubcategory_second a).
586 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (PreMonoidalWideSubcategory_second a >>>>
587 PreMonoidalWideSubcategory_first b) (PreMonoidalWideSubcategory_first b >>>>
588 PreMonoidalWideSubcategory_second a) (fun c => PreMonoidalWideSubcategory_assoc_iso a c b)).
590 unfold PreMonoidalWideSubcategory_second_fmor; simpl.
592 set (ni_commutes (pmon_assoc(PreMonoidalCat:=pm) a b) x) as q.
596 Definition PreMonoidalWideSubcategory_assoc_ll
598 PreMonoidalWideSubcategory_second (a⊗b) <~~~>
599 PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a.
601 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
602 (PreMonoidalWideSubcategory_second (a⊗b))
603 (PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a)
604 (fun c => PreMonoidalWideSubcategory_assoc_iso a b c)).
606 unfold PreMonoidalWideSubcategory_second_fmor; simpl.
608 set (ni_commutes (pmon_assoc_ll(PreMonoidalCat:=pm) a b) x) as q.
609 unfold functor_comp in q; simpl in q.
610 set (pmon_coherent_l(PreMonoidalCat:=pm)) as q'.
611 setoid_rewrite q' in q.
615 Definition PreMonoidalWideSubcategory_assoc_rr
617 PreMonoidalWideSubcategory_first (a⊗b) <~~~>
618 PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b.
621 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
622 (PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b)
623 (PreMonoidalWideSubcategory_first (a⊗b))
624 (fun c => PreMonoidalWideSubcategory_assoc_iso c a b)).
626 unfold PreMonoidalWideSubcategory_second_fmor; simpl.
628 set (ni_commutes (pmon_assoc_rr(PreMonoidalCat:=pm) a b) x) as q.
629 unfold functor_comp in q; simpl in q.
630 set (pmon_coherent_r(PreMonoidalCat:=pm)) as q'.
631 setoid_rewrite q' in q.
632 apply iso_shift_right' in q.
633 apply iso_shift_left.
635 setoid_rewrite iso_inv_inv in q.
636 setoid_rewrite associativity.
640 Definition PreMonoidalWideSubcategory_cancelr_iso : forall a, Isomorphic(C:=S) (bin_obj' a pmI) a.
642 refine {| iso_forward := existT _ _ (Pmor_cancelr a) ; iso_backward := existT _ _ (Pmor_uncancelr a) |}.
643 simpl; apply iso_comp1.
644 simpl; apply iso_comp2.
647 Definition PreMonoidalWideSubcategory_cancell_iso : forall a, Isomorphic(C:=S) (bin_obj' pmI a) a.
649 refine {| iso_forward := existT _ _ (Pmor_cancell a) ; iso_backward := existT _ _ (Pmor_uncancell a) |}.
650 simpl; apply iso_comp1.
651 simpl; apply iso_comp2.
654 Definition PreMonoidalWideSubcategory_cancelr : PreMonoidalWideSubcategory_first pmI <~~~> functor_id _.
655 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
656 (PreMonoidalWideSubcategory_first pmI) (functor_id _) PreMonoidalWideSubcategory_cancelr_iso).
658 unfold PreMonoidalWideSubcategory_first_fmor; simpl.
660 apply (ni_commutes (pmon_cancelr(PreMonoidalCat:=pm)) x).
663 Definition PreMonoidalWideSubcategory_cancell : PreMonoidalWideSubcategory_second pmI <~~~> functor_id _.
664 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
665 (PreMonoidalWideSubcategory_second pmI) (functor_id _) PreMonoidalWideSubcategory_cancell_iso).
667 unfold PreMonoidalWideSubcategory_second_fmor; simpl.
669 apply (ni_commutes (pmon_cancell(PreMonoidalCat:=pm)) x).
672 Instance PreMonoidalWideSubcategory_PreMonoidal : PreMonoidalCat PreMonoidalWideSubcategory_is_Binoidal pmI :=
673 { pmon_assoc := PreMonoidalWideSubcategory_assoc
674 ; pmon_assoc_rr := PreMonoidalWideSubcategory_assoc_rr
675 ; pmon_assoc_ll := PreMonoidalWideSubcategory_assoc_ll
676 ; pmon_cancelr := PreMonoidalWideSubcategory_cancelr
677 ; pmon_cancell := PreMonoidalWideSubcategory_cancell
679 apply Build_Pentagon.
680 intros; unfold PreMonoidalWideSubcategory_assoc; simpl.
681 set (pmon_pentagon(PreMonoidalCat:=pm) a b c) as q.
684 apply Build_Triangle.
685 intros; unfold PreMonoidalWideSubcategory_assoc;
686 unfold PreMonoidalWideSubcategory_cancelr; unfold PreMonoidalWideSubcategory_cancell; simpl.
687 set (pmon_triangle(PreMonoidalCat:=pm) a b) as q.
692 set (pmon_triangle(PreMonoidalCat:=pm)) as q.
695 intros; simpl; reflexivity.
696 intros; simpl; reflexivity.
699 apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
700 apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c).
701 apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c).
704 apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
705 apply (pmon_cancelr_central(PreMonoidalCat:=pm) a).
706 apply (pmon_cancelr_central(PreMonoidalCat:=pm) a).
709 apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
710 apply (pmon_cancell_central(PreMonoidalCat:=pm) a).
711 apply (pmon_cancell_central(PreMonoidalCat:=pm) a).
714 End PreMonoidalWideSubcategory.
717 (* a full subcategory inherits the premonoidal structure if it includes the unit object and is closed under object-pairing *)
719 Section PreMonoidalFullSubcategory.
721 Context `(pm:PreMonoidalCat(I:=pmI)).
722 Context {Pobj}(S:FullSubcategory pm Pobj).
723 Context (Pobj_unit:Pobj pmI).
724 Context (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)).
725 Implicit Arguments Pobj_closed [[a][b]].
727 Definition PreMonoidalFullSubcategory_bobj (x y:S) :=
728 existT Pobj _ (Pobj_closed (projT2 x) (projT2 y)).
730 Definition PreMonoidalFullSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
731 (PreMonoidalFullSubcategory_bobj x a)~~{S}~~>(PreMonoidalFullSubcategory_bobj y a).
732 unfold hom; simpl; intros.
733 destruct a as [a apf].
734 destruct x as [x xpf].
735 destruct y as [y ypf].
740 Definition PreMonoidalFullSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
741 (PreMonoidalFullSubcategory_bobj a x)~~{S}~~>(PreMonoidalFullSubcategory_bobj a y).
742 unfold hom; simpl; intros.
743 destruct a as [a apf].
744 destruct x as [x xpf].
745 destruct y as [y ypf].
750 Instance PreMonoidalFullSubcategory_first (a:S)
751 : Functor S S (fun x => PreMonoidalFullSubcategory_bobj x a) :=
752 { fmor := fun x y f => PreMonoidalFullSubcategory_first_fmor a f }.
753 unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0; destruct b; simpl in *.
754 apply (fmor_respects (-⋉x)); auto.
755 unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0; simpl in *.
756 apply (fmor_preserves_id (-⋉x)); auto.
757 unfold PreMonoidalFullSubcategory_first_fmor; intros;
758 destruct a; destruct a0; destruct b; destruct c; simpl in *.
759 apply (fmor_preserves_comp (-⋉x)); auto.
762 Instance PreMonoidalFullSubcategory_second (a:S)
763 : Functor S S (fun x => PreMonoidalFullSubcategory_bobj a x) :=
764 { fmor := fun x y f => PreMonoidalFullSubcategory_second_fmor a f }.
765 unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0; destruct b; simpl in *.
766 apply (fmor_respects (x⋊-)); auto.
767 unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0; simpl in *.
768 apply (fmor_preserves_id (x⋊-)); auto.
769 unfold PreMonoidalFullSubcategory_second_fmor; intros;
770 destruct a; destruct a0; destruct b; destruct c; simpl in *.
771 apply (fmor_preserves_comp (x⋊-)); auto.
774 Instance PreMonoidalFullSubcategory_is_Binoidal : BinoidalCat S PreMonoidalFullSubcategory_bobj :=
775 { bin_first := PreMonoidalFullSubcategory_first
776 ; bin_second := PreMonoidalFullSubcategory_second }.
778 Definition PreMonoidalFullSubcategory_assoc
780 (PreMonoidalFullSubcategory_second a >>>> PreMonoidalFullSubcategory_first b) <~~~>
781 (PreMonoidalFullSubcategory_first b >>>> PreMonoidalFullSubcategory_second a).
784 Definition PreMonoidalFullSubcategory_assoc_ll
786 PreMonoidalFullSubcategory_second (a⊗b) <~~~>
787 PreMonoidalFullSubcategory_second b >>>> PreMonoidalFullSubcategory_second a.
791 Definition PreMonoidalFullSubcategory_assoc_rr
793 PreMonoidalFullSubcategory_first (a⊗b) <~~~>
794 PreMonoidalFullSubcategory_first a >>>> PreMonoidalFullSubcategory_first b.
798 Definition PreMonoidalFullSubcategory_I := existT _ pmI Pobj_unit.
800 Definition PreMonoidalFullSubcategory_cancelr
801 : PreMonoidalFullSubcategory_first PreMonoidalFullSubcategory_I <~~~> functor_id _.
804 Definition PreMonoidalFullSubcategory_cancell
805 : PreMonoidalFullSubcategory_second PreMonoidalFullSubcategory_I <~~~> functor_id _.
808 Instance PreMonoidalFullSubcategory_PreMonoidal
809 : PreMonoidalCat PreMonoidalFullSubcategory_is_Binoidal PreMonoidalFullSubcategory_I :=
810 { pmon_assoc := PreMonoidalFullSubcategory_assoc
811 ; pmon_assoc_rr := PreMonoidalFullSubcategory_assoc_rr
812 ; pmon_assoc_ll := PreMonoidalFullSubcategory_assoc_ll
813 ; pmon_cancelr := PreMonoidalFullSubcategory_cancelr
814 ; pmon_cancell := PreMonoidalFullSubcategory_cancell
817 End PreMonoidalFullSubcategory.