X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FPreMonoidalCategories.v;h=e09f8abb775a3e4d5b2bd3ea04875ebf5196767f;hp=7d9699b8df07c7e6192a81a15aae4c8834e43d3c;hb=27ffdd2265eb1c15acc62970f49d25a07bcadb05;hpb=b0262af94b62376527556d79b10c4f1de29a9565

diff --git a/src/PreMonoidalCategories.v b/src/PreMonoidalCategories.v
index 7d9699b..e09f8ab 100644
--- a/src/PreMonoidalCategories.v
+++ b/src/PreMonoidalCategories.v
@@ -3,7 +3,6 @@ Require Import Preamble.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
 Require Import InitialTerminal_ch2_2.
 Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
@@ -13,19 +12,22 @@ Require Import BinoidalCategories.
 
 (* not in Awodey *)
 Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
-{ pmon_I          := I
-; pmon_bin        := bc
-; pmon_cat        := C
-; pmon_assoc      : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
-; pmon_cancelr    :                               (bin_first I) <~~~> functor_id C
-; pmon_cancell    :                              (bin_second I) <~~~> functor_id C
-; 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))
-; 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))
-                             (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
-; pmon_assoc_rr   :  forall a b, (bin_first  (a⊗b)) <~~~> (bin_first  a >>>> bin_first  b)
-; pmon_assoc_ll   :  forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
-; pmon_coherent_r :  forall a c d:C,  #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
-; pmon_coherent_l :  forall a c d:C,  #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
+{ pmon_I               := I
+; pmon_bin             := bc
+; pmon_cat             := C
+; pmon_assoc           : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
+; pmon_cancelr         :                               (bin_first I) <~~~> functor_id C
+; pmon_cancell         :                              (bin_second I) <~~~> functor_id C
+; 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))
+; 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))
+                                  (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
+; pmon_assoc_rr        :  forall a b, (bin_first  (a⊗b)) <~~~> (bin_first  a >>>> bin_first  b)
+; pmon_assoc_ll        :  forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
+; pmon_coherent_r      :  forall a c d:C,  #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
+; pmon_coherent_l      :  forall a c d:C,  #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
+; pmon_assoc_central   :  forall a b c, CentralMorphism #(pmon_assoc   a b c)
+; pmon_cancelr_central :  forall a    , CentralMorphism #(pmon_cancelr a)
+; pmon_cancell_central :  forall a    , CentralMorphism #(pmon_cancell a)
 }.
 (*
  * Premonoidal categories actually have three associators (the "f"
@@ -45,20 +47,20 @@ Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
  * might need extra versions of the triangle/pentagon diagrams.
  *)
 
-Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I ].
-Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I ].
-Implicit Arguments pmon_assoc   [ Ob Hom C bin_obj' bc I ].
+Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
+Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
+Implicit Arguments pmon_assoc   [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
 Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
 
 (* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
 Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b
-  : #((pmon_cancelr mn) (a ⊗ b)) ~~ #((pmon_assoc mn a EI) b) >>> (a ⋊-) \ #((pmon_cancelr mn) b).
+  : #(pmon_cancelr (a ⊗ b)) ~~ #((pmon_assoc a EI) b) >>> (a ⋊-) \ #(pmon_cancelr b).
   set (pmon_pentagon EI EI a b) as penta. unfold pmon_pentagon in penta.
   set (pmon_triangle a b) as tria. unfold pmon_triangle in tria.
   apply (fmor_respects(bin_second EI)) in tria.
   set (@fmor_preserves_comp) as fpc.
   setoid_rewrite <- fpc in tria.
-  set (ni_commutes (pmon_assoc mn a b)) as xx.
+  set (ni_commutes (pmon_assoc a b)) as xx.
   (* FIXME *)
   Admitted.
 
@@ -66,27 +68,187 @@ Class PreMonoidalFunctor
 `(PM1:PreMonoidalCat(C:=C1)(I:=I1))
 `(PM2:PreMonoidalCat(C:=C2)(I:=I2))
  (fobj : C1 -> C2          ) :=
-{ mf_F                :> Functor C1 C2 fobj
-; mf_preserves_i      :  mf_F I1 ≅ I2
-; mf_preserves_first  :  forall a,   bin_first a >>>> mf_F  <~~~>  mf_F >>>> bin_first  (mf_F a)
-; mf_preserves_second :  forall a,  bin_second a >>>> mf_F  <~~~>  mf_F >>>> bin_second (mf_F a)
-; mf_preserves_center :  forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
+{ mf_F          :> Functor C1 C2 fobj
+; mf_i          :  I2 ≅ mf_F I1
+; mf_first      :  ∀ a,              mf_F >>>> bin_first  (mf_F a)  <~~~>  bin_first  a >>>> mf_F
+; mf_second     :  ∀ a,              mf_F >>>> bin_second (mf_F a)  <~~~>  bin_second a >>>> mf_F
+; mf_consistent :  ∀ a b,            #(mf_first a b) ~~ #(mf_second b a)
+; mf_center     :  forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
+; mf_cancell    :  ∀ b,     #(pmon_cancell _) ~~ #mf_i ⋉ _ >>> #(mf_first  b I1) >>> mf_F \ #(pmon_cancell b)
+; mf_cancelr    :  ∀ a,     #(pmon_cancelr _) ~~ _ ⋊ #mf_i >>> #(mf_second a I1) >>> mf_F \ #(pmon_cancelr a)
+; mf_assoc      :  ∀ a b c, #(pmon_assoc _ _ _)  >>> _ ⋊ #(mf_second _ _) >>>        #(mf_second _ _) ~~
+                            #(mf_second _ _) ⋉ _ >>>     #(mf_second _ _) >>> mf_F \ #(pmon_assoc a c b)
 }.
 Coercion mf_F : PreMonoidalFunctor >-> Functor.
 
+Definition PreMonoidalFunctorsCompose
+  `{PM1   :PreMonoidalCat(C:=C1)(I:=I1)}
+  `{PM2   :PreMonoidalCat(C:=C2)(I:=I2)}
+   {fobj12:C1 -> C2                    }
+   (PMF12 :PreMonoidalFunctor PM1 PM2 fobj12)
+  `{PM3   :PreMonoidalCat(C:=C3)(I:=I3)}
+   {fobj23:C2 -> C3                    }
+   (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23)
+   : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12).
+   admit.
+   Defined.
+
 (*******************************************************************************)
 (* Braided and Symmetric Categories                                            *)
 
 Class BraidedCat `(mc:PreMonoidalCat) :=
 { 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
+; triangleb      : forall a:C,     #(pmon_cancelr a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell a)
+; hexagon1       : forall {a b c}, #(pmon_assoc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc _ _ _)
+                                   ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc _ _ _) >>> b ⋊ #(br_swap _ _)
+; hexagon2       : forall {a b c}, #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc _ _ _)⁻¹
+                                   ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
 }.
 
 Class SymmetricCat `(bc:BraidedCat) :=
 { symcat_swap  :  forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
 }.
+
+
+Section PreMonoidalSubCategory.
+
+  Context `(pm:PreMonoidalCat(I:=pmI)).
+  Context  {Pobj}{Pmor}(S:SubCategory pm Pobj Pmor).
+  Context  (Pobj_unit:Pobj pmI).
+  Context  (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)).
+  Implicit Arguments Pobj_closed [[a][b]].
+  Context  (Pmor_first: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
+                            Pmor _ _ (Pobj_closed pa pc) (Pobj_closed pb pc) (f ⋉ c)).
+  Context  (Pmor_second: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
+                            Pmor _ _ (Pobj_closed pc pa) (Pobj_closed pc pb) (c ⋊ f)).
+  Context  (Pmor_assoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
+                            Pmor _ _
+                            (Pobj_closed (Pobj_closed pa pb) pc)
+                            (Pobj_closed pa (Pobj_closed pb pc))
+                            #(pmon_assoc a c b)).
+  Context  (Pmor_unassoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
+                            Pmor _ _
+                            (Pobj_closed pa (Pobj_closed pb pc))
+                            (Pobj_closed (Pobj_closed pa pb) pc)
+                            #(pmon_assoc a c b)⁻¹).
+  Context  (Pmor_cancell: forall {a}(pa:Pobj a),
+                            Pmor _ _ (Pobj_closed Pobj_unit pa) pa 
+                            #(pmon_cancell a)).
+  Context  (Pmor_uncancell: forall {a}(pa:Pobj a),
+                            Pmor _ _ pa (Pobj_closed Pobj_unit pa)
+                            #(pmon_cancell a)⁻¹).
+  Context  (Pmor_cancelr: forall {a}(pa:Pobj a),
+                            Pmor _ _ (Pobj_closed pa Pobj_unit) pa 
+                            #(pmon_cancelr a)).
+  Context  (Pmor_uncancelr: forall {a}(pa:Pobj a),
+                            Pmor _ _ pa (Pobj_closed pa Pobj_unit)
+                            #(pmon_cancelr a)⁻¹).
+  Implicit Arguments Pmor_first [[a][b][c][f]].
+  Implicit Arguments Pmor_second [[a][b][c][f]].
+
+  Definition PreMonoidalSubCategory_bobj (x y:S) :=
+    existT Pobj _ (Pobj_closed (projT2 x) (projT2 y)).
+
+  Definition PreMonoidalSubCategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
+    (PreMonoidalSubCategory_bobj x a)~~{S}~~>(PreMonoidalSubCategory_bobj y a).
+    unfold hom; simpl; intros.
+    destruct f.
+    destruct a as [a apf].
+    destruct x as [x xpf].
+    destruct y as [y ypf].
+    simpl in *.
+    exists (x0 ⋉ a).
+    apply Pmor_first; auto.
+    Defined.
+
+  Definition PreMonoidalSubCategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
+    (PreMonoidalSubCategory_bobj a x)~~{S}~~>(PreMonoidalSubCategory_bobj a y).
+    unfold hom; simpl; intros.
+    destruct f.
+    destruct a as [a apf].
+    destruct x as [x xpf].
+    destruct y as [y ypf].
+    simpl in *.
+    exists (a ⋊ x0).
+    apply Pmor_second; auto.
+    Defined.
+
+  Instance PreMonoidalSubCategory_first (a:S)
+    : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj x a) :=
+    { fmor := fun x y f => PreMonoidalSubCategory_first_fmor a f }.
+    unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
+    apply (fmor_respects (-⋉x)); auto.
+    unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0;  simpl in *.
+    apply (fmor_preserves_id (-⋉x)); auto.
+    unfold PreMonoidalSubCategory_first_fmor; intros;
+      destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
+    apply (fmor_preserves_comp (-⋉x)); auto.
+    Defined.
+
+  Instance PreMonoidalSubCategory_second (a:S)
+    : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj a x) :=
+    { fmor := fun x y f => PreMonoidalSubCategory_second_fmor a f }.
+    unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
+    apply (fmor_respects (x⋊-)); auto.
+    unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0;  simpl in *.
+    apply (fmor_preserves_id (x⋊-)); auto.
+    unfold PreMonoidalSubCategory_second_fmor; intros;
+      destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
+    apply (fmor_preserves_comp (x⋊-)); auto.
+    Defined.
+
+  Instance PreMonoidalSubCategory_is_Binoidal : BinoidalCat S PreMonoidalSubCategory_bobj :=
+    { bin_first := PreMonoidalSubCategory_first
+    ; bin_second := PreMonoidalSubCategory_second }.
+
+  Definition PreMonoidalSubCategory_assoc
+    : forall a b,
+      (PreMonoidalSubCategory_second a >>>> PreMonoidalSubCategory_first b) <~~~>
+      (PreMonoidalSubCategory_first  b >>>> PreMonoidalSubCategory_second a).
+    admit.
+    Defined.
+
+  Definition PreMonoidalSubCategory_assoc_ll
+    : forall a b,
+      PreMonoidalSubCategory_second (a⊗b) <~~~>
+      PreMonoidalSubCategory_second b >>>> PreMonoidalSubCategory_second a.
+    intros.
+    admit.
+    Defined.
+
+  Definition PreMonoidalSubCategory_assoc_rr
+    : forall a b,
+      PreMonoidalSubCategory_first (a⊗b) <~~~>
+      PreMonoidalSubCategory_first a >>>> PreMonoidalSubCategory_first b.
+    intros.
+    admit.
+    Defined.
+
+  Definition PreMonoidalSubCategory_I := existT _ pmI (Pobj_unit).
+
+  Definition PreMonoidalSubCategory_cancelr : PreMonoidalSubCategory_first PreMonoidalSubCategory_I <~~~> functor_id _.
+    admit.
+    Defined.
+
+  Definition PreMonoidalSubCategory_cancell : PreMonoidalSubCategory_second PreMonoidalSubCategory_I <~~~> functor_id _.
+    admit.
+    Defined.
+
+  Instance PreMonoidalSubCategory_PreMonoidal : PreMonoidalCat PreMonoidalSubCategory_is_Binoidal PreMonoidalSubCategory_I :=
+  { pmon_assoc           := PreMonoidalSubCategory_assoc 
+  ; pmon_assoc_rr        := PreMonoidalSubCategory_assoc_rr
+  ; pmon_assoc_ll        := PreMonoidalSubCategory_assoc_ll
+  ; pmon_cancelr         := PreMonoidalSubCategory_cancelr
+  ; pmon_cancell         := PreMonoidalSubCategory_cancell
+  }.
+  admit.
+  admit.
+  admit.
+  admit.
+  admit.
+  admit.
+  admit.
+  Defined.
+
+End PreMonoidalSubCategory.