src/MonoidalCategories_ch7_8.v

   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
  13 (******************************************************************************)
  14 (* Chapter 7.8: (Pre)Monoidal Categories                                      *)
  15 (******************************************************************************)
  16
  17 Class BinoidalCat
  18 `( C                  :  Category                               )
  19 ( bin_obj'            :  C -> C -> C                            ) :=
  20 { bin_obj             := bin_obj' where "a ⊗ b" := (bin_obj a b)
  21 ; bin_first           :  forall a:C, Functor C C (fun x => x⊗a)
  22 ; bin_second          :  forall a:C, Functor C C (fun x => a⊗x)
  23 ; bin_c               := C
  24 }.
  25 Coercion bin_c : BinoidalCat >-> Category.
  26 Notation "a ⊗ b"  := (@bin_obj _ _ _ _ _ a b)                              : category_scope.
  27 Notation "C ⋊ f"  := (@fmor _ _ _ _ _ _ _ (@bin_second _ _ _ _ _ C) _ _ f) : category_scope.
  28 Notation "g ⋉ C"  := (@fmor _ _ _ _ _ _ _ (@bin_first _ _ _ _ _ C) _ _ g)  : category_scope.
  29 Notation "C ⋊ -"  := (@bin_second _ _ _ _ _ C)                             : category_scope.
  30 Notation "- ⋉ C"  := (@bin_first _ _ _ _ _ C)                              : category_scope.
  31
  32 Class CentralMorphism `{BinoidalCat}`(f:a~>b) : Prop :=
  33 { centralmor_first  : forall `(g:c~>d), (f ⋉ _ >>> _ ⋊ g) ~~ (_ ⋊ g >>> f ⋉ _)
  34 ; centralmor_second : forall `(g:c~>d), (g ⋉ _ >>> _ ⋊ f) ~~ (_ ⋊ f >>> g ⋉ _)
  35 }.
  36
  37 Lemma central_morphisms_compose `{bc:BinoidalCat}{a b c}(f:a~>b)(g:b~>c)
  38   : CentralMorphism f -> CentralMorphism g -> CentralMorphism (f >>> g).
  39   intros.
  40   apply Build_CentralMorphism; intros.
  41   abstract (setoid_rewrite <- (fmor_preserves_comp(bin_first c0));
  42               setoid_rewrite associativity;
  43               setoid_rewrite centralmor_first;
  44               setoid_rewrite <- associativity;
  45               setoid_rewrite centralmor_first;
  46               setoid_rewrite associativity;
  47               setoid_rewrite <- (fmor_preserves_comp(bin_first d));
  48               reflexivity).
  49   abstract (setoid_rewrite <- (fmor_preserves_comp(bin_second d));
  50               setoid_rewrite <- associativity;
  51               setoid_rewrite centralmor_second;
  52               setoid_rewrite associativity;
  53               setoid_rewrite centralmor_second;
  54               setoid_rewrite <- associativity;
  55               setoid_rewrite <- (fmor_preserves_comp(bin_second c0));
  56               reflexivity).
  57   Qed.
  58
  59 (* the central morphisms of a category constitute a subcategory *)
  60 Definition Center `(bc:BinoidalCat) : SubCategory bc (fun _ => True) (fun _ _ _ _ f => CentralMorphism f).
  61   apply Build_SubCategory; intros.
  62   apply Build_CentralMorphism; intros.
  63   abstract (setoid_rewrite (fmor_preserves_id(bin_first c));
  64               setoid_rewrite (fmor_preserves_id(bin_first d));
  65               setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
  66   abstract (setoid_rewrite (fmor_preserves_id(bin_second c));
  67               setoid_rewrite (fmor_preserves_id(bin_second d));
  68               setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
  69   apply central_morphisms_compose; auto.
  70   Qed.
  71
  72 Class CommutativeCat `(BinoidalCat) :=
  73 { commutative_central  :  forall `(f:a~>b), CentralMorphism f
  74 ; commutative_morprod  := fun `(f:a~>b)`(g:a~>b) => f ⋉ _ >>> _ ⋊ g
  75 }.
  76 Notation "f × g"    := (commutative_morprod f g).
  77
  78 Section BinoidalCat_from_Bifunctor.
  79   Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).
  80   Definition BinoidalCat_from_Bifunctor_first (a:C) : Functor C C (fun b => Fobj (pair_obj b a)).
  81   apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
  82     @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;
  83     [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
  84     | abstract (set (fmor_preserves_id(F)) as q; apply q)
  85     | abstract (etransitivity;
  86       [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
  87       | set (fmor_respects(F)) as q; apply q ];
  88       split; simpl; auto) ].
  89   Defined.
  90   Definition BinoidalCat_from_Bifunctor_second (a:C) : Functor C C (fun b => Fobj (pair_obj a b)).
  91   apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
  92     @fmor _ _ _ _ _ _ _ F (pair_obj a a0) (pair_obj a b) (pair_mor (pair_obj a a0) (pair_obj a b) (id a) f))); intros;
  93     [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
  94     | abstract (set (fmor_preserves_id(F)) as q; apply q)
  95     | abstract (etransitivity;
  96       [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
  97       | set (fmor_respects(F)) as q; apply q ];
  98       split; simpl; auto) ].
  99   Defined.
 100
 101   Definition BinoidalCat_from_Bifunctor : BinoidalCat C (fun a b => Fobj (pair_obj a b)).
 102    refine {| bin_first  := BinoidalCat_from_Bifunctor_first
 103            ; bin_second := BinoidalCat_from_Bifunctor_second
 104           |}.
 105    Defined.
 106
 107   Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat BinoidalCat_from_Bifunctor.
 108   abstract (intros; apply Build_CommutativeCat; intros; apply Build_CentralMorphism; intros; simpl; (
 109     etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ]; symmetry;
 110     etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ];
 111     apply (fmor_respects(F));
 112     split;
 113       [ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
 114       | etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
 115   Defined.
 116
 117 End BinoidalCat_from_Bifunctor.
 118
 119 (* not in Awodey *)
 120 Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
 121 { pmon_I          := I
 122 ; pmon_bin        := bc
 123 ; pmon_cat        := C
 124 ; pmon_assoc      : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
 125 ; pmon_cancelr    :                               (bin_first I) <~~~> functor_id C
 126 ; pmon_cancell    :                              (bin_second I) <~~~> functor_id C
 127 ; 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))
 128 ; 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))
 129                              (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
 130 ; pmon_assoc_rr   :  forall a b, (bin_first  (a⊗b)) <~~~> (bin_first  a >>>> bin_first  b)
 131 ; pmon_assoc_ll   :  forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
 132 ; pmon_coherent_r :  forall a c d:C,  #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
 133 ; pmon_coherent_l :  forall a c d:C,  #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
 134 }.
 135 (*
 136  * Premonoidal categories actually have three associators (the "f"
 137  * indicates the position in which the operation is natural:
 138  *
 139  *  assoc    : (A ⋊ f) ⋉ C <->  A ⋊ (f ⋉  C)
 140  *  assoc_rr : (f ⋉ B) ⋉ C <->  f ⋉ (B  ⊗ C)
 141  *  assoc_ll : (A ⋊ B) ⋊ f <-> (A ⊗  B) ⋊ f
 142  *
 143  * Fortunately, in a monoidal category these are all the same natural
 144  * isomorphism (and in any case -- monoidal or not -- the objects in
 145  * the left column are all the same and the objects in the right
 146  * column are all the same).  This formalization assumes that is the
 147  * case even for premonoidal categories with non-central maps, in
 148  * order to keep the complexity manageable.  I don't know much about
 149  * the consequences of having them and letting them be different; you
 150  * might need extra versions of the triangle/pentagon diagrams.
 151  *)
 152
 153 Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I ].
 154 Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I ].
 155 Implicit Arguments pmon_assoc   [ Ob Hom C bin_obj' bc I ].
 156 Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
 157
 158 (* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
 159 Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b
 160   : #((pmon_cancelr mn) (a ⊗ b)) ~~ #((pmon_assoc mn a EI) b) >>> (a ⋊-) \ #((pmon_cancelr mn) b).
 161   set (pmon_pentagon EI EI a b) as penta. unfold pmon_pentagon in penta.
 162   set (pmon_triangle a b) as tria. unfold pmon_triangle in tria.
 163   apply (fmor_respects(bin_second EI)) in tria.
 164   set (@fmor_preserves_comp) as fpc.
 165   setoid_rewrite <- fpc in tria.
 166   set (ni_commutes (pmon_assoc mn a b)) as xx.
 167   (* FIXME *)
 168   Admitted.
 169
 170 Class PreMonoidalFunctor
 171 `(PM1:PreMonoidalCat(C:=C1)(I:=I1))
 172 `(PM2:PreMonoidalCat(C:=C2)(I:=I2))
 173  (fobj : C1 -> C2          ) :=
 174 { mf_F                :> Functor C1 C2 fobj
 175 ; mf_preserves_i      :  mf_F I1 ≅ I2
 176 ; mf_preserves_first  :  forall a,   bin_first a >>>> mf_F  <~~~>  mf_F >>>> bin_first  (mf_F a)
 177 ; mf_preserves_second :  forall a,  bin_second a >>>> mf_F  <~~~>  mf_F >>>> bin_second (mf_F a)
 178 ; mf_preserves_center :  forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
 179 }.
 180 Coercion mf_F : PreMonoidalFunctor >-> Functor.
 181
 182 (*******************************************************************************)
 183 (* Braided and Symmetric Categories                                            *)
 184
 185 Class BraidedCat `(mc:PreMonoidalCat) :=
 186 { br_niso        : forall a, bin_first a <~~~> bin_second a
 187 ; br_swap        := fun a b => ni_iso (br_niso b) a
 188 ; triangleb      : forall a:C,     #(pmon_cancelr mc a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell mc a)
 189 ; hexagon1       : forall {a b c}, #(pmon_assoc mc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc mc _ _ _)
 190                                    ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc mc _ _ _) >>> b ⋊ #(br_swap _ _)
 191 ; hexagon2       : forall {a b c}, #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc mc _ _ _)⁻¹
 192                                    ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
 193 }.
 194
 195 Class SymmetricCat `(bc:BraidedCat) :=
 196 { symcat_swap  :  forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
 197 }.
 198
 199 (* Definition 7.23 *)
 200 Class MonoidalCat `{C:Category}{Fobj:prod_obj C C -> C}{F:Functor (C ×× C) C Fobj}(I:C) :=
 201 { mon_f         := F
 202 ; mon_i         := I
 203 ; mon_c         := C
 204 ; mon_first     := fun a b c (f:a~>b) => F \ pair_mor (pair_obj a c) (pair_obj b c) f (id c)
 205 ; mon_second    := fun a b c (f:a~>b) => F \ pair_mor (pair_obj c a) (pair_obj c b) (id c) f
 206 ; mon_cancelr   :  (func_rlecnac I >>>> F) <~~~> functor_id C
 207 ; mon_cancell   :  (func_llecnac I >>>> F) <~~~> functor_id C
 208 ; mon_assoc     :  ((F **** (functor_id C)) >>>> F) <~~~> func_cossa >>>> ((((functor_id C) **** F) >>>> F))
 209 ; mon_pentagon  :  Pentagon mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
 210 ; mon_triangle  :  Triangle mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
 211                                                  (fun a => #(mon_cancell a)) (fun a => #(mon_cancelr a))
 212 }.
 213 (* Coq manual on coercions: ... only the oldest one is valid and the
 214  * others are ignored. So the order of declaration of coercions is
 215  * important. *)
 216 Coercion mon_c   : MonoidalCat >-> Category.
 217 Coercion mon_f   : MonoidalCat >-> Functor.
 218 Implicit Arguments mon_f [Ob Hom C Fobj F I].
 219 Implicit Arguments mon_i [Ob Hom C Fobj F I].
 220 Implicit Arguments mon_c [Ob Hom C Fobj F I].
 221 Implicit Arguments MonoidalCat [Ob Hom ].
 222
 223 Section MonoidalCat_is_PreMonoidal.
 224   Context `(M:MonoidalCat).
 225   Definition mon_bin_M := BinoidalCat_from_Bifunctor (mon_f M).
 226   Existing Instance mon_bin_M.
 227   Lemma mon_pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a).
 228     intros.
 229     set (fun c => mon_assoc (pair_obj (pair_obj a c) b)) as qq.
 230     simpl in qq.
 231     apply Build_NaturalIsomorphism with (ni_iso:=qq).
 232     abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
 233                     (pair_mor (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
 234                     (pair_mor (pair_obj a A) (pair_obj a B) (id a) f) (id b))) as qr;
 235              apply qr).
 236     Defined.
 237
 238   Lemma mon_pmon_assoc_rr   :  forall a b, (bin_first  (a⊗b)) <~~~> (bin_first  a >>>> bin_first  b).
 239     intros.
 240     set (fun c:C => mon_assoc (pair_obj (pair_obj c a) b)) as qq.
 241     simpl in qq.
 242     apply ni_inv.
 243     apply Build_NaturalIsomorphism with (ni_iso:=qq).
 244     abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
 245                     (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
 246                     (pair_mor (pair_obj _ _) (pair_obj _ _) f (id a)) (id b))) as qr;
 247               etransitivity; [ idtac | apply qr ];
 248               apply comp_respects; try reflexivity;
 249               unfold mon_f;
 250               simpl;
 251               apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
 252               split; try reflexivity;
 253               symmetry;
 254               simpl;
 255               set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
 256               simpl in qqqq;
 257               apply qqqq).
 258    Defined.
 259
 260   Lemma mon_pmon_assoc_ll   :  forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a).
 261     intros.
 262     set (fun c:C => mon_assoc (pair_obj (pair_obj a b) c)) as qq.
 263     simpl in qq.
 264     set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (Fobj (pair_obj a b) ⋊-) (b ⋊- >>>> a ⋊-)) as qqq.
 265     set (qqq qq) as q'.
 266     apply q'.
 267     clear q'.
 268     clear qqq.
 269     abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
 270                     (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
 271                     (pair_mor (pair_obj _ _) (pair_obj _ _) (id a) (id b)) f)) as qr;
 272               etransitivity; [ apply qr | idtac ];
 273               apply comp_respects; try reflexivity;
 274               unfold mon_f;
 275               simpl;
 276               apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
 277               split; try reflexivity;
 278               simpl;
 279               set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
 280               simpl in qqqq;
 281               apply qqqq).
 282     Defined.
 283
 284   Lemma mon_pmon_cancelr : (bin_first I0) <~~~> functor_id C.
 285     set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_first I0) (functor_id C)) as qq.
 286     set (mon_cancelr) as z.
 287     simpl in z.
 288     simpl in qq.
 289     set (qq z) as zz.
 290     apply zz.
 291     abstract (intros;
 292               set (ni_commutes mon_cancelr) as q; simpl in *;
 293               apply q).
 294     Defined.
 295
 296   Lemma mon_pmon_cancell : (bin_second I0) <~~~> functor_id C.
 297     set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_second I0) (functor_id C)) as qq.
 298     set (mon_cancell) as z.
 299     simpl in z.
 300     simpl in qq.
 301     set (qq z) as zz.
 302     apply zz.
 303     abstract (intros;
 304               set (ni_commutes mon_cancell) as q; simpl in *;
 305               apply q).
 306     Defined.
 307
 308   Lemma mon_pmon_triangle : forall a b, #(mon_pmon_cancelr a) ⋉ b ~~ #(mon_pmon_assoc _ _ _) >>> a ⋊ #(mon_pmon_cancell b).
 309     intros.
 310     set mon_triangle as q.
 311     simpl in q.
 312     apply q.
 313     Qed.
 314
 315   Lemma mon_pmon_pentagon a b c d : (#(mon_pmon_assoc a c b ) ⋉ d)  >>>
 316                                      #(mon_pmon_assoc a d _ )   >>>
 317                                 (a ⋊ #(mon_pmon_assoc b d c))
 318                                   ~~ #(mon_pmon_assoc _ d c )   >>>
 319                                      #(mon_pmon_assoc a _ b ).
 320     set (@pentagon _ _ _ _ _ _ _ mon_pentagon) as x.
 321     simpl in x.
 322     unfold bin_obj.
 323     unfold mon_first in x.
 324     simpl in *.
 325     apply x.
 326     Qed.
 327
 328   Definition MonoidalCat_is_PreMonoidal : PreMonoidalCat (BinoidalCat_from_Bifunctor (mon_f M)) (mon_i M).
 329     refine {| pmon_assoc                 := mon_pmon_assoc
 330             ; pmon_cancell               := mon_pmon_cancell
 331             ; pmon_cancelr               := mon_pmon_cancelr
 332             ; pmon_triangle              := {| triangle := mon_pmon_triangle |}
 333             ; pmon_pentagon              := {| pentagon := mon_pmon_pentagon |}
 334             ; pmon_assoc_ll              := mon_pmon_assoc_ll
 335             ; pmon_assoc_rr              := mon_pmon_assoc_rr
 336             |}.
 337     abstract (set (coincide mon_triangle) as qq; simpl in *; apply qq).
 338     abstract (intros; simpl; reflexivity).
 339     abstract (intros; simpl; reflexivity).
 340     Defined.
 341
 342   Lemma MonoidalCat_all_central : forall a b (f:a~~{M}~~>b), CentralMorphism f.
 343     intros;
 344     set (@fmor_preserves_comp _ _ _ _ _ _ _ M) as fc.
 345     apply Build_CentralMorphism;
 346     intros; simpl in *.
 347     etransitivity.
 348       apply fc.
 349       symmetry.
 350       etransitivity.
 351       apply fc.
 352       apply (fmor_respects M).
 353       simpl.
 354       setoid_rewrite left_identity;
 355       setoid_rewrite right_identity;
 356       split; reflexivity.
 357     etransitivity.
 358       apply fc.
 359       symmetry.
 360       etransitivity.
 361       apply fc.
 362       apply (fmor_respects M).
 363       simpl.
 364       setoid_rewrite left_identity;
 365       setoid_rewrite right_identity;
 366       split; reflexivity.
 367     Qed.
 368
 369 End MonoidalCat_is_PreMonoidal.
 370
 371 Hint Extern 1 => apply MonoidalCat_all_central.
 372 Coercion MonoidalCat_is_PreMonoidal : MonoidalCat >-> PreMonoidalCat.
 373
 374 (* Later: generalize to premonoidal categories *)
 375 Class DiagonalCat `(mc:MonoidalCat(F:=F)) :=
 376 {  copy_nt      :  forall a, functor_id _ ~~~> func_diagonal >>>> F
 377 ;  copy         :  forall (a:mc),   a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
 378                 := fun a => nt_component _ _ (copy_nt a) a
 379 (* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)
 380 }.
 381
 382 (* TO DO: show that the endofunctors on any given category form a monoidal category *)
 383 Section MonoidalFunctor.
 384   Context `(m1:MonoidalCat(C:=C1)) `(m2:MonoidalCat(C:=C2)).
 385   Class MonoidalFunctor {Mobj:C1->C2} (mf_F:Functor C1 C2 Mobj) :=
 386   { mf_f         := mf_F where "f ⊕⊕ g" := (@fmor _ _ _ _ _ _ _ m2 _ _ (pair_mor (pair_obj _ _) (pair_obj _ _) f g))
 387   ; mf_coherence :  (mf_F **** mf_F) >>>> (mon_f m2) <~~~> (mon_f m1) >>>> mf_F
 388   ; mf_phi       := fun a b => #(mf_coherence (pair_obj a b))
 389   ; mf_id        :  (mon_i m2) ≅ (mf_F (mon_i m1))
 390   ; mf_cancelr   :  forall a,    #(mon_cancelr(MonoidalCat:=m2) (mf_F a)) ~~
 391                                   (id (mf_F a)) ⊕⊕ #mf_id >>> mf_phi a (mon_i _) >>> mf_F \ #(mon_cancelr a)
 392   ; mf_cancell   :  forall b,    #(mon_cancell (mf_F b)) ~~
 393                                  #mf_id ⊕⊕ (id (mf_F b)) >>> mf_phi (mon_i _) b >>> mf_F \ #(mon_cancell b)
 394   ; mf_assoc     :  forall a b c, (mf_phi a b) ⊕⊕ (id (mf_F c)) >>> (mf_phi _ c) >>>
 395                                   (mf_F \ #(mon_assoc (pair_obj (pair_obj a b) c) )) ~~
 396                                           #(mon_assoc (pair_obj (pair_obj _ _) _) )  >>>
 397                                   (id (mf_F a)) ⊕⊕ (mf_phi b c) >>> (mf_phi a _)
 398   }.
 399 End MonoidalFunctor.
 400 Coercion mf_f : MonoidalFunctor >-> Functor.
 401 Implicit Arguments mf_coherence [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
 402 Implicit Arguments mf_id        [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
 403
 404 Section MonoidalFunctorsCompose.
 405   Context `(m1:MonoidalCat).
 406   Context `(m2:MonoidalCat).
 407   Context `(m3:MonoidalCat).
 408   Context  {f1obj}(f1:@Functor _ _ m1 _ _ m2 f1obj).
 409   Context  {f2obj}(f2:@Functor _ _ m2 _ _ m3 f2obj).
 410   Context  (mf1:MonoidalFunctor m1 m2 f1).
 411   Context  (mf2:MonoidalFunctor m2 m3 f2).
 412
 413   Lemma mf_compose_coherence : (f1 >>>> f2) **** (f1 >>>> f2) >>>> m3 <~~~> m1 >>>> (f1 >>>> f2).
 414     set (mf_coherence mf1) as mc1.
 415     set (mf_coherence mf2) as mc2.
 416     set (@ni_comp) as q.
 417     set (q _ _ _ _ _ _ _ ((f1 >>>> f2) **** (f1 >>>> f2) >>>> m3) _ ((f1 **** f1 >>>> m2) >>>> f2) _ (m1 >>>> (f1 >>>> f2))) as qq.
 418     apply qq; clear qq; clear q.
 419     apply (@ni_comp _ _ _ _ _ _ _ _ _ (f1 **** f1 >>>> (f2 **** f2 >>>> m3)) _ _).
 420     apply (@ni_comp _ _ _ _ _ _ _ _ _ ((f1 **** f1 >>>> f2 **** f2) >>>> m3) _ _).
 421     eapply ni_respects.
 422       apply ni_prod_comp.
 423       apply ni_id.
 424     apply ni_associativity.
 425     apply ni_inv.
 426     eapply ni_comp.
 427       apply (ni_associativity (f1 **** f1) m2 f2).
 428       apply (ni_respects (F0:=f1 **** f1)(F1:=f1 **** f1)(G0:=(m2 >>>> f2))(G1:=(f2 **** f2 >>>> m3))).
 429         apply ni_id.
 430         apply ni_inv.
 431         apply mc2.
 432     apply ni_inv.
 433     eapply ni_comp.
 434       eapply ni_inv.
 435       apply (ni_associativity m1 f1 f2).
 436       apply ni_respects.
 437         apply ni_inv.
 438         apply mc1.
 439         apply ni_id.
 440   Defined.
 441
 442   Instance MonoidalFunctorsCompose : MonoidalFunctor m1 m3 (f1 >>>> f2) :=
 443   { mf_id        := id_comp         (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
 444   ; mf_coherence := mf_compose_coherence
 445   }.
 446   admit.
 447   admit.
 448   admit.
 449   Defined.
 450
 451 End MonoidalFunctorsCompose.
 452
 453 Class CartesianCat `(mc:MonoidalCat) :=
 454 { car_terminal  : Terminal mc
 455 ; car_one       : (@one _ _ _ car_terminal) ≅ (mon_i mc)
 456 ; car_diagonal  : DiagonalCat mc
 457 ; car_law1      : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell mc _))
 458 ; car_law2      : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr mc _))
 459 ; car_mn        := mc
 460 }.
 461 Coercion car_diagonal : CartesianCat >-> DiagonalCat.
 462 Coercion car_terminal : CartesianCat >-> Terminal.
 463 Coercion car_mn       : CartesianCat >-> MonoidalCat.
 464
 465 Section CenterMonoidal.
 466
 467   Context `(mc:PreMonoidalCat(I:=pI)).
 468
 469   Definition CenterMonoidal_Fobj : (Center mc) ×× (Center mc) -> Center mc.
 470     intro.
 471     destruct X as [a b].
 472     destruct a as [a apf].
 473     destruct b as [b bpf].
 474     exists (a ⊗ b); auto.
 475     Defined.
 476
 477   Definition CenterMonoidal_F_fmor (a b:(Center mc) ×× (Center mc)) :
 478     (a~~{(Center mc) ×× (Center mc)}~~>b) ->
 479     ((CenterMonoidal_Fobj a)~~{Center mc}~~>(CenterMonoidal_Fobj b)).
 480     destruct a as [[a1 a1'] [a2 a2']].
 481     destruct b as [[b1 b1'] [b2 b2']].
 482     intro f.
 483     destruct f as [[f1 f1'] [f2 f2']].
 484     simpl in *.
 485     unfold hom.
 486     simpl.
 487     exists (f1 ⋉ a2 >>> b1 ⋊ f2).
 488     apply central_morphisms_compose.
 489     admit.
 490     admit.
 491     Defined.
 492
 493   Definition CenterMonoidal_F : Functor _ _ CenterMonoidal_Fobj.
 494     refine {| fmor := CenterMonoidal_F_fmor |}.
 495     intros.
 496     destruct a as [[a1 a1'] [a2 a2']].
 497     destruct b as [[b1 b1'] [b2 b2']].
 498     destruct f as [[f1 f1'] [f2 f2']].
 499     destruct f' as [[g1 g1'] [g2 g2']].
 500     simpl in *.
 501     destruct H.
 502     apply comp_respects.
 503     set (fmor_respects(-⋉a2)) as q; apply q; auto.
 504     set (fmor_respects(b1⋊-)) as q; apply q; auto.
 505     intros.
 506     destruct a as [[a1 a1'] [a2 a2']].
 507     simpl in *.
 508     setoid_rewrite (fmor_preserves_id (-⋉a2)).
 509     setoid_rewrite (fmor_preserves_id (a1⋊-)).
 510     apply left_identity.
 511     intros.
 512     destruct a as [[a1 a1'] [a2 a2']].
 513     destruct b as [[b1 b1'] [b2 b2']].
 514     destruct c as [[c1 c1'] [c2 c2']].
 515     destruct f as [[f1 f1'] [f2 f2']].
 516     destruct g as [[g1 g1'] [g2 g2']].
 517     simpl in *.
 518     setoid_rewrite juggle3.
 519     setoid_rewrite <- (centralmor_first(CentralMorphism:=g1')).
 520     setoid_rewrite <- juggle3.
 521     setoid_rewrite <- fmor_preserves_comp.
 522     reflexivity.
 523     Defined.
 524
 525   Definition CenterMonoidal  : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I).
 526     admit.
 527     Defined.
 528
 529 End CenterMonoidal.
 530