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 InitialTerminal_ch2_2.
7 Require Import Subcategories_ch7_1.
8 Require Import ProductCategories_ch1_6_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 (* TO DO: show that the endofunctors on any given category form a monoidal category *)
22 * Unlike Awodey, I define a monoidal category to be a premonoidal
23 * category in which all morphisms are central. This is partly to
24 * have a clean inheritance hierarchy, but also because Coq bogs down
25 * on product categories for some inexplicable reason.
27 Class MonoidalCat `(pm:PreMonoidalCat) :=
29 ; mon_commutative :> CommutativeCat pm
31 Coercion mon_pm : MonoidalCat >-> PreMonoidalCat.
32 Coercion mon_commutative : MonoidalCat >-> CommutativeCat.
34 (* a monoidal functor is just a premonoidal functor between premonoidal categories which happen to be monoidal *)
35 Definition MonoidalFunctor `(m1:MonoidalCat) `(m2:MonoidalCat) {fobj}(F:Functor m1 m2 fobj) := PreMonoidalFunctor m1 m2 F.
37 Definition MonoidalFunctorsCompose
38 `{PM1 :MonoidalCat(C:=C1)}
39 `{PM2 :MonoidalCat(C:=C2)}
41 {PMFF12:Functor C1 C2 fobj12 }
42 (PMF12 :MonoidalFunctor PM1 PM2 PMFF12)
43 `{PM3 :MonoidalCat(C:=C3)}
45 {PMFF23:Functor C2 C3 fobj23 }
46 (PMF23 :MonoidalFunctor PM2 PM3 PMFF23)
47 := PreMonoidalFunctorsCompose PMF12 PMF23.
49 Class MonoidalNaturalIsomorphism
50 `{C1:MonoidalCat}`{C2:MonoidalCat}
51 `(F1:!MonoidalFunctor(fobj:=fobj1) C1 C2 Func1)
52 `(F2:!MonoidalFunctor(fobj:=fobj2) C1 C2 Func2) :=
53 { mni_ni : NaturalIsomorphism F1 F2
54 ; mni_commutes1 : forall A B,
55 #(ni_iso (mf_first(PreMonoidalFunctor:=F1) B) A) >>> #(ni_iso mni_ni (A⊗B)) ~~
56 #(ni_iso mni_ni _) ⋉ _ >>> _ ⋊ #(ni_iso mni_ni _) >>> #(ni_iso (mf_first(PreMonoidalFunctor:=F2) B) A)
57 ; mni_commutes2 : forall A B,
58 #(ni_iso (mf_second(PreMonoidalFunctor:=F1) A) B) >>> #(ni_iso mni_ni (A⊗B)) ~~
59 #(ni_iso mni_ni _) ⋉ _ >>> _ ⋊ #(ni_iso mni_ni _) >>> #(ni_iso (mf_second(PreMonoidalFunctor:=F2) A) B)
61 Notation "F <~~⊗~~> G" := (@MonoidalNaturalIsomorphism _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ F _ _ G) : category_scope.
63 (* an equivalence of categories via monoidal functors, but the natural iso isn't necessarily a monoidal natural iso *)
64 Structure MonoidalEquivalence `{C1:MonoidalCat} `{C2:MonoidalCat} :=
65 { meqv_forward_fobj : C1 -> C2
66 ; meqv_forward : Functor C1 C2 meqv_forward_fobj
67 ; meqv_forward_mon : PreMonoidalFunctor _ _ meqv_forward
68 ; meqv_backward_fobj : C2 -> C1
69 ; meqv_backward : Functor C2 C1 meqv_backward_fobj
70 ; meqv_backward_mon : PreMonoidalFunctor _ _ meqv_backward
71 ; meqv_comp1 : meqv_forward >>>> meqv_backward ≃ functor_id _
72 ; meqv_comp2 : meqv_backward >>>> meqv_forward ≃ functor_id _
75 (* a monoidally-natural equivalence of categories *)
77 Structure MonoidalNaturalEquivalence `{C1:MonoidalCat} `{C2:MonoidalCat} :=
78 { mneqv_forward_fobj : C1 -> C2
79 ; mneqv_forward : Functor C1 C2 mneqv_forward_fobj
80 ; mneqv_forward_mon : PreMonoidalFunctor _ _ mneqv_forward
81 ; mneqv_backward_fobj : C2 -> C1
82 ; mneqv_backward : Functor C2 C1 mneqv_backward_fobj
83 ; mneqv_backward_mon : PreMonoidalFunctor _ _ mneqv_backward
84 ; mneqv_comp1 : mneqv_forward_mon >>⊗>> mneqv_backward_mon <~~⊗~~> premonoidal_id _
85 ; mneqv_comp2 : mneqv_backward_mon >>⊗>> mneqv_forward_mon <~~⊗~~> premonoidal_id _
89 Section BinoidalCat_from_Bifunctor.
90 Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).
91 Definition BinoidalCat_from_Bifunctor_first (a:C) : Functor C C (fun b => Fobj (pair_obj b a)).
92 apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
93 @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;
94 [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
95 | abstract (set (fmor_preserves_id(F)) as q; apply q)
96 | abstract (etransitivity;
97 [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
98 | set (fmor_respects(F)) as q; apply q ];
99 split; simpl; auto) ].
101 Definition BinoidalCat_from_Bifunctor_second (a:C) : Functor C C (fun b => Fobj (pair_obj a b)).
102 apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
103 @fmor _ _ _ _ _ _ _ F (pair_obj a a0) (pair_obj a b) (pair_mor (pair_obj a a0) (pair_obj a b) (id a) f))); intros;
104 [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
105 | abstract (set (fmor_preserves_id(F)) as q; apply q)
106 | abstract (etransitivity;
107 [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
108 | set (fmor_respects(F)) as q; apply q ];
109 split; simpl; auto) ].
112 Definition BinoidalCat_from_Bifunctor : BinoidalCat C (fun a b => Fobj (pair_obj a b)).
113 refine {| bin_first := BinoidalCat_from_Bifunctor_first
114 ; bin_second := BinoidalCat_from_Bifunctor_second
118 Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat BinoidalCat_from_Bifunctor.
119 abstract (intros; apply Build_CommutativeCat; intros; apply Build_CentralMorphism; intros; simpl; (
120 etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ]; symmetry;
121 etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ];
122 apply (fmor_respects(F));
124 [ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
125 | etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
128 (* if this binoidal structure has all of the natural isomorphisms of a premonoidal category, then it's monoidal *)
129 Context {pmI}(pm:PreMonoidalCat BinoidalCat_from_Bifunctor pmI).
131 Instance PreMonoidalCat_from_bifunctor_is_Monoidal : MonoidalCat pm :=
132 { mon_commutative := Bifunctors_Create_Commutative_Binoidal_Categories
135 End BinoidalCat_from_Bifunctor.
138 (* we can go the other way: given a monoidal category, its left/right functors can be combined into a bifunctor *)
139 Section Bifunctor_from_MonoidalCat.
140 Context `(M:MonoidalCat).
143 Definition Bifunctor_from_MonoidalCat_fobj : M ×× M -> M.
146 exact (bin_obj' o o0).
149 Definition Bifunctor_from_MonoidalCat_fmor {a}{b}(f:a~~{M××M}~~>b)
150 : (Bifunctor_from_MonoidalCat_fobj a)~~{M}~~>(Bifunctor_from_MonoidalCat_fobj b).
151 destruct a; destruct b; destruct f.
153 apply (h ⋉ _ >>> _ ⋊ h0).
156 Instance Bifunctor_from_MonoidalCat : Functor (M ×× M) M Bifunctor_from_MonoidalCat_fobj :=
157 { fmor := fun x y f => Bifunctor_from_MonoidalCat_fmor f }.
159 destruct a; destruct b; destruct f; destruct f'; simpl in *.
162 apply (fmor_respects (-⋉o0)); auto.
163 apply (fmor_respects (o1⋊-)); auto.
164 intros; destruct a; simpl in *.
165 setoid_rewrite (fmor_preserves_id (-⋉o0)).
166 setoid_rewrite left_identity.
167 apply fmor_preserves_id.
168 intros; destruct a; destruct b; destruct c; destruct f; destruct g; simpl in *.
169 setoid_rewrite <- fmor_preserves_comp.
170 setoid_rewrite juggle3 at 1.
171 assert (CentralMorphism h1).
172 apply mon_commutative.
173 setoid_rewrite <- (centralmor_first(CentralMorphism:=H)).
174 setoid_rewrite <- juggle3.
178 End Bifunctor_from_MonoidalCat.
181 Class DiagonalCat `(mc:MonoidalCat) :=
182 { copy : forall (a:mc), a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
183 ; copy_natural1 : forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> f ⋉ a >>> b ⋊ f ~~ f >>> copy _
184 ; copy_natural2 : forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> a ⋊ f >>> f ⋉ b ~~ f >>> copy _
185 (* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)
188 Class CartesianCat `(mc:MonoidalCat) :=
189 { car_terminal :> TerminalObject mc pmon_I
190 ; car_diagonal : DiagonalCat mc
191 ; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (drop a ⋉ a) >>> (#(pmon_cancell _))
192 ; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ drop a) >>> (#(pmon_cancelr _))
195 Coercion car_diagonal : CartesianCat >-> DiagonalCat.
196 Coercion car_terminal : CartesianCat >-> TerminalObject.
197 Coercion car_mn : CartesianCat >-> MonoidalCat.