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 ProductCategories_ch1_6_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.
13 (******************************************************************************)
14 (* Chapter 7.8: (Pre)Monoidal Categories *)
15 (******************************************************************************)
19 ( bin_obj' : C -> C -> C ) :=
20 { bin_obj := bin_obj' where "a ⊗ b" := (bin_obj a b)
21 ; bin_first : forall a:C, Functor C C (fun x => x⊗a)
22 ; bin_second : forall a:C, Functor C C (fun x => a⊗x)
25 Coercion bin_c : BinoidalCat >-> Category.
26 Notation "a ⊗ b" := (@bin_obj _ _ _ _ _ a b) : category_scope.
27 Notation "C ⋊ f" := (@fmor _ _ _ _ _ _ _ (@bin_second _ _ _ _ _ C) _ _ f) : category_scope.
28 Notation "g ⋉ C" := (@fmor _ _ _ _ _ _ _ (@bin_first _ _ _ _ _ C) _ _ g) : category_scope.
29 Notation "C ⋊ -" := (@bin_second _ _ _ _ _ C) : category_scope.
30 Notation "- ⋉ C" := (@bin_first _ _ _ _ _ C) : category_scope.
32 Class CentralMorphism `{BinoidalCat}`(f:a~>b) : Prop :=
33 { centralmor_first : forall `(g:c~>d), (f ⋉ _ >>> _ ⋊ g) ~~ (_ ⋊ g >>> f ⋉ _)
34 ; centralmor_second : forall `(g:c~>d), (g ⋉ _ >>> _ ⋊ f) ~~ (_ ⋊ f >>> g ⋉ _)
37 Lemma central_morphisms_compose `{bc:BinoidalCat}{a b c}(f:a~>b)(g:b~>c)
38 : CentralMorphism f -> CentralMorphism g -> CentralMorphism (f >>> g).
40 apply Build_CentralMorphism; intros.
41 abstract (setoid_rewrite <- (fmor_preserves_comp(bin_first c0));
42 setoid_rewrite associativity;
43 setoid_rewrite centralmor_first;
44 setoid_rewrite <- associativity;
45 setoid_rewrite centralmor_first;
46 setoid_rewrite associativity;
47 setoid_rewrite <- (fmor_preserves_comp(bin_first d));
49 abstract (setoid_rewrite <- (fmor_preserves_comp(bin_second d));
50 setoid_rewrite <- associativity;
51 setoid_rewrite centralmor_second;
52 setoid_rewrite associativity;
53 setoid_rewrite centralmor_second;
54 setoid_rewrite <- associativity;
55 setoid_rewrite <- (fmor_preserves_comp(bin_second c0));
59 (* the central morphisms of a category constitute a subcategory *)
60 Definition Center `(bc:BinoidalCat) : SubCategory bc (fun _ => True) (fun _ _ _ _ f => CentralMorphism f).
61 apply Build_SubCategory; intros.
62 apply Build_CentralMorphism; intros.
63 abstract (setoid_rewrite (fmor_preserves_id(bin_first c));
64 setoid_rewrite (fmor_preserves_id(bin_first d));
65 setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
66 abstract (setoid_rewrite (fmor_preserves_id(bin_second c));
67 setoid_rewrite (fmor_preserves_id(bin_second d));
68 setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
69 apply central_morphisms_compose; auto.
72 Class CommutativeCat `(BinoidalCat) :=
73 { commutative_central : forall `(f:a~>b), CentralMorphism f
74 ; commutative_morprod := fun `(f:a~>b)`(g:a~>b) => f ⋉ _ >>> _ ⋊ g
76 Notation "f × g" := (commutative_morprod f g).
78 Section BinoidalCat_from_Bifunctor.
79 Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).
80 Definition BinoidalCat_from_Bifunctor_first (a:C) : Functor C C (fun b => Fobj (pair_obj b a)).
81 apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
82 @fmor _ _ _ _ _ _ _ F (pair_obj a0 a) (pair_obj b a) (pair_mor (pair_obj a0 a) (pair_obj b a) f (id a)))); intros; simpl;
83 [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
84 | abstract (set (fmor_preserves_id(F)) as q; apply q)
85 | abstract (etransitivity;
86 [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
87 | set (fmor_respects(F)) as q; apply q ];
88 split; simpl; auto) ].
90 Definition BinoidalCat_from_Bifunctor_second (a:C) : Functor C C (fun b => Fobj (pair_obj a b)).
91 apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
92 @fmor _ _ _ _ _ _ _ F (pair_obj a a0) (pair_obj a b) (pair_mor (pair_obj a a0) (pair_obj a b) (id a) f))); intros;
93 [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
94 | abstract (set (fmor_preserves_id(F)) as q; apply q)
95 | abstract (etransitivity;
96 [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
97 | set (fmor_respects(F)) as q; apply q ];
98 split; simpl; auto) ].
101 Definition BinoidalCat_from_Bifunctor : BinoidalCat C (fun a b => Fobj (pair_obj a b)).
102 refine {| bin_first := BinoidalCat_from_Bifunctor_first
103 ; bin_second := BinoidalCat_from_Bifunctor_second
107 Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat BinoidalCat_from_Bifunctor.
108 abstract (intros; apply Build_CommutativeCat; intros; apply Build_CentralMorphism; intros; simpl; (
109 etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ]; symmetry;
110 etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ];
111 apply (fmor_respects(F));
113 [ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
114 | etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
117 End BinoidalCat_from_Bifunctor.
120 Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
124 ; pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
125 ; pmon_cancelr : (bin_first I) <~~~> functor_id C
126 ; pmon_cancell : (bin_second I) <~~~> functor_id C
127 ; 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))
128 ; 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))
129 (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
130 ; pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b)
131 ; pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
132 ; pmon_coherent_r : forall a c d:C, #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
133 ; pmon_coherent_l : forall a c d:C, #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
136 * Premonoidal categories actually have three associators (the "f"
137 * indicates the position in which the operation is natural:
139 * assoc : (A ⋊ f) ⋉ C <-> A ⋊ (f ⋉ C)
140 * assoc_rr : (f ⋉ B) ⋉ C <-> f ⋉ (B ⊗ C)
141 * assoc_ll : (A ⋊ B) ⋊ f <-> (A ⊗ B) ⋊ f
143 * Fortunately, in a monoidal category these are all the same natural
144 * isomorphism (and in any case -- monoidal or not -- the objects in
145 * the left column are all the same and the objects in the right
146 * column are all the same). This formalization assumes that is the
147 * case even for premonoidal categories with non-central maps, in
148 * order to keep the complexity manageable. I don't know much about
149 * the consequences of having them and letting them be different; you
150 * might need extra versions of the triangle/pentagon diagrams.
153 Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I ].
154 Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I ].
155 Implicit Arguments pmon_assoc [ Ob Hom C bin_obj' bc I ].
156 Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
158 (* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
159 Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b
160 : #((pmon_cancelr mn) (a ⊗ b)) ~~ #((pmon_assoc mn a EI) b) >>> (a ⋊-) \ #((pmon_cancelr mn) b).
161 set (pmon_pentagon EI EI a b) as penta. unfold pmon_pentagon in penta.
162 set (pmon_triangle a b) as tria. unfold pmon_triangle in tria.
163 apply (fmor_respects(bin_second EI)) in tria.
164 set (@fmor_preserves_comp) as fpc.
165 setoid_rewrite <- fpc in tria.
166 set (ni_commutes (pmon_assoc mn a b)) as xx.
170 Class PreMonoidalFunctor
171 `(PM1:PreMonoidalCat(C:=C1)(I:=I1))
172 `(PM2:PreMonoidalCat(C:=C2)(I:=I2))
173 (fobj : C1 -> C2 ) :=
174 { mf_F :> Functor C1 C2 fobj
175 ; mf_preserves_i : mf_F I1 ≅ I2
176 ; mf_preserves_first : forall a, bin_first a >>>> mf_F <~~~> mf_F >>>> bin_first (mf_F a)
177 ; mf_preserves_second : forall a, bin_second a >>>> mf_F <~~~> mf_F >>>> bin_second (mf_F a)
178 ; mf_preserves_center : forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
180 Coercion mf_F : PreMonoidalFunctor >-> Functor.
182 (*******************************************************************************)
183 (* Braided and Symmetric Categories *)
185 Class BraidedCat `(mc:PreMonoidalCat) :=
186 { br_niso : forall a, bin_first a <~~~> bin_second a
187 ; br_swap := fun a b => ni_iso (br_niso b) a
188 ; triangleb : forall a:C, #(pmon_cancelr mc a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell mc a)
189 ; hexagon1 : forall {a b c}, #(pmon_assoc mc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc mc _ _ _)
190 ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc mc _ _ _) >>> b ⋊ #(br_swap _ _)
191 ; hexagon2 : forall {a b c}, #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc mc _ _ _)⁻¹
192 ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
195 Class SymmetricCat `(bc:BraidedCat) :=
196 { symcat_swap : forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
199 (* Definition 7.23 *)
200 Class MonoidalCat `{C:Category}{Fobj:prod_obj C C -> C}{F:Functor (C ×× C) C Fobj}(I:C) :=
204 ; mon_first := fun a b c (f:a~>b) => F \ pair_mor (pair_obj a c) (pair_obj b c) f (id c)
205 ; mon_second := fun a b c (f:a~>b) => F \ pair_mor (pair_obj c a) (pair_obj c b) (id c) f
206 ; mon_cancelr : (func_rlecnac I >>>> F) <~~~> functor_id C
207 ; mon_cancell : (func_llecnac I >>>> F) <~~~> functor_id C
208 ; mon_assoc : ((F **** (functor_id C)) >>>> F) <~~~> func_cossa >>>> ((((functor_id C) **** F) >>>> F))
209 ; mon_pentagon : Pentagon mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
210 ; mon_triangle : Triangle mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
211 (fun a => #(mon_cancell a)) (fun a => #(mon_cancelr a))
213 (* Coq manual on coercions: ... only the oldest one is valid and the
214 * others are ignored. So the order of declaration of coercions is
216 Coercion mon_c : MonoidalCat >-> Category.
217 Coercion mon_f : MonoidalCat >-> Functor.
218 Implicit Arguments mon_f [Ob Hom C Fobj F I].
219 Implicit Arguments mon_i [Ob Hom C Fobj F I].
220 Implicit Arguments mon_c [Ob Hom C Fobj F I].
221 Implicit Arguments MonoidalCat [Ob Hom ].
223 Section MonoidalCat_is_PreMonoidal.
224 Context `(M:MonoidalCat).
225 Definition mon_bin_M := BinoidalCat_from_Bifunctor (mon_f M).
226 Existing Instance mon_bin_M.
227 Lemma mon_pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a).
229 set (fun c => mon_assoc (pair_obj (pair_obj a c) b)) as qq.
231 apply Build_NaturalIsomorphism with (ni_iso:=qq).
232 abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
233 (pair_mor (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
234 (pair_mor (pair_obj a A) (pair_obj a B) (id a) f) (id b))) as qr;
238 Lemma mon_pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b).
240 set (fun c:C => mon_assoc (pair_obj (pair_obj c a) b)) as qq.
243 apply Build_NaturalIsomorphism with (ni_iso:=qq).
244 abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
245 (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
246 (pair_mor (pair_obj _ _) (pair_obj _ _) f (id a)) (id b))) as qr;
247 etransitivity; [ idtac | apply qr ];
248 apply comp_respects; try reflexivity;
251 apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
252 split; try reflexivity;
255 set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
260 Lemma mon_pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a).
262 set (fun c:C => mon_assoc (pair_obj (pair_obj a b) c)) as qq.
264 set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (Fobj (pair_obj a b) ⋊-) (b ⋊- >>>> a ⋊-)) as qqq.
269 abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
270 (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
271 (pair_mor (pair_obj _ _) (pair_obj _ _) (id a) (id b)) f)) as qr;
272 etransitivity; [ apply qr | idtac ];
273 apply comp_respects; try reflexivity;
276 apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
277 split; try reflexivity;
279 set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
284 Lemma mon_pmon_cancelr : (bin_first I0) <~~~> functor_id C.
285 set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_first I0) (functor_id C)) as qq.
286 set (mon_cancelr) as z.
292 set (ni_commutes mon_cancelr) as q; simpl in *;
296 Lemma mon_pmon_cancell : (bin_second I0) <~~~> functor_id C.
297 set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_second I0) (functor_id C)) as qq.
298 set (mon_cancell) as z.
304 set (ni_commutes mon_cancell) as q; simpl in *;
308 Lemma mon_pmon_triangle : forall a b, #(mon_pmon_cancelr a) ⋉ b ~~ #(mon_pmon_assoc _ _ _) >>> a ⋊ #(mon_pmon_cancell b).
310 set mon_triangle as q.
315 Lemma mon_pmon_pentagon a b c d : (#(mon_pmon_assoc a c b ) ⋉ d) >>>
316 #(mon_pmon_assoc a d _ ) >>>
317 (a ⋊ #(mon_pmon_assoc b d c))
318 ~~ #(mon_pmon_assoc _ d c ) >>>
319 #(mon_pmon_assoc a _ b ).
320 set (@pentagon _ _ _ _ _ _ _ mon_pentagon) as x.
323 unfold mon_first in x.
328 Definition MonoidalCat_is_PreMonoidal : PreMonoidalCat (BinoidalCat_from_Bifunctor (mon_f M)) (mon_i M).
329 refine {| pmon_assoc := mon_pmon_assoc
330 ; pmon_cancell := mon_pmon_cancell
331 ; pmon_cancelr := mon_pmon_cancelr
332 ; pmon_triangle := {| triangle := mon_pmon_triangle |}
333 ; pmon_pentagon := {| pentagon := mon_pmon_pentagon |}
334 ; pmon_assoc_ll := mon_pmon_assoc_ll
335 ; pmon_assoc_rr := mon_pmon_assoc_rr
337 abstract (set (coincide mon_triangle) as qq; simpl in *; apply qq).
338 abstract (intros; simpl; reflexivity).
339 abstract (intros; simpl; reflexivity).
342 Lemma MonoidalCat_all_central : forall a b (f:a~~{M}~~>b), CentralMorphism f.
344 set (@fmor_preserves_comp _ _ _ _ _ _ _ M) as fc.
345 apply Build_CentralMorphism;
352 apply (fmor_respects M).
354 setoid_rewrite left_identity;
355 setoid_rewrite right_identity;
362 apply (fmor_respects M).
364 setoid_rewrite left_identity;
365 setoid_rewrite right_identity;
369 End MonoidalCat_is_PreMonoidal.
371 Hint Extern 1 => apply MonoidalCat_all_central.
372 Coercion MonoidalCat_is_PreMonoidal : MonoidalCat >-> PreMonoidalCat.
374 (* Later: generalize to premonoidal categories *)
375 Class DiagonalCat `(mc:MonoidalCat(F:=F)) :=
376 { copy_nt : forall a, functor_id _ ~~~> func_diagonal >>>> F
377 ; copy : forall (a:mc), a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
378 := fun a => nt_component _ _ (copy_nt a) a
379 (* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)
382 (* TO DO: show that the endofunctors on any given category form a monoidal category *)
383 Section MonoidalFunctor.
384 Context `(m1:MonoidalCat(C:=C1)) `(m2:MonoidalCat(C:=C2)).
385 Class MonoidalFunctor {Mobj:C1->C2} (mf_F:Functor C1 C2 Mobj) :=
386 { mf_f := mf_F where "f ⊕⊕ g" := (@fmor _ _ _ _ _ _ _ m2 _ _ (pair_mor (pair_obj _ _) (pair_obj _ _) f g))
387 ; mf_coherence : (mf_F **** mf_F) >>>> (mon_f m2) <~~~> (mon_f m1) >>>> mf_F
388 ; mf_phi := fun a b => #(mf_coherence (pair_obj a b))
389 ; mf_id : (mon_i m2) ≅ (mf_F (mon_i m1))
390 ; mf_cancelr : forall a, #(mon_cancelr(MonoidalCat:=m2) (mf_F a)) ~~
391 (id (mf_F a)) ⊕⊕ #mf_id >>> mf_phi a (mon_i _) >>> mf_F \ #(mon_cancelr a)
392 ; mf_cancell : forall b, #(mon_cancell (mf_F b)) ~~
393 #mf_id ⊕⊕ (id (mf_F b)) >>> mf_phi (mon_i _) b >>> mf_F \ #(mon_cancell b)
394 ; mf_assoc : forall a b c, (mf_phi a b) ⊕⊕ (id (mf_F c)) >>> (mf_phi _ c) >>>
395 (mf_F \ #(mon_assoc (pair_obj (pair_obj a b) c) )) ~~
396 #(mon_assoc (pair_obj (pair_obj _ _) _) ) >>>
397 (id (mf_F a)) ⊕⊕ (mf_phi b c) >>> (mf_phi a _)
400 Coercion mf_f : MonoidalFunctor >-> Functor.
401 Implicit Arguments mf_coherence [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
402 Implicit Arguments mf_id [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
404 Section MonoidalFunctorsCompose.
405 Context `(m1:MonoidalCat).
406 Context `(m2:MonoidalCat).
407 Context `(m3:MonoidalCat).
408 Context {f1obj}(f1:@Functor _ _ m1 _ _ m2 f1obj).
409 Context {f2obj}(f2:@Functor _ _ m2 _ _ m3 f2obj).
410 Context (mf1:MonoidalFunctor m1 m2 f1).
411 Context (mf2:MonoidalFunctor m2 m3 f2).
413 Lemma mf_compose_coherence : (f1 >>>> f2) **** (f1 >>>> f2) >>>> m3 <~~~> m1 >>>> (f1 >>>> f2).
414 set (mf_coherence mf1) as mc1.
415 set (mf_coherence mf2) as mc2.
417 set (q _ _ _ _ _ _ _ ((f1 >>>> f2) **** (f1 >>>> f2) >>>> m3) _ ((f1 **** f1 >>>> m2) >>>> f2) _ (m1 >>>> (f1 >>>> f2))) as qq.
418 apply qq; clear qq; clear q.
419 apply (@ni_comp _ _ _ _ _ _ _ _ _ (f1 **** f1 >>>> (f2 **** f2 >>>> m3)) _ _).
420 apply (@ni_comp _ _ _ _ _ _ _ _ _ ((f1 **** f1 >>>> f2 **** f2) >>>> m3) _ _).
424 apply ni_associativity.
427 apply (ni_associativity (f1 **** f1) m2 f2).
428 apply (ni_respects (F0:=f1 **** f1)(F1:=f1 **** f1)(G0:=(m2 >>>> f2))(G1:=(f2 **** f2 >>>> m3))).
435 apply (ni_associativity m1 f1 f2).
442 Instance MonoidalFunctorsCompose : MonoidalFunctor m1 m3 (f1 >>>> f2) :=
443 { mf_id := id_comp (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
444 ; mf_coherence := mf_compose_coherence
451 End MonoidalFunctorsCompose.
453 Class CartesianCat `(mc:MonoidalCat) :=
454 { car_terminal : Terminal mc
455 ; car_one : (@one _ _ _ car_terminal) ≅ (mon_i mc)
456 ; car_diagonal : DiagonalCat mc
457 ; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell mc _))
458 ; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr mc _))
461 Coercion car_diagonal : CartesianCat >-> DiagonalCat.
462 Coercion car_terminal : CartesianCat >-> Terminal.
463 Coercion car_mn : CartesianCat >-> MonoidalCat.
465 Section CenterMonoidal.
467 Context `(mc:PreMonoidalCat(I:=pI)).
469 Definition CenterMonoidal_Fobj : (Center mc) ×× (Center mc) -> Center mc.
472 destruct a as [a apf].
473 destruct b as [b bpf].
474 exists (a ⊗ b); auto.
477 Definition CenterMonoidal_F_fmor (a b:(Center mc) ×× (Center mc)) :
478 (a~~{(Center mc) ×× (Center mc)}~~>b) ->
479 ((CenterMonoidal_Fobj a)~~{Center mc}~~>(CenterMonoidal_Fobj b)).
480 destruct a as [[a1 a1'] [a2 a2']].
481 destruct b as [[b1 b1'] [b2 b2']].
483 destruct f as [[f1 f1'] [f2 f2']].
487 exists (f1 ⋉ a2 >>> b1 ⋊ f2).
488 apply central_morphisms_compose.
493 Definition CenterMonoidal_F : Functor _ _ CenterMonoidal_Fobj.
494 refine {| fmor := CenterMonoidal_F_fmor |}.
496 destruct a as [[a1 a1'] [a2 a2']].
497 destruct b as [[b1 b1'] [b2 b2']].
498 destruct f as [[f1 f1'] [f2 f2']].
499 destruct f' as [[g1 g1'] [g2 g2']].
503 set (fmor_respects(-⋉a2)) as q; apply q; auto.
504 set (fmor_respects(b1⋊-)) as q; apply q; auto.
506 destruct a as [[a1 a1'] [a2 a2']].
508 setoid_rewrite (fmor_preserves_id (-⋉a2)).
509 setoid_rewrite (fmor_preserves_id (a1⋊-)).
512 destruct a as [[a1 a1'] [a2 a2']].
513 destruct b as [[b1 b1'] [b2 b2']].
514 destruct c as [[c1 c1'] [c2 c2']].
515 destruct f as [[f1 f1'] [f2 f2']].
516 destruct g as [[g1 g1'] [g2 g2']].
518 setoid_rewrite juggle3.
519 setoid_rewrite <- (centralmor_first(CentralMorphism:=g1')).
520 setoid_rewrite <- juggle3.
521 setoid_rewrite <- fmor_preserves_comp.
525 Definition CenterMonoidal : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I).