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.
12 Require Import BinoidalCategories.
13 Require Import PreMonoidalCategories.
15 (******************************************************************************)
16 (* Chapter 7.8: Monoidal Categories *)
17 (******************************************************************************)
19 Class MonoidalCat `{C:Category}{Fobj:prod_obj C C -> C}{F:Functor (C ×× C) C Fobj}(I:C) :=
23 ; mon_first := fun a b c (f:a~>b) => F \ pair_mor (pair_obj a c) (pair_obj b c) f (id c)
24 ; mon_second := fun a b c (f:a~>b) => F \ pair_mor (pair_obj c a) (pair_obj c b) (id c) f
25 ; mon_cancelr : (func_rlecnac I >>>> F) <~~~> functor_id C
26 ; mon_cancell : (func_llecnac I >>>> F) <~~~> functor_id C
27 ; mon_assoc : ((F **** (functor_id C)) >>>> F) <~~~> func_cossa >>>> ((((functor_id C) **** F) >>>> F))
28 ; mon_pentagon : Pentagon mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
29 ; mon_triangle : Triangle mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
30 (fun a => #(mon_cancell a)) (fun a => #(mon_cancelr a))
32 (* Coq manual on coercions: ... only the oldest one is valid and the
33 * others are ignored. So the order of declaration of coercions is
35 Coercion mon_c : MonoidalCat >-> Category.
36 Coercion mon_f : MonoidalCat >-> Functor.
37 Implicit Arguments mon_f [Ob Hom C Fobj F I].
38 Implicit Arguments mon_i [Ob Hom C Fobj F I].
39 Implicit Arguments mon_c [Ob Hom C Fobj F I].
40 Implicit Arguments MonoidalCat [Ob Hom ].
42 (* TO DO: show that the endofunctors on any given category form a monoidal category *)
43 Section MonoidalFunctor.
44 Context `(m1:MonoidalCat(C:=C1)) `(m2:MonoidalCat(C:=C2)).
45 Class MonoidalFunctor {Mobj:C1->C2} (mf_F:Functor C1 C2 Mobj) :=
46 { mf_f := mf_F where "f ⊕⊕ g" := (@fmor _ _ _ _ _ _ _ m2 _ _ (pair_mor (pair_obj _ _) (pair_obj _ _) f g))
47 ; mf_coherence : (mf_F **** mf_F) >>>> (mon_f m2) <~~~> (mon_f m1) >>>> mf_F
48 ; mf_phi := fun a b => #(mf_coherence (pair_obj a b))
49 ; mf_id : (mon_i m2) ≅ (mf_F (mon_i m1))
50 ; mf_cancelr : forall a, #(mon_cancelr(MonoidalCat:=m2) (mf_F a)) ~~
51 (id (mf_F a)) ⊕⊕ #mf_id >>> mf_phi a (mon_i _) >>> mf_F \ #(mon_cancelr a)
52 ; mf_cancell : forall b, #(mon_cancell (mf_F b)) ~~
53 #mf_id ⊕⊕ (id (mf_F b)) >>> mf_phi (mon_i _) b >>> mf_F \ #(mon_cancell b)
54 ; mf_assoc : forall a b c, (mf_phi a b) ⊕⊕ (id (mf_F c)) >>> (mf_phi _ c) >>>
55 (mf_F \ #(mon_assoc (pair_obj (pair_obj a b) c) )) ~~
56 #(mon_assoc (pair_obj (pair_obj _ _) _) ) >>>
57 (id (mf_F a)) ⊕⊕ (mf_phi b c) >>> (mf_phi a _)
60 Coercion mf_f : MonoidalFunctor >-> Functor.
61 Implicit Arguments mf_coherence [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
62 Implicit Arguments mf_id [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
64 Section MonoidalFunctorsCompose.
65 Context `(m1:MonoidalCat).
66 Context `(m2:MonoidalCat).
67 Context `(m3:MonoidalCat).
68 Context {f1obj}(f1:@Functor _ _ m1 _ _ m2 f1obj).
69 Context {f2obj}(f2:@Functor _ _ m2 _ _ m3 f2obj).
70 Context (mf1:MonoidalFunctor m1 m2 f1).
71 Context (mf2:MonoidalFunctor m2 m3 f2).
73 Lemma mf_compose_coherence : (f1 >>>> f2) **** (f1 >>>> f2) >>>> m3 <~~~> m1 >>>> (f1 >>>> f2).
74 set (mf_coherence mf1) as mc1.
75 set (mf_coherence mf2) as mc2.
77 set (q _ _ _ _ _ _ _ ((f1 >>>> f2) **** (f1 >>>> f2) >>>> m3) _ ((f1 **** f1 >>>> m2) >>>> f2) _ (m1 >>>> (f1 >>>> f2))) as qq.
78 apply qq; clear qq; clear q.
79 apply (@ni_comp _ _ _ _ _ _ _ _ _ (f1 **** f1 >>>> (f2 **** f2 >>>> m3)) _ _).
80 apply (@ni_comp _ _ _ _ _ _ _ _ _ ((f1 **** f1 >>>> f2 **** f2) >>>> m3) _ _).
84 apply ni_associativity.
87 apply (ni_associativity (f1 **** f1) m2 f2).
88 apply (ni_respects (F0:=f1 **** f1)(F1:=f1 **** f1)(G0:=(m2 >>>> f2))(G1:=(f2 **** f2 >>>> m3))).
95 apply (ni_associativity m1 f1 f2).
102 Instance MonoidalFunctorsCompose : MonoidalFunctor m1 m3 (f1 >>>> f2) :=
103 { mf_id := id_comp (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
104 ; mf_coherence := mf_compose_coherence
111 End MonoidalFunctorsCompose.
113 Section MonoidalCat_is_PreMonoidal.
114 Context `(M:MonoidalCat).
115 Definition mon_bin_M := BinoidalCat_from_Bifunctor (mon_f M).
116 Existing Instance mon_bin_M.
118 Lemma mon_pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a).
120 set (fun c => mon_assoc (pair_obj (pair_obj a c) b)) as qq.
122 apply Build_NaturalIsomorphism with (ni_iso:=qq).
123 abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
124 (pair_mor (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
125 (pair_mor (pair_obj a A) (pair_obj a B) (id a) f) (id b))) as qr;
129 Lemma mon_pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b).
131 set (fun c:C => mon_assoc (pair_obj (pair_obj c a) b)) as qq.
134 apply Build_NaturalIsomorphism with (ni_iso:=qq).
135 abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
136 (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
137 (pair_mor (pair_obj _ _) (pair_obj _ _) f (id a)) (id b))) as qr;
138 etransitivity; [ idtac | apply qr ];
139 apply comp_respects; try reflexivity;
142 apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
143 split; try reflexivity;
146 set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
151 Lemma mon_pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a).
153 set (fun c:C => mon_assoc (pair_obj (pair_obj a b) c)) as qq.
155 set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (Fobj (pair_obj a b) ⋊-) (b ⋊- >>>> a ⋊-)) as qqq.
160 abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
161 (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
162 (pair_mor (pair_obj _ _) (pair_obj _ _) (id a) (id b)) f)) as qr;
163 etransitivity; [ apply qr | idtac ];
164 apply comp_respects; try reflexivity;
167 apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
168 split; try reflexivity;
170 set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
175 Lemma mon_pmon_cancelr : (bin_first I0) <~~~> functor_id C.
176 set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_first I0) (functor_id C)) as qq.
177 set (mon_cancelr) as z.
183 set (ni_commutes mon_cancelr) as q; simpl in *;
187 Lemma mon_pmon_cancell : (bin_second I0) <~~~> functor_id C.
188 set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_second I0) (functor_id C)) as qq.
189 set (mon_cancell) as z.
195 set (ni_commutes mon_cancell) as q; simpl in *;
199 Lemma mon_pmon_triangle : forall a b, #(mon_pmon_cancelr a) ⋉ b ~~ #(mon_pmon_assoc _ _ _) >>> a ⋊ #(mon_pmon_cancell b).
201 set mon_triangle as q.
206 Lemma mon_pmon_pentagon a b c d : (#(mon_pmon_assoc a c b ) ⋉ d) >>>
207 #(mon_pmon_assoc a d _ ) >>>
208 (a ⋊ #(mon_pmon_assoc b d c))
209 ~~ #(mon_pmon_assoc _ d c ) >>>
210 #(mon_pmon_assoc a _ b ).
211 set (@pentagon _ _ _ _ _ _ _ mon_pentagon) as x.
214 unfold mon_first in x.
219 Definition MonoidalCat_is_PreMonoidal : PreMonoidalCat (BinoidalCat_from_Bifunctor (mon_f M)) (mon_i M).
220 refine {| pmon_assoc := mon_pmon_assoc
221 ; pmon_cancell := mon_pmon_cancell
222 ; pmon_cancelr := mon_pmon_cancelr
223 ; pmon_triangle := {| triangle := mon_pmon_triangle |}
224 ; pmon_pentagon := {| pentagon := mon_pmon_pentagon |}
225 ; pmon_assoc_ll := mon_pmon_assoc_ll
226 ; pmon_assoc_rr := mon_pmon_assoc_rr
228 abstract (set (coincide mon_triangle) as qq; simpl in *; apply qq).
229 abstract (intros; simpl; reflexivity).
230 abstract (intros; simpl; reflexivity).
233 Lemma MonoidalCat_all_central : forall a b (f:a~~{M}~~>b), CentralMorphism f.
235 set (@fmor_preserves_comp _ _ _ _ _ _ _ M) as fc.
236 apply Build_CentralMorphism;
243 apply (fmor_respects M).
245 setoid_rewrite left_identity;
246 setoid_rewrite right_identity;
253 apply (fmor_respects M).
255 setoid_rewrite left_identity;
256 setoid_rewrite right_identity;
260 End MonoidalCat_is_PreMonoidal.
262 Hint Extern 1 => apply MonoidalCat_all_central.
263 Coercion MonoidalCat_is_PreMonoidal : MonoidalCat >-> PreMonoidalCat.
265 (* Later: generalize to premonoidal categories *)
266 Class DiagonalCat `(mc:MonoidalCat(F:=F)) :=
267 { copy_nt : forall a, functor_id _ ~~~> func_diagonal >>>> F
268 ; copy : forall (a:mc), a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
269 := fun a => nt_component _ _ (copy_nt a) a
270 (* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)
273 Class CartesianCat `(mc:MonoidalCat) :=
274 { car_terminal : Terminal mc
275 ; car_one : (@one _ _ _ car_terminal) ≅ (mon_i mc)
276 ; car_diagonal : DiagonalCat mc
277 ; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell mc _))
278 ; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr mc _))
281 Coercion car_diagonal : CartesianCat >-> DiagonalCat.
282 Coercion car_terminal : CartesianCat >-> Terminal.
283 Coercion car_mn : CartesianCat >-> MonoidalCat.