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 InitialTerminal_ch2_2.
7 Require Import Subcategories_ch7_1.
8 Require Import NaturalTransformations_ch7_4.
9 Require Import NaturalIsomorphisms_ch7_5.
10 Require Import Coherence_ch7_8.
11 Require Import BinoidalCategories.
14 Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
18 ; pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
19 ; pmon_cancelr : (bin_first I) <~~~> functor_id C
20 ; pmon_cancell : (bin_second I) <~~~> functor_id C
21 ; 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))
22 ; 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))
23 (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
24 ; pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b)
25 ; pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
26 ; pmon_coherent_r : forall a c d:C, #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
27 ; pmon_coherent_l : forall a c d:C, #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
28 ; pmon_assoc_central : forall a b c, CentralMorphism #(pmon_assoc a b c)
29 ; pmon_cancelr_central : forall a , CentralMorphism #(pmon_cancelr a)
30 ; pmon_cancell_central : forall a , CentralMorphism #(pmon_cancell a)
33 * Premonoidal categories actually have three associators (the "f"
34 * indicates the position in which the operation is natural:
36 * assoc : (A ⋊ f) ⋉ C <-> A ⋊ (f ⋉ C)
37 * assoc_rr : (f ⋉ B) ⋉ C <-> f ⋉ (B ⊗ C)
38 * assoc_ll : (A ⋊ B) ⋊ f <-> (A ⊗ B) ⋊ f
40 * Fortunately, in a monoidal category these are all the same natural
41 * isomorphism (and in any case -- monoidal or not -- the objects in
42 * the left column are all the same and the objects in the right
43 * column are all the same). This formalization assumes that is the
44 * case even for premonoidal categories with non-central maps, in
45 * order to keep the complexity manageable. I don't know much about
46 * the consequences of having them and letting them be different; you
47 * might need extra versions of the triangle/pentagon diagrams.
50 Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
51 Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
52 Implicit Arguments pmon_assoc [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
53 Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
55 (* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
56 Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b
57 : #(pmon_cancelr (a ⊗ b)) ~~ #((pmon_assoc a EI) b) >>> (a ⋊-) \ #(pmon_cancelr b).
58 set (pmon_pentagon EI EI a b) as penta. unfold pmon_pentagon in penta.
59 set (pmon_triangle a b) as tria. unfold pmon_triangle in tria.
60 apply (fmor_respects(bin_second EI)) in tria.
61 set (@fmor_preserves_comp) as fpc.
62 setoid_rewrite <- fpc in tria.
63 set (ni_commutes (pmon_assoc a b)) as xx.
67 Class PreMonoidalFunctor
68 `(PM1:PreMonoidalCat(C:=C1)(I:=I1))
69 `(PM2:PreMonoidalCat(C:=C2)(I:=I2))
71 { mf_F :> Functor C1 C2 fobj
73 ; mf_first : ∀ a, mf_F >>>> bin_first (mf_F a) <~~~> bin_first a >>>> mf_F
74 ; mf_second : ∀ a, mf_F >>>> bin_second (mf_F a) <~~~> bin_second a >>>> mf_F
75 ; mf_consistent : ∀ a b, #(mf_first a b) ~~ #(mf_second b a)
76 ; mf_center : forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
77 ; mf_cancell : ∀ b, #(pmon_cancell _) ~~ #mf_i ⋉ _ >>> #(mf_first b I1) >>> mf_F \ #(pmon_cancell b)
78 ; mf_cancelr : ∀ a, #(pmon_cancelr _) ~~ _ ⋊ #mf_i >>> #(mf_second a I1) >>> mf_F \ #(pmon_cancelr a)
79 ; mf_assoc : ∀ a b c, #(pmon_assoc _ _ _) >>> _ ⋊ #(mf_second _ _) >>> #(mf_second _ _) ~~
80 #(mf_second _ _) ⋉ _ >>> #(mf_second _ _) >>> mf_F \ #(pmon_assoc a c b)
82 Coercion mf_F : PreMonoidalFunctor >-> Functor.
84 Definition PreMonoidalFunctorsCompose
85 `{PM1 :PreMonoidalCat(C:=C1)(I:=I1)}
86 `{PM2 :PreMonoidalCat(C:=C2)(I:=I2)}
88 (PMF12 :PreMonoidalFunctor PM1 PM2 fobj12)
89 `{PM3 :PreMonoidalCat(C:=C3)(I:=I3)}
91 (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23)
92 : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12).
96 (*******************************************************************************)
97 (* Braided and Symmetric Categories *)
99 Class BraidedCat `(mc:PreMonoidalCat) :=
100 { br_niso : forall a, bin_first a <~~~> bin_second a
101 ; br_swap := fun a b => ni_iso (br_niso b) a
102 ; triangleb : forall a:C, #(pmon_cancelr a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell a)
103 ; hexagon1 : forall {a b c}, #(pmon_assoc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc _ _ _)
104 ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc _ _ _) >>> b ⋊ #(br_swap _ _)
105 ; hexagon2 : forall {a b c}, #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc _ _ _)⁻¹
106 ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
109 Class SymmetricCat `(bc:BraidedCat) :=
110 { symcat_swap : forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
114 Section PreMonoidalSubCategory.
116 Context `(pm:PreMonoidalCat(I:=pmI)).
117 Context {Pobj}{Pmor}(S:SubCategory pm Pobj Pmor).
118 Context (Pobj_unit:Pobj pmI).
119 Context (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)).
120 Implicit Arguments Pobj_closed [[a][b]].
121 Context (Pmor_first: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
122 Pmor _ _ (Pobj_closed pa pc) (Pobj_closed pb pc) (f ⋉ c)).
123 Context (Pmor_second: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
124 Pmor _ _ (Pobj_closed pc pa) (Pobj_closed pc pb) (c ⋊ f)).
125 Context (Pmor_assoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
127 (Pobj_closed (Pobj_closed pa pb) pc)
128 (Pobj_closed pa (Pobj_closed pb pc))
129 #(pmon_assoc a c b)).
130 Context (Pmor_unassoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
132 (Pobj_closed pa (Pobj_closed pb pc))
133 (Pobj_closed (Pobj_closed pa pb) pc)
134 #(pmon_assoc a c b)⁻¹).
135 Context (Pmor_cancell: forall {a}(pa:Pobj a),
136 Pmor _ _ (Pobj_closed Pobj_unit pa) pa
138 Context (Pmor_uncancell: forall {a}(pa:Pobj a),
139 Pmor _ _ pa (Pobj_closed Pobj_unit pa)
140 #(pmon_cancell a)⁻¹).
141 Context (Pmor_cancelr: forall {a}(pa:Pobj a),
142 Pmor _ _ (Pobj_closed pa Pobj_unit) pa
144 Context (Pmor_uncancelr: forall {a}(pa:Pobj a),
145 Pmor _ _ pa (Pobj_closed pa Pobj_unit)
146 #(pmon_cancelr a)⁻¹).
147 Implicit Arguments Pmor_first [[a][b][c][f]].
148 Implicit Arguments Pmor_second [[a][b][c][f]].
150 Definition PreMonoidalSubCategory_bobj (x y:S) :=
151 existT Pobj _ (Pobj_closed (projT2 x) (projT2 y)).
153 Definition PreMonoidalSubCategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
154 (PreMonoidalSubCategory_bobj x a)~~{S}~~>(PreMonoidalSubCategory_bobj y a).
155 unfold hom; simpl; intros.
157 destruct a as [a apf].
158 destruct x as [x xpf].
159 destruct y as [y ypf].
162 apply Pmor_first; auto.
165 Definition PreMonoidalSubCategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
166 (PreMonoidalSubCategory_bobj a x)~~{S}~~>(PreMonoidalSubCategory_bobj a y).
167 unfold hom; simpl; intros.
169 destruct a as [a apf].
170 destruct x as [x xpf].
171 destruct y as [y ypf].
174 apply Pmor_second; auto.
177 Instance PreMonoidalSubCategory_first (a:S)
178 : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj x a) :=
179 { fmor := fun x y f => PreMonoidalSubCategory_first_fmor a f }.
180 unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
181 apply (fmor_respects (-⋉x)); auto.
182 unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0; simpl in *.
183 apply (fmor_preserves_id (-⋉x)); auto.
184 unfold PreMonoidalSubCategory_first_fmor; intros;
185 destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
186 apply (fmor_preserves_comp (-⋉x)); auto.
189 Instance PreMonoidalSubCategory_second (a:S)
190 : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj a x) :=
191 { fmor := fun x y f => PreMonoidalSubCategory_second_fmor a f }.
192 unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
193 apply (fmor_respects (x⋊-)); auto.
194 unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0; simpl in *.
195 apply (fmor_preserves_id (x⋊-)); auto.
196 unfold PreMonoidalSubCategory_second_fmor; intros;
197 destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
198 apply (fmor_preserves_comp (x⋊-)); auto.
201 Instance PreMonoidalSubCategory_is_Binoidal : BinoidalCat S PreMonoidalSubCategory_bobj :=
202 { bin_first := PreMonoidalSubCategory_first
203 ; bin_second := PreMonoidalSubCategory_second }.
205 Definition PreMonoidalSubCategory_assoc
207 (PreMonoidalSubCategory_second a >>>> PreMonoidalSubCategory_first b) <~~~>
208 (PreMonoidalSubCategory_first b >>>> PreMonoidalSubCategory_second a).
212 Definition PreMonoidalSubCategory_assoc_ll
214 PreMonoidalSubCategory_second (a⊗b) <~~~>
215 PreMonoidalSubCategory_second b >>>> PreMonoidalSubCategory_second a.
220 Definition PreMonoidalSubCategory_assoc_rr
222 PreMonoidalSubCategory_first (a⊗b) <~~~>
223 PreMonoidalSubCategory_first a >>>> PreMonoidalSubCategory_first b.
228 Definition PreMonoidalSubCategory_I := existT _ pmI (Pobj_unit).
230 Definition PreMonoidalSubCategory_cancelr : PreMonoidalSubCategory_first PreMonoidalSubCategory_I <~~~> functor_id _.
234 Definition PreMonoidalSubCategory_cancell : PreMonoidalSubCategory_second PreMonoidalSubCategory_I <~~~> functor_id _.
238 Instance PreMonoidalSubCategory_PreMonoidal : PreMonoidalCat PreMonoidalSubCategory_is_Binoidal PreMonoidalSubCategory_I :=
239 { pmon_assoc := PreMonoidalSubCategory_assoc
240 ; pmon_assoc_rr := PreMonoidalSubCategory_assoc_rr
241 ; pmon_assoc_ll := PreMonoidalSubCategory_assoc_ll
242 ; pmon_cancelr := PreMonoidalSubCategory_cancelr
243 ; pmon_cancell := PreMonoidalSubCategory_cancell
254 End PreMonoidalSubCategory.