X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FMonoidalCategories_ch7_8.v;h=2872b1fa7ef42fe36a6bd76dbcaedebe004251eb;hp=494e7585a1fe2bc5143ae2119918785cf0b5bd4d;hb=56e6abe14b2cd219b34917d8d5084074394b0839;hpb=77fb38900253b1bc9c4552d474f8564fda398d09

diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v
index 494e758..2872b1f 100644
--- a/src/MonoidalCategories_ch7_8.v
+++ b/src/MonoidalCategories_ch7_8.v
@@ -34,15 +34,10 @@ Class CentralMorphism `{BinoidalCat}`(f:a~>b) : Prop :=
 ; centralmor_second : forall `(g:c~>d), (g ⋉ _ >>> _ ⋊ f) ~~ (_ ⋊ f >>> g ⋉ _)
 }.
 
-(* the central morphisms of a category constitute a subcategory *)
-Definition Center `(bc:BinoidalCat) : SubCategory bc (fun _ => True) (fun _ _ _ _ f => CentralMorphism f).
-  apply Build_SubCategory; intros; apply Build_CentralMorphism; intros.
-  abstract (setoid_rewrite (fmor_preserves_id(bin_first c));
-              setoid_rewrite (fmor_preserves_id(bin_first d));
-              setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
-  abstract (setoid_rewrite (fmor_preserves_id(bin_second c));
-              setoid_rewrite (fmor_preserves_id(bin_second d));
-              setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
+Lemma central_morphisms_compose `{bc:BinoidalCat}{a b c}(f:a~>b)(g:b~>c)
+  : CentralMorphism f -> CentralMorphism g -> CentralMorphism (f >>> g).
+  intros.
+  apply Build_CentralMorphism; intros.
   abstract (setoid_rewrite <- (fmor_preserves_comp(bin_first c0));
               setoid_rewrite associativity;
               setoid_rewrite centralmor_first;
@@ -61,6 +56,19 @@ Definition Center `(bc:BinoidalCat) : SubCategory bc (fun _ => True) (fun _ _ _
               reflexivity).
   Qed.
 
+(* the central morphisms of a category constitute a subcategory *)
+Definition Center `(bc:BinoidalCat) : SubCategory bc (fun _ => True) (fun _ _ _ _ f => CentralMorphism f).
+  apply Build_SubCategory; intros.
+  apply Build_CentralMorphism; intros.
+  abstract (setoid_rewrite (fmor_preserves_id(bin_first c));
+              setoid_rewrite (fmor_preserves_id(bin_first d));
+              setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
+  abstract (setoid_rewrite (fmor_preserves_id(bin_second c));
+              setoid_rewrite (fmor_preserves_id(bin_second d));
+              setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
+  apply central_morphisms_compose; auto.
+  Qed.
+
 Class CommutativeCat `(BinoidalCat) :=
 { commutative_central  :  forall `(f:a~>b), CentralMorphism f
 ; commutative_morprod  := fun `(f:a~>b)`(g:a~>b) => f ⋉ _ >>> _ ⋊ g
@@ -96,8 +104,7 @@ Section BinoidalCat_from_Bifunctor.
           |}.
    Defined.
 
-  (*
-  Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat (BinoidalCat_from_Bifunctor F).
+  Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat BinoidalCat_from_Bifunctor.
   abstract (intros; apply Build_CommutativeCat; intros; apply Build_CentralMorphism; intros; simpl; (
     etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ]; symmetry;
     etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ];
@@ -106,7 +113,7 @@ Section BinoidalCat_from_Bifunctor.
       [ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
       | etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
   Defined.
-  *)
+
 End BinoidalCat_from_Bifunctor.
 
 (* not in Awodey *)
@@ -160,7 +167,6 @@ Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b
   (* FIXME *)
   Admitted.
 
-(* Formalized Definition 3.10 *)
 Class PreMonoidalFunctor
 `(PM1:PreMonoidalCat(C:=C1)(I:=I1))
 `(PM2:PreMonoidalCat(C:=C2)(I:=I2))
@@ -177,29 +183,24 @@ Coercion mf_F : PreMonoidalFunctor >-> Functor.
 (* Braided and Symmetric Categories                                            *)
 
 Class BraidedCat `(mc:PreMonoidalCat) :=
-{ br_swap      :  forall a b,   a⊗b ≅ b⊗a
-; triangleb    :  forall a:C,     #(pmon_cancelr mc a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell mc a)
-; hexagon1     :  forall {a b c}, #(pmon_assoc mc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc mc _ _ _)
-                                  ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc mc _ _ _) >>> b ⋊ #(br_swap _ _)
-; hexagon2     :  forall {a b c}, #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc mc _ _ _)⁻¹
-                                  ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
+{ br_niso        : forall a, bin_first a <~~~> bin_second a
+; br_swap        := fun a b => ni_iso (br_niso b) a
+; triangleb      : forall a:C,     #(pmon_cancelr mc a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell mc a)
+; hexagon1       : forall {a b c}, #(pmon_assoc mc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc mc _ _ _)
+                                   ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc mc _ _ _) >>> b ⋊ #(br_swap _ _)
+; hexagon2       : forall {a b c}, #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc mc _ _ _)⁻¹
+                                   ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
 }.
 
 Class SymmetricCat `(bc:BraidedCat) :=
 { symcat_swap  :  forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
 }.
 
-Class DiagonalCat `(BinoidalCat) :=
-{  copy         :  forall a, a ~> (a⊗a)
-(* copy >> swap == copy  -- only necessary for non-cartesian braided diagonal categories *)
-}.
-
 (* Definition 7.23 *)
 Class MonoidalCat `{C:Category}{Fobj:prod_obj C C -> C}{F:Functor (C ×× C) C Fobj}(I:C) :=
 { mon_f         := F
 ; mon_i         := I
 ; mon_c         := C
-(*; mon_bin       := BinoidalCat_from_Bifunctor mon_f*)
 ; mon_first     := fun a b c (f:a~>b) => F \ pair_mor (pair_obj a c) (pair_obj b c) f (id c)
 ; mon_second    := fun a b c (f:a~>b) => F \ pair_mor (pair_obj c a) (pair_obj c b) (id c) f
 ; mon_cancelr   :  (func_rlecnac I >>>> F) <~~~> functor_id C
@@ -209,19 +210,14 @@ Class MonoidalCat `{C:Category}{Fobj:prod_obj C C -> C}{F:Functor (C ×× C) C F
 ; mon_triangle  :  Triangle mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
                                                  (fun a => #(mon_cancell a)) (fun a => #(mon_cancelr a))
 }.
-
-(* FIXME: show that the endofunctors on any given category form a monoidal category *)
-
 (* Coq manual on coercions: ... only the oldest one is valid and the
  * others are ignored. So the order of declaration of coercions is
  * important. *)
 Coercion mon_c   : MonoidalCat >-> Category.
-(*Coercion mon_bin : MonoidalCat >-> BinoidalCat.*)
 Coercion mon_f   : MonoidalCat >-> Functor.
 Implicit Arguments mon_f [Ob Hom C Fobj F I].
 Implicit Arguments mon_i [Ob Hom C Fobj F I].
 Implicit Arguments mon_c [Ob Hom C Fobj F I].
-(*Implicit Arguments mon_bin [Ob Hom C Fobj F I].*)
 Implicit Arguments MonoidalCat [Ob Hom ].
 
 Section MonoidalCat_is_PreMonoidal.
@@ -374,8 +370,16 @@ End MonoidalCat_is_PreMonoidal.
 
 Hint Extern 1 => apply MonoidalCat_all_central.
 Coercion MonoidalCat_is_PreMonoidal : MonoidalCat >-> PreMonoidalCat.
-(*Lemma CommutativePreMonoidalCategoriesAreMonoidal `(pm:PreMonoidalCat)(cc:CommutativeCat pm) : MonoidalCat pm.*)
 
+(* Later: generalize to premonoidal categories *)
+Class DiagonalCat `(mc:MonoidalCat(F:=F)) :=
+{  copy_nt      :  forall a, functor_id _ ~~~> func_diagonal >>>> F
+;  copy         :  forall (a:mc),   a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
+                := fun a => nt_component _ _ (copy_nt a) a
+(* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)
+}.
+
+(* TO DO: show that the endofunctors on any given category form a monoidal category *)
 Section MonoidalFunctor.
   Context `(m1:MonoidalCat(C:=C1)) `(m2:MonoidalCat(C:=C2)).
   Class MonoidalFunctor {Mobj:C1->C2} (mf_F:Functor C1 C2 Mobj) :=
@@ -433,13 +437,16 @@ Section MonoidalFunctorsCompose.
         apply ni_inv.
         apply mc1.
         apply ni_id.
-    Qed.
+  Defined.
 
   Instance MonoidalFunctorsCompose : MonoidalFunctor m1 m3 (f1 >>>> f2) :=
   { mf_id        := id_comp         (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
   ; mf_coherence := mf_compose_coherence
   }.
-  Admitted.
+  admit.
+  admit.
+  admit.
+  Defined.
 
 End MonoidalFunctorsCompose.
 
@@ -447,10 +454,77 @@ Class CartesianCat `(mc:MonoidalCat) :=
 { car_terminal  : Terminal mc
 ; car_one       : (@one _ _ _ car_terminal) ≅ (mon_i mc)
 ; car_diagonal  : DiagonalCat mc
-; car_law1      : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) _) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell mc _))
-; car_law2      : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) _) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr mc _))
+; car_law1      : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell mc _))
+; car_law2      : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr mc _))
 ; car_mn        := mc
 }.
 Coercion car_diagonal : CartesianCat >-> DiagonalCat.
 Coercion car_terminal : CartesianCat >-> Terminal.
 Coercion car_mn       : CartesianCat >-> MonoidalCat.
+
+Section CenterMonoidal.
+
+  Context `(mc:PreMonoidalCat(I:=pI)).
+
+  Definition CenterMonoidal_Fobj : (Center mc) ×× (Center mc) -> Center mc.
+    intro.
+    destruct X as [a b].
+    destruct a as [a apf].
+    destruct b as [b bpf].
+    exists (a ⊗ b); auto.
+    Defined.
+
+  Definition CenterMonoidal_F_fmor (a b:(Center mc) ×× (Center mc)) : 
+    (a~~{(Center mc) ×× (Center mc)}~~>b) ->
+    ((CenterMonoidal_Fobj a)~~{Center mc}~~>(CenterMonoidal_Fobj b)).
+    destruct a as [[a1 a1'] [a2 a2']].
+    destruct b as [[b1 b1'] [b2 b2']].
+    intro f.
+    destruct f as [[f1 f1'] [f2 f2']].
+    simpl in *.
+    unfold hom.
+    simpl.
+    exists (f1 ⋉ a2 >>> b1 ⋊ f2).
+    apply central_morphisms_compose.
+    admit.
+    admit.
+    Defined.
+
+  Definition CenterMonoidal_F : Functor _ _ CenterMonoidal_Fobj.
+    refine {| fmor := CenterMonoidal_F_fmor |}.
+    intros.
+    destruct a as [[a1 a1'] [a2 a2']].
+    destruct b as [[b1 b1'] [b2 b2']].
+    destruct f as [[f1 f1'] [f2 f2']].
+    destruct f' as [[g1 g1'] [g2 g2']].
+    simpl in *.
+    destruct H.
+    apply comp_respects.
+    set (fmor_respects(-⋉a2)) as q; apply q; auto.
+    set (fmor_respects(b1⋊-)) as q; apply q; auto.
+    intros.
+    destruct a as [[a1 a1'] [a2 a2']].
+    simpl in *.
+    setoid_rewrite (fmor_preserves_id (-⋉a2)).
+    setoid_rewrite (fmor_preserves_id (a1⋊-)).
+    apply left_identity.
+    intros.
+    destruct a as [[a1 a1'] [a2 a2']].
+    destruct b as [[b1 b1'] [b2 b2']].
+    destruct c as [[c1 c1'] [c2 c2']].
+    destruct f as [[f1 f1'] [f2 f2']].
+    destruct g as [[g1 g1'] [g2 g2']].
+    simpl in *.
+    setoid_rewrite juggle3.
+    setoid_rewrite <- (centralmor_first(CentralMorphism:=g1')).
+    setoid_rewrite <- juggle3.
+    setoid_rewrite <- fmor_preserves_comp.
+    reflexivity.
+    Defined.
+
+  Definition CenterMonoidal  : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I).
+    admit.
+    Defined.
+
+End CenterMonoidal.
+