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.
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)
31 * Premonoidal categories actually have three associators (the "f"
32 * indicates the position in which the operation is natural:
34 * assoc : (A ⋊ f) ⋉ C <-> A ⋊ (f ⋉ C)
35 * assoc_rr : (f ⋉ B) ⋉ C <-> f ⋉ (B ⊗ C)
36 * assoc_ll : (A ⋊ B) ⋊ f <-> (A ⊗ B) ⋊ f
38 * Fortunately, in a monoidal category these are all the same natural
39 * isomorphism (and in any case -- monoidal or not -- the objects in
40 * the left column are all the same and the objects in the right
41 * column are all the same). This formalization assumes that is the
42 * case even for premonoidal categories with non-central maps, in
43 * order to keep the complexity manageable. I don't know much about
44 * the consequences of having them and letting them be different; you
45 * might need extra versions of the triangle/pentagon diagrams.
48 Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I ].
49 Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I ].
50 Implicit Arguments pmon_assoc [ Ob Hom C bin_obj' bc I ].
51 Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
53 (* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
54 Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b
55 : #((pmon_cancelr mn) (a ⊗ b)) ~~ #((pmon_assoc mn a EI) b) >>> (a ⋊-) \ #((pmon_cancelr mn) b).
56 set (pmon_pentagon EI EI a b) as penta. unfold pmon_pentagon in penta.
57 set (pmon_triangle a b) as tria. unfold pmon_triangle in tria.
58 apply (fmor_respects(bin_second EI)) in tria.
59 set (@fmor_preserves_comp) as fpc.
60 setoid_rewrite <- fpc in tria.
61 set (ni_commutes (pmon_assoc mn a b)) as xx.
65 Class PreMonoidalFunctor
66 `(PM1:PreMonoidalCat(C:=C1)(I:=I1))
67 `(PM2:PreMonoidalCat(C:=C2)(I:=I2))
69 { mf_F :> Functor C1 C2 fobj
70 ; mf_preserves_i : mf_F I1 ≅ I2
71 ; mf_preserves_first : forall a, bin_first a >>>> mf_F <~~~> mf_F >>>> bin_first (mf_F a)
72 ; mf_preserves_second : forall a, bin_second a >>>> mf_F <~~~> mf_F >>>> bin_second (mf_F a)
73 ; mf_preserves_center : forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
75 Coercion mf_F : PreMonoidalFunctor >-> Functor.
77 (*******************************************************************************)
78 (* Braided and Symmetric Categories *)
80 Class BraidedCat `(mc:PreMonoidalCat) :=
81 { br_niso : forall a, bin_first a <~~~> bin_second a
82 ; br_swap := fun a b => ni_iso (br_niso b) a
83 ; triangleb : forall a:C, #(pmon_cancelr mc a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell mc a)
84 ; hexagon1 : forall {a b c}, #(pmon_assoc mc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc mc _ _ _)
85 ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc mc _ _ _) >>> b ⋊ #(br_swap _ _)
86 ; hexagon2 : forall {a b c}, #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc mc _ _ _)⁻¹
87 ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
90 Class SymmetricCat `(bc:BraidedCat) :=
91 { symcat_swap : forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹