1 Generalizable All Variables.
2 Require Import Notations.
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_I [ Ob Hom C bin_obj' bc I ].
52 Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
53 Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
54 Implicit Arguments pmon_assoc [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
55 Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
57 (* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
58 Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} b a
60 let α := fun a b c => #((pmon_assoc a c) b)
61 in α a b EI >>> _ ⋊ #(pmon_cancelr _) ~~ #(pmon_cancelr _).
65 (* following Mac Lane's hint, we aim for (λ >>> α >>> λ×1)~~(λ >>> λ) *)
66 set (epic _ (iso_epic (pmon_cancelr ((a⊗b)⊗EI)))) as q.
70 (* next, we show that the hint goal above is implied by the bottom-left 1/5th of the big whiteboard diagram *)
71 set (ni_commutes pmon_cancelr (α a b EI)) as q.
72 setoid_rewrite <- associativity.
75 setoid_rewrite associativity.
77 set (ni_commutes pmon_cancelr (a ⋊ #(pmon_cancelr b))) as q.
82 set (ni_commutes pmon_cancelr (#(pmon_cancelr (a⊗b)))) as q.
87 setoid_rewrite <- associativity.
88 apply comp_respects; try reflexivity.
90 (* now we carry out the proof in the whiteboard diagram, starting from the pentagon diagram *)
93 assert (α (a⊗b) EI EI >>> α _ _ _ >>> (_ ⋊ (_ ⋊ #(pmon_cancell _))) ~~ #(pmon_cancelr _) ⋉ _ >>> α _ _ _).
94 set (pmon_triangle (a⊗b) EI) as tria.
99 setoid_rewrite associativity.
100 apply comp_respects; try reflexivity.
101 set (ni_commutes (pmon_assoc_ll a b) #(pmon_cancell EI)) as x.
103 setoid_rewrite pmon_coherent_l in x.
107 assert (((#((pmon_assoc a EI) b) ⋉ EI >>> #((pmon_assoc a EI) (b ⊗ EI))) >>>
108 a ⋊ #((pmon_assoc b EI) EI)) >>> a ⋊ (b ⋊ #(pmon_cancell EI))
109 ~~ α _ _ _ ⋉ _ >>> (_ ⋊ #(pmon_cancelr _)) ⋉ _ >>> α _ _ _).
112 repeat setoid_rewrite associativity.
113 apply comp_respects; try reflexivity.
115 set (ni_commutes (pmon_assoc a EI) (#(pmon_cancelr b) )) as x.
117 setoid_rewrite <- associativity.
122 setoid_rewrite associativity.
123 apply comp_respects; try reflexivity.
124 setoid_rewrite (fmor_preserves_comp (a⋊-)).
125 apply (fmor_respects (a⋊-)).
127 set (pmon_triangle b EI) as tria.
132 set (pmon_pentagon a b EI EI) as penta. unfold pmon_pentagon in penta. simpl in penta.
134 set (@comp_respects _ _ _ _ _ _ _ _ penta (a ⋊ (b ⋊ #(pmon_cancell EI))) (a ⋊ (b ⋊ #(pmon_cancell EI)))) as qq.
136 setoid_rewrite H in qq.
138 setoid_rewrite H0 in qq.
142 apply (monic _ (iso_monic ((pmon_assoc a EI) b))).
148 Class PreMonoidalFunctor
149 `(PM1 : PreMonoidalCat(C:=C1)(I:=I1))
150 `(PM2 : PreMonoidalCat(C:=C2)(I:=I2))
152 (F : Functor C1 C2 fobj ) :=
154 ; mf_i : I2 ≅ mf_F I1
155 ; mf_first : ∀ a, mf_F >>>> bin_first (mf_F a) <~~~> bin_first a >>>> mf_F
156 ; mf_second : ∀ a, mf_F >>>> bin_second (mf_F a) <~~~> bin_second a >>>> mf_F
157 ; mf_consistent : ∀ a b, #(mf_first a b) ~~ #(mf_second b a)
158 ; mf_center : forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
159 ; mf_cancell : ∀ b, #(pmon_cancell _) ~~ #mf_i ⋉ _ >>> #(mf_first b I1) >>> mf_F \ #(pmon_cancell b)
160 ; mf_cancelr : ∀ a, #(pmon_cancelr _) ~~ _ ⋊ #mf_i >>> #(mf_second a I1) >>> mf_F \ #(pmon_cancelr a)
161 ; mf_assoc : ∀ a b c, #(pmon_assoc _ _ _) >>> _ ⋊ #(mf_first _ _) >>> #(mf_second _ _) ~~
162 #(mf_second _ _) ⋉ _ >>> #(mf_first _ _) >>> mf_F \ #(pmon_assoc a c b)
164 Coercion mf_F : PreMonoidalFunctor >-> Functor.
166 Section PreMonoidalFunctorsCompose.
168 `{PM1 :PreMonoidalCat(C:=C1)(I:=I1)}
169 `{PM2 :PreMonoidalCat(C:=C2)(I:=I2)}
171 {PMFF12:Functor C1 C2 fobj12 }
172 (PMF12 :PreMonoidalFunctor PM1 PM2 PMFF12)
173 `{PM3 :PreMonoidalCat(C:=C3)(I:=I3)}
175 {PMFF23:Functor C2 C3 fobj23 }
176 (PMF23 :PreMonoidalFunctor PM2 PM3 PMFF23).
178 Definition compose_mf := PMF12 >>>> PMF23.
180 Definition compose_mf_i : I3 ≅ PMF23 (PMF12 I1).
182 apply (mf_i(PreMonoidalFunctor:=PMF23)).
183 apply functors_preserve_isos.
184 apply (mf_i(PreMonoidalFunctor:=PMF12)).
187 Definition compose_mf_first a : compose_mf >>>> bin_first (compose_mf a) <~~~> bin_first a >>>> compose_mf.
188 set (mf_first(PreMonoidalFunctor:=PMF12) a) as mf_first12.
189 set (mf_first(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_first23.
190 unfold functor_fobj in *; simpl in *.
193 apply (ni_associativity PMF12 PMF23 (- ⋉fobj23 (fobj12 a))).
195 apply (ni_respects1 PMF12 (PMF23 >>>> - ⋉fobj23 (fobj12 a)) (- ⋉fobj12 a >>>> PMF23)).
201 apply (ni_associativity PMF12 (- ⋉fobj12 a) PMF23).
206 eapply (ni_associativity _ PMF12 PMF23).
213 Definition compose_mf_second a : compose_mf >>>> bin_second (compose_mf a) <~~~> bin_second a >>>> compose_mf.
214 set (mf_second(PreMonoidalFunctor:=PMF12) a) as mf_second12.
215 set (mf_second(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_second23.
216 unfold functor_fobj in *; simpl in *.
219 apply (ni_associativity PMF12 PMF23 (fobj23 (fobj12 a) ⋊-)).
221 apply (ni_respects1 PMF12 (PMF23 >>>> fobj23 (fobj12 a) ⋊-) (fobj12 a ⋊- >>>> PMF23)).
227 apply (ni_associativity PMF12 (fobj12 a ⋊ -) PMF23).
232 eapply (ni_associativity (a ⋊-) PMF12 PMF23).
239 (* this proof is really gross; I will write a better one some other day *)
240 Lemma mf_associativity_comp :
242 (#((pmon_assoc (compose_mf a) (compose_mf c)) (fobj23 (fobj12 b))) >>>
243 compose_mf a ⋊ #((compose_mf_first c) b)) >>>
244 #((compose_mf_second a) (b ⊗ c)) ~~
245 (#((compose_mf_second a) b) ⋉ compose_mf c >>>
246 #((compose_mf_first c) (a ⊗ b))) >>> compose_mf \ #((pmon_assoc a c) b).
248 unfold compose_mf_second; simpl.
249 unfold compose_mf_first; simpl.
250 unfold functor_comp; simpl.
252 unfold functor_fobj; simpl.
254 set (mf_first (fobj12 c)) as m'.
255 assert (mf_first (fobj12 c)=m'). reflexivity.
258 set (mf_second (fobj12 a)) as m.
259 assert (mf_second (fobj12 a)=m). reflexivity.
262 Implicit Arguments id [[Ob][Hom][Category][a]].
267 repeat setoid_rewrite <- fmor_preserves_comp.
268 repeat setoid_rewrite fmor_preserves_id.
269 repeat setoid_rewrite left_identity.
270 repeat setoid_rewrite right_identity.
274 repeat setoid_rewrite <- fmor_preserves_comp.
275 repeat setoid_rewrite fmor_preserves_id.
276 repeat setoid_rewrite left_identity.
277 repeat setoid_rewrite right_identity.
280 assert ( (#((pmon_assoc (fobj23 (fobj12 a)) (fobj23 (fobj12 c)))
281 (fobj23 (fobj12 b))) >>>
284 (#(ni_iso (fobj12 b)) >>> ( (PMF23 \ #((mf_first c) b) ))))) >>>
286 (#(ni_iso0 (fobj12 (b ⊗ c))) >>>
287 ((PMF23 \ #((mf_second a) (b ⊗ c)))))) ~~
289 (#(ni_iso0 (fobj12 b)) >>> ( (PMF23 \ #((mf_second a) b) ))))
290 ⋉ fobj23 (fobj12 c) >>>
292 (#(ni_iso (fobj12 (a ⊗ b))) >>>
293 ( (PMF23 \ #((mf_first c) (a ⊗ b))))))) >>>
294 PMF23 \ (PMF12 \ #((pmon_assoc a c) b))
297 repeat setoid_rewrite associativity.
298 setoid_rewrite (fmor_preserves_comp PMF23).
299 unfold functor_comp in *.
300 unfold functor_fobj in *.
302 rename ni_commutes into ni_commutes7.
303 set (mf_assoc(PreMonoidalFunctor:=PMF12)) as q.
304 set (ni_commutes7 _ _ (#((mf_second a) b))) as q'.
306 repeat setoid_rewrite associativity.
308 setoid_rewrite <- (fmor_preserves_comp (-⋉ fobj23 (fobj12 c))).
309 repeat setoid_rewrite <- associativity.
310 setoid_rewrite juggle1.
311 setoid_rewrite <- q'.
312 repeat setoid_rewrite associativity.
313 setoid_rewrite fmor_preserves_comp.
315 unfold functor_fobj in *.
317 repeat setoid_rewrite <- associativity.
320 repeat setoid_rewrite <- fmor_preserves_comp.
321 repeat setoid_rewrite <- associativity.
322 apply comp_respects; try reflexivity.
324 set (mf_assoc(PreMonoidalFunctor:=PMF23) (fobj12 a) (fobj12 b) (fobj12 c)) as q.
325 unfold functor_fobj in *.
331 repeat setoid_rewrite <- associativity.
332 repeat setoid_rewrite <- associativity in q.
335 unfold functor_fobj; simpl.
337 repeat setoid_rewrite associativity.
338 apply comp_respects; try reflexivity.
339 apply comp_respects; try reflexivity.
342 repeat setoid_rewrite associativity.
343 repeat setoid_rewrite associativity in H1.
344 repeat setoid_rewrite <- fmor_preserves_comp in H1.
345 repeat setoid_rewrite associativity in H1.
348 Implicit Arguments id [[Ob][Hom][Category]].
350 (* this proof is really gross; I will write a better one some other day *)
351 Instance PreMonoidalFunctorsCompose : PreMonoidalFunctor PM1 PM3 compose_mf :=
352 { mf_i := compose_mf_i
353 ; mf_first := compose_mf_first
354 ; mf_second := compose_mf_second }.
356 intros; unfold compose_mf_first; unfold compose_mf_second.
357 set (mf_first (PMF12 a)) as x in *.
358 set (mf_second (PMF12 b)) as y in *.
359 assert (x=mf_first (PMF12 a)). reflexivity.
360 assert (y=mf_second (PMF12 b)). reflexivity.
364 repeat setoid_rewrite left_identity.
365 repeat setoid_rewrite right_identity.
366 set (mf_consistent (PMF12 a) (PMF12 b)) as later.
367 apply comp_respects; try reflexivity.
368 rewrite <- H in later.
369 rewrite <- H0 in later.
382 unfold compose_mf_first; simpl.
383 set (mf_first (PMF12 b)) as m.
384 assert (mf_first (PMF12 b)=m). reflexivity.
387 unfold functor_fobj; simpl.
388 repeat setoid_rewrite <- fmor_preserves_comp.
389 repeat setoid_rewrite left_identity.
390 repeat setoid_rewrite right_identity.
392 set (mf_cancell b) as y.
393 set (mf_cancell (fobj12 b)) as y'.
394 unfold functor_fobj in *.
395 setoid_rewrite y in y'.
397 setoid_rewrite <- fmor_preserves_comp in y'.
398 setoid_rewrite <- fmor_preserves_comp in y'.
403 repeat setoid_rewrite <- associativity.
404 apply comp_respects; try reflexivity.
405 apply comp_respects; try reflexivity.
406 repeat setoid_rewrite associativity.
407 apply comp_respects; try reflexivity.
409 set (ni_commutes _ _ #mf_i) as x.
410 unfold functor_comp in x.
411 unfold functor_fobj in x.
418 unfold compose_mf_second; simpl.
419 set (mf_second (PMF12 a)) as m.
420 assert (mf_second (PMF12 a)=m). reflexivity.
423 unfold functor_fobj; simpl.
424 repeat setoid_rewrite <- fmor_preserves_comp.
425 repeat setoid_rewrite left_identity.
426 repeat setoid_rewrite right_identity.
428 set (mf_cancelr a) as y.
429 set (mf_cancelr (fobj12 a)) as y'.
430 unfold functor_fobj in *.
431 setoid_rewrite y in y'.
433 setoid_rewrite <- fmor_preserves_comp in y'.
434 setoid_rewrite <- fmor_preserves_comp in y'.
439 repeat setoid_rewrite <- associativity.
440 apply comp_respects; try reflexivity.
441 apply comp_respects; try reflexivity.
442 repeat setoid_rewrite associativity.
443 apply comp_respects; try reflexivity.
445 set (ni_commutes _ _ #mf_i) as x.
446 unfold functor_comp in x.
447 unfold functor_fobj in x.
453 apply mf_associativity_comp.
457 End PreMonoidalFunctorsCompose.
458 Notation "a >>⊗>> b" := (PreMonoidalFunctorsCompose a b).
461 (*******************************************************************************)
462 (* Braided and Symmetric Categories *)
464 Class BraidedCat `(mc:PreMonoidalCat) :=
465 { br_niso : forall a, bin_first a <~~~> bin_second a
466 ; br_swap := fun a b => ni_iso (br_niso b) a
467 ; triangleb : forall a:C, #(pmon_cancelr a) ~~ #(br_swap a (pmon_I mc)) >>> #(pmon_cancell a)
468 ; hexagon1 : forall {a b c}, #(pmon_assoc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc _ _ _)
469 ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc _ _ _) >>> b ⋊ #(br_swap _ _)
470 ; hexagon2 : forall {a b c}, #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc _ _ _)⁻¹
471 ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
474 Class SymmetricCat `(bc:BraidedCat) :=
475 { symcat_swap : forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
479 (* a wide subcategory inherits the premonoidal structure if it includes all of the coherence maps *)
480 Section PreMonoidalWideSubcategory.
482 Context `(pm:PreMonoidalCat(I:=pmI)).
483 Context {Pmor}(S:WideSubcategory pm Pmor).
484 Context (Pmor_first : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (f ⋉ c)).
485 Context (Pmor_second : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (c ⋊ f)).
486 Context (Pmor_assoc : forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)).
487 Context (Pmor_unassoc: forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)⁻¹).
488 Context (Pmor_cancell: forall {a}, Pmor _ _ #(pmon_cancell a)).
489 Context (Pmor_uncancell: forall {a}, Pmor _ _ #(pmon_cancell a)⁻¹).
490 Context (Pmor_cancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)).
491 Context (Pmor_uncancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)⁻¹).
492 Implicit Arguments Pmor_first [[a][b][c][f]].
493 Implicit Arguments Pmor_second [[a][b][c][f]].
495 Definition PreMonoidalWideSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' x a)~~{S}~~>(bin_obj' y a).
496 unfold hom; simpl; intros.
499 exists (bin_first(BinoidalCat:=pm) a \ x0).
500 apply Pmor_first; auto.
503 Definition PreMonoidalWideSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' a x)~~{S}~~>(bin_obj' a y).
504 unfold hom; simpl; intros.
507 exists (bin_second(BinoidalCat:=pm) a \ x0).
508 apply Pmor_second; auto.
511 Instance PreMonoidalWideSubcategory_first (a:S) : Functor S S (fun x => bin_obj' x a) :=
512 { fmor := fun x y f => PreMonoidalWideSubcategory_first_fmor a f }.
513 unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct f'; simpl in *.
514 apply (fmor_respects (bin_first(BinoidalCat:=pm) a)); auto.
515 unfold PreMonoidalWideSubcategory_first_fmor; intros; simpl in *.
516 apply (fmor_preserves_id (bin_first(BinoidalCat:=pm) a)); auto.
517 unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct g; simpl in *.
518 apply (fmor_preserves_comp (bin_first(BinoidalCat:=pm) a)); auto.
521 Instance PreMonoidalWideSubcategory_second (a:S) : Functor S S (fun x => bin_obj' a x) :=
522 { fmor := fun x y f => PreMonoidalWideSubcategory_second_fmor a f }.
523 unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct f'; simpl in *.
524 apply (fmor_respects (bin_second(BinoidalCat:=pm) a)); auto.
525 unfold PreMonoidalWideSubcategory_second_fmor; intros; simpl in *.
526 apply (fmor_preserves_id (bin_second(BinoidalCat:=pm) a)); auto.
527 unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct g; simpl in *.
528 apply (fmor_preserves_comp (bin_second(BinoidalCat:=pm) a)); auto.
531 Instance PreMonoidalWideSubcategory_is_Binoidal : BinoidalCat S bin_obj' :=
532 { bin_first := PreMonoidalWideSubcategory_first
533 ; bin_second := PreMonoidalWideSubcategory_second }.
535 Definition PreMonoidalWideSubcategory_assoc_iso
536 : forall a b c, Isomorphic(C:=S) (bin_obj' (bin_obj' a b) c) (bin_obj' a (bin_obj' b c)).
538 refine {| iso_forward := existT _ _ (Pmor_assoc a b c) ; iso_backward := existT _ _ (Pmor_unassoc a b c) |}.
539 simpl; apply iso_comp1.
540 simpl; apply iso_comp2.
543 Definition PreMonoidalWideSubcategory_assoc
545 (PreMonoidalWideSubcategory_second a >>>> PreMonoidalWideSubcategory_first b) <~~~>
546 (PreMonoidalWideSubcategory_first b >>>> PreMonoidalWideSubcategory_second a).
548 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (PreMonoidalWideSubcategory_second a >>>>
549 PreMonoidalWideSubcategory_first b) (PreMonoidalWideSubcategory_first b >>>>
550 PreMonoidalWideSubcategory_second a) (fun c => PreMonoidalWideSubcategory_assoc_iso a c b)).
552 unfold PreMonoidalWideSubcategory_second_fmor; simpl.
554 set (ni_commutes (pmon_assoc(PreMonoidalCat:=pm) a b) x) as q.
558 Definition PreMonoidalWideSubcategory_assoc_ll
560 PreMonoidalWideSubcategory_second (a⊗b) <~~~>
561 PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a.
563 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
564 (PreMonoidalWideSubcategory_second (a⊗b))
565 (PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a)
566 (fun c => PreMonoidalWideSubcategory_assoc_iso a b c)).
568 unfold PreMonoidalWideSubcategory_second_fmor; simpl.
570 set (ni_commutes (pmon_assoc_ll(PreMonoidalCat:=pm) a b) x) as q.
571 unfold functor_comp in q; simpl in q.
572 set (pmon_coherent_l(PreMonoidalCat:=pm)) as q'.
573 setoid_rewrite q' in q.
577 Definition PreMonoidalWideSubcategory_assoc_rr
579 PreMonoidalWideSubcategory_first (a⊗b) <~~~>
580 PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b.
583 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
584 (PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b)
585 (PreMonoidalWideSubcategory_first (a⊗b))
586 (fun c => PreMonoidalWideSubcategory_assoc_iso c a b)).
588 unfold PreMonoidalWideSubcategory_second_fmor; simpl.
590 set (ni_commutes (pmon_assoc_rr(PreMonoidalCat:=pm) a b) x) as q.
591 unfold functor_comp in q; simpl in q.
592 set (pmon_coherent_r(PreMonoidalCat:=pm)) as q'.
593 setoid_rewrite q' in q.
594 apply iso_shift_right' in q.
595 apply iso_shift_left.
597 setoid_rewrite iso_inv_inv in q.
598 setoid_rewrite associativity.
602 Definition PreMonoidalWideSubcategory_cancelr_iso : forall a, Isomorphic(C:=S) (bin_obj' a pmI) a.
604 refine {| iso_forward := existT _ _ (Pmor_cancelr a) ; iso_backward := existT _ _ (Pmor_uncancelr a) |}.
605 simpl; apply iso_comp1.
606 simpl; apply iso_comp2.
609 Definition PreMonoidalWideSubcategory_cancell_iso : forall a, Isomorphic(C:=S) (bin_obj' pmI a) a.
611 refine {| iso_forward := existT _ _ (Pmor_cancell a) ; iso_backward := existT _ _ (Pmor_uncancell a) |}.
612 simpl; apply iso_comp1.
613 simpl; apply iso_comp2.
616 Definition PreMonoidalWideSubcategory_cancelr : PreMonoidalWideSubcategory_first pmI <~~~> functor_id _.
617 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
618 (PreMonoidalWideSubcategory_first pmI) (functor_id _) PreMonoidalWideSubcategory_cancelr_iso).
620 unfold PreMonoidalWideSubcategory_first_fmor; simpl.
622 apply (ni_commutes (pmon_cancelr(PreMonoidalCat:=pm)) x).
625 Definition PreMonoidalWideSubcategory_cancell : PreMonoidalWideSubcategory_second pmI <~~~> functor_id _.
626 apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
627 (PreMonoidalWideSubcategory_second pmI) (functor_id _) PreMonoidalWideSubcategory_cancell_iso).
629 unfold PreMonoidalWideSubcategory_second_fmor; simpl.
631 apply (ni_commutes (pmon_cancell(PreMonoidalCat:=pm)) x).
634 Instance PreMonoidalWideSubcategory_PreMonoidal : PreMonoidalCat PreMonoidalWideSubcategory_is_Binoidal pmI :=
635 { pmon_assoc := PreMonoidalWideSubcategory_assoc
636 ; pmon_assoc_rr := PreMonoidalWideSubcategory_assoc_rr
637 ; pmon_assoc_ll := PreMonoidalWideSubcategory_assoc_ll
638 ; pmon_cancelr := PreMonoidalWideSubcategory_cancelr
639 ; pmon_cancell := PreMonoidalWideSubcategory_cancell
641 apply Build_Pentagon.
642 intros; unfold PreMonoidalWideSubcategory_assoc; simpl.
643 set (pmon_pentagon(PreMonoidalCat:=pm) a b c) as q.
646 apply Build_Triangle.
647 intros; unfold PreMonoidalWideSubcategory_assoc;
648 unfold PreMonoidalWideSubcategory_cancelr; unfold PreMonoidalWideSubcategory_cancell; simpl.
649 set (pmon_triangle(PreMonoidalCat:=pm) a b) as q.
654 set (pmon_triangle(PreMonoidalCat:=pm)) as q.
657 intros; simpl; reflexivity.
658 intros; simpl; reflexivity.
661 apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
662 apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c).
663 apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c).
666 apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
667 apply (pmon_cancelr_central(PreMonoidalCat:=pm) a).
668 apply (pmon_cancelr_central(PreMonoidalCat:=pm) a).
671 apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
672 apply (pmon_cancell_central(PreMonoidalCat:=pm) a).
673 apply (pmon_cancell_central(PreMonoidalCat:=pm) a).
676 End PreMonoidalWideSubcategory.
678 Section IsoFullSubCategory.
679 Context `{C:Category}.
680 Context {Pobj}(S:FullSubcategory C Pobj).
682 Definition iso_full {a b:C}(i:a≅b)(pa:Pobj a)(pb:Pobj b) : (existT _ _ pa) ≅ (existT _ _ pb).
683 set (#i : existT Pobj a pa ~~{S}~~> existT Pobj b pb) as i1.
684 set (iso_backward i : existT Pobj b pb ~~{S}~~> existT Pobj a pa) as i2.
685 refine {| iso_forward := i1 ; iso_backward := i2 |}.
686 unfold i1; unfold i2; unfold hom; simpl.
688 unfold i1; unfold i2; unfold hom; simpl.
691 End IsoFullSubCategory.
693 (* a full subcategory inherits the premonoidal structure if it includes the unit object and is closed under object-pairing *)
694 Section PreMonoidalFullSubcategory.
696 Context `(pm:PreMonoidalCat(I:=pmI)).
697 Context {Pobj}(S:FullSubcategory pm Pobj).
699 Context (Pobj_unit:Pobj pmI).
700 Context (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)).
701 Implicit Arguments Pobj_closed [[a][b]].
703 Definition PreMonoidalFullSubcategory_bobj (x y:S) :=
704 existT Pobj _ (Pobj_closed (projT2 x) (projT2 y)).
706 Definition PreMonoidalFullSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
707 (PreMonoidalFullSubcategory_bobj x a)~~{S}~~>(PreMonoidalFullSubcategory_bobj y a).
708 unfold hom; simpl; intros.
709 destruct a as [a apf].
710 destruct x as [x xpf].
711 destruct y as [y ypf].
716 Definition PreMonoidalFullSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
717 (PreMonoidalFullSubcategory_bobj a x)~~{S}~~>(PreMonoidalFullSubcategory_bobj a y).
718 unfold hom; simpl; intros.
719 destruct a as [a apf].
720 destruct x as [x xpf].
721 destruct y as [y ypf].
726 Instance PreMonoidalFullSubcategory_first (a:S)
727 : Functor S S (fun x => PreMonoidalFullSubcategory_bobj x a) :=
728 { fmor := fun x y f => PreMonoidalFullSubcategory_first_fmor a f }.
729 unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0; destruct b; simpl in *.
730 apply (fmor_respects (-⋉x)); auto.
731 unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0; simpl in *.
732 apply (fmor_preserves_id (-⋉x)); auto.
733 unfold PreMonoidalFullSubcategory_first_fmor; intros;
734 destruct a; destruct a0; destruct b; destruct c; simpl in *.
735 apply (fmor_preserves_comp (-⋉x)); auto.
738 Instance PreMonoidalFullSubcategory_second (a:S)
739 : Functor S S (fun x => PreMonoidalFullSubcategory_bobj a x) :=
740 { fmor := fun x y f => PreMonoidalFullSubcategory_second_fmor a f }.
741 unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0; destruct b; simpl in *.
742 apply (fmor_respects (x⋊-)); auto.
743 unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0; simpl in *.
744 apply (fmor_preserves_id (x⋊-)); auto.
745 unfold PreMonoidalFullSubcategory_second_fmor; intros;
746 destruct a; destruct a0; destruct b; destruct c; simpl in *.
747 apply (fmor_preserves_comp (x⋊-)); auto.
750 Instance PreMonoidalFullSubcategory_is_Binoidal : BinoidalCat S PreMonoidalFullSubcategory_bobj :=
751 { bin_first := PreMonoidalFullSubcategory_first
752 ; bin_second := PreMonoidalFullSubcategory_second }.
754 Definition central_full {a b}(f:a~~{S}~~>b)
755 : @CentralMorphism _ _ _ _ pm (projT1 a) (projT1 b) f -> CentralMorphism f.
757 apply Build_CentralMorphism; simpl.
759 destruct a as [a apf].
760 destruct b as [b bpf].
761 destruct c as [c cpf].
762 destruct d as [d dpf].
766 destruct a as [a apf].
767 destruct b as [b bpf].
768 destruct c as [c cpf].
769 destruct d as [d dpf].
774 Notation "a ⊕ b" := (Pobj_closed a b).
775 Definition PreMonoidalFullSubcategory_assoc
777 (PreMonoidalFullSubcategory_second a >>>> PreMonoidalFullSubcategory_first b) <~~~>
778 (PreMonoidalFullSubcategory_first b >>>> PreMonoidalFullSubcategory_second a).
780 refine {| ni_iso := (fun (c:S) => iso_full S (pmon_assoc(PreMonoidalCat:=pm) _ _ _)
781 ((projT2 a⊕projT2 c)⊕projT2 b)
782 (projT2 a⊕(projT2 c⊕projT2 b))) |}.
784 destruct a as [a apf].
785 destruct b as [b bpf].
786 destruct A as [A Apf].
787 destruct B as [B Bpf].
788 apply (ni_commutes (pmon_assoc(PreMonoidalCat:=pm) a b) f).
791 Definition PreMonoidalFullSubcategory_assoc_ll
793 PreMonoidalFullSubcategory_second (a⊗b) <~~~>
794 PreMonoidalFullSubcategory_second b >>>> PreMonoidalFullSubcategory_second a.
796 refine {| ni_iso := (fun (c:S) => iso_full S (pmon_assoc_ll(PreMonoidalCat:=pm) _ _ _)
797 ((projT2 a⊕projT2 b)⊕projT2 c)
798 (projT2 a⊕(projT2 b⊕projT2 c))
801 destruct a as [a apf].
802 destruct b as [b bpf].
803 destruct A as [A Apf].
804 destruct B as [B Bpf].
805 apply (ni_commutes (pmon_assoc_ll(PreMonoidalCat:=pm) a b) f).
808 Definition PreMonoidalFullSubcategory_assoc_rr
810 PreMonoidalFullSubcategory_first (a⊗b) <~~~>
811 PreMonoidalFullSubcategory_first a >>>> PreMonoidalFullSubcategory_first b.
813 refine {| ni_iso := (fun (c:S) => iso_full S (pmon_assoc_rr(PreMonoidalCat:=pm) _ _ _)
814 (projT2 c⊕(projT2 a⊕projT2 b))
815 ((projT2 c⊕projT2 a)⊕projT2 b)
818 destruct a as [a apf].
819 destruct b as [b bpf].
820 destruct A as [A Apf].
821 destruct B as [B Bpf].
822 apply (ni_commutes (pmon_assoc_rr(PreMonoidalCat:=pm) a b) f).
825 Definition PreMonoidalFullSubcategory_I := existT _ pmI Pobj_unit.
827 Definition PreMonoidalFullSubcategory_cancelr_iso A
828 : (fun x : S => PreMonoidalFullSubcategory_bobj x (existT Pobj pmI Pobj_unit)) A ≅ (fun x : S => x) A.
834 Definition PreMonoidalFullSubcategory_cancelr
835 : PreMonoidalFullSubcategory_first PreMonoidalFullSubcategory_I <~~~> functor_id _.
837 refine {| ni_iso := PreMonoidalFullSubcategory_cancelr_iso |}.
839 destruct A as [A Apf].
840 destruct B as [B Bpf].
842 apply (ni_commutes (pmon_cancelr(PreMonoidalCat:=pm)) f).
845 Definition PreMonoidalFullSubcategory_cancell_iso A
846 : (fun x : S => PreMonoidalFullSubcategory_bobj (existT Pobj pmI Pobj_unit) x) A ≅ (fun x : S => x) A.
852 Definition PreMonoidalFullSubcategory_cancell
853 : PreMonoidalFullSubcategory_second PreMonoidalFullSubcategory_I <~~~> functor_id _.
855 refine {| ni_iso := PreMonoidalFullSubcategory_cancell_iso |}.
857 destruct A as [A Apf].
858 destruct B as [B Bpf].
860 apply (ni_commutes (pmon_cancell(PreMonoidalCat:=pm)) f).
863 Instance PreMonoidalFullSubcategory_PreMonoidal
864 : PreMonoidalCat PreMonoidalFullSubcategory_is_Binoidal PreMonoidalFullSubcategory_I :=
865 { pmon_assoc := PreMonoidalFullSubcategory_assoc
866 ; pmon_assoc_rr := PreMonoidalFullSubcategory_assoc_rr
867 ; pmon_assoc_ll := PreMonoidalFullSubcategory_assoc_ll
868 ; pmon_cancelr := PreMonoidalFullSubcategory_cancelr
869 ; pmon_cancell := PreMonoidalFullSubcategory_cancell
871 apply Build_Pentagon.
873 destruct a as [a apf].
874 destruct b as [b bpf].
875 destruct c as [c cpf].
876 destruct d as [d dpf].
878 apply (pmon_pentagon(PreMonoidalCat:=pm)).
880 apply Build_Triangle.
882 destruct a as [a apf].
883 destruct b as [b bpf].
885 apply (pmon_triangle(PreMonoidalCat:=pm)).
887 apply (pmon_triangle(PreMonoidalCat:=pm)).
890 destruct a as [a apf].
891 destruct c as [c cpf].
892 destruct d as [d dpf].
894 apply (pmon_coherent_r(PreMonoidalCat:=pm)).
897 destruct a as [a apf].
898 destruct c as [c cpf].
899 destruct d as [d dpf].
901 apply (pmon_coherent_l(PreMonoidalCat:=pm)).
904 destruct a as [a apf].
905 destruct b as [b bpf].
906 destruct c as [c cpf].
910 apply (pmon_assoc_central(PreMonoidalCat:=pm)).
913 destruct a as [a apf].
917 apply (pmon_cancelr_central(PreMonoidalCat:=pm)).
920 destruct a as [a apf].
924 apply (pmon_cancell_central(PreMonoidalCat:=pm)).
927 End PreMonoidalFullSubcategory.