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 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 Section BinoidalCat_from_Bifunctor.
50 Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).
51 Definition BinoidalCat_from_Bifunctor_first (a:C) : Functor C C (fun b => Fobj (pair_obj b a)).
52 apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
53 @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;
54 [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
55 | abstract (set (fmor_preserves_id(F)) as q; apply q)
56 | abstract (etransitivity;
57 [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
58 | set (fmor_respects(F)) as q; apply q ];
59 split; simpl; auto) ].
61 Definition BinoidalCat_from_Bifunctor_second (a:C) : Functor C C (fun b => Fobj (pair_obj a b)).
62 apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
63 @fmor _ _ _ _ _ _ _ F (pair_obj a a0) (pair_obj a b) (pair_mor (pair_obj a a0) (pair_obj a b) (id a) f))); intros;
64 [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
65 | abstract (set (fmor_preserves_id(F)) as q; apply q)
66 | abstract (etransitivity;
67 [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
68 | set (fmor_respects(F)) as q; apply q ];
69 split; simpl; auto) ].
72 Definition BinoidalCat_from_Bifunctor : BinoidalCat C (fun a b => Fobj (pair_obj a b)).
73 refine {| bin_first := BinoidalCat_from_Bifunctor_first
74 ; bin_second := BinoidalCat_from_Bifunctor_second
78 Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat BinoidalCat_from_Bifunctor.
79 abstract (intros; apply Build_CommutativeCat; intros; apply Build_CentralMorphism; intros; simpl; (
80 etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ]; symmetry;
81 etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ];
82 apply (fmor_respects(F));
84 [ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
85 | etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
88 (* if this binoidal structure has all of the natural isomorphisms of a premonoidal category, then it's monoidal *)
89 Context {pmI}(pm:PreMonoidalCat BinoidalCat_from_Bifunctor pmI).
91 Instance PreMonoidalCat_from_bifunctor_is_Monoidal : MonoidalCat pm :=
92 { mon_commutative := Bifunctors_Create_Commutative_Binoidal_Categories
95 End BinoidalCat_from_Bifunctor.
98 (* we can go the other way: given a monoidal category, its left/right functors can be combined into a bifunctor *)
99 Section Bifunctor_from_MonoidalCat.
100 Context `(M:MonoidalCat).
103 Definition Bifunctor_from_MonoidalCat_fobj : M ×× M -> M.
106 exact (bin_obj' o o0).
109 Definition Bifunctor_from_MonoidalCat_fmor {a}{b}(f:a~~{M××M}~~>b)
110 : (Bifunctor_from_MonoidalCat_fobj a)~~{M}~~>(Bifunctor_from_MonoidalCat_fobj b).
111 destruct a; destruct b; destruct f.
113 apply (h ⋉ _ >>> _ ⋊ h0).
116 Instance Bifunctor_from_MonoidalCat : Functor (M ×× M) M Bifunctor_from_MonoidalCat_fobj :=
117 { fmor := fun x y f => Bifunctor_from_MonoidalCat_fmor f }.
119 destruct a; destruct b; destruct f; destruct f'; simpl in *.
122 apply (fmor_respects (-⋉o0)); auto.
123 apply (fmor_respects (o1⋊-)); auto.
124 intros; destruct a; simpl in *.
125 setoid_rewrite (fmor_preserves_id (-⋉o0)).
126 setoid_rewrite left_identity.
127 apply fmor_preserves_id.
128 intros; destruct a; destruct b; destruct c; destruct f; destruct g; simpl in *.
129 setoid_rewrite <- fmor_preserves_comp.
130 setoid_rewrite juggle3 at 1.
131 assert (CentralMorphism h1).
132 apply mon_commutative.
133 setoid_rewrite <- (centralmor_first(CentralMorphism:=H)).
134 setoid_rewrite <- juggle3.
138 End Bifunctor_from_MonoidalCat.
141 Class DiagonalCat `(mc:MonoidalCat) :=
142 { copy : forall (a:mc), a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
143 ; copy_natural1 : forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> f ⋉ a >>> b ⋊ f ~~ f >>> copy _
144 ; copy_natural2 : forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> a ⋊ f >>> f ⋉ b ~~ f >>> copy _
145 (* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)
148 Class CartesianCat `(mc:MonoidalCat) :=
149 { car_terminal :> TerminalObject mc pmon_I
150 ; car_diagonal : DiagonalCat mc
151 ; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (drop a ⋉ a) >>> (#(pmon_cancell _))
152 ; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ drop a) >>> (#(pmon_cancelr _))
155 Coercion car_diagonal : CartesianCat >-> DiagonalCat.
156 Coercion car_terminal : CartesianCat >-> TerminalObject.
157 Coercion car_mn : CartesianCat >-> MonoidalCat.