src/PreMonoidalCategories.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 InitialTerminal_ch2_2.
   7 Require Import Subcategories_ch7_1.
   8 Require Import NaturalTransformations_ch7_4.
   9 Require Import NaturalIsomorphisms_ch7_5.
  10 Require Import Coherence_ch7_8.
  11 Require Import BinoidalCategories.
  12
  13 (* not in Awodey *)
  14 Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
  15 { pmon_I               := I
  16 ; pmon_bin             := bc
  17 ; pmon_cat             := C
  18 ; pmon_assoc           : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
  19 ; pmon_cancelr         :                               (bin_first I) <~~~> functor_id C
  20 ; pmon_cancell         :                              (bin_second I) <~~~> functor_id C
  21 ; 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))
  22 ; 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))
  23                                   (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
  24 ; pmon_assoc_rr        :  forall a b, (bin_first  (a⊗b)) <~~~> (bin_first  a >>>> bin_first  b)
  25 ; pmon_assoc_ll        :  forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
  26 ; pmon_coherent_r      :  forall a c d:C,  #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
  27 ; pmon_coherent_l      :  forall a c d:C,  #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
  28 ; pmon_assoc_central   :  forall a b c, CentralMorphism #(pmon_assoc   a b c)
  29 ; pmon_cancelr_central :  forall a    , CentralMorphism #(pmon_cancelr a)
  30 ; pmon_cancell_central :  forall a    , CentralMorphism #(pmon_cancell a)
  31 }.
  32 (*
  33  * Premonoidal categories actually have three associators (the "f"
  34  * indicates the position in which the operation is natural:
  35  *
  36  *  assoc    : (A ⋊ f) ⋉ C <->  A ⋊ (f ⋉  C)
  37  *  assoc_rr : (f ⋉ B) ⋉ C <->  f ⋉ (B  ⊗ C)
  38  *  assoc_ll : (A ⋊ B) ⋊ f <-> (A ⊗  B) ⋊ f
  39  *
  40  * Fortunately, in a monoidal category these are all the same natural
  41  * isomorphism (and in any case -- monoidal or not -- the objects in
  42  * the left column are all the same and the objects in the right
  43  * column are all the same).  This formalization assumes that is the
  44  * case even for premonoidal categories with non-central maps, in
  45  * order to keep the complexity manageable.  I don't know much about
  46  * the consequences of having them and letting them be different; you
  47  * might need extra versions of the triangle/pentagon diagrams.
  48  *)
  49
  50 Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
  51 Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
  52 Implicit Arguments pmon_assoc   [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
  53 Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
  54
  55 (* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
  56 Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b
  57   : #(pmon_cancelr (a ⊗ b)) ~~ #((pmon_assoc a EI) b) >>> (a ⋊-) \ #(pmon_cancelr b).
  58   set (pmon_pentagon EI EI a b) as penta. unfold pmon_pentagon in penta.
  59   set (pmon_triangle a b) as tria. unfold pmon_triangle in tria.
  60   apply (fmor_respects(bin_second EI)) in tria.
  61   set (@fmor_preserves_comp) as fpc.
  62   setoid_rewrite <- fpc in tria.
  63   set (ni_commutes (pmon_assoc a b)) as xx.
  64   (* FIXME *)
  65   Admitted.
  66
  67 Class PreMonoidalFunctor
  68 `(PM1:PreMonoidalCat(C:=C1)(I:=I1))
  69 `(PM2:PreMonoidalCat(C:=C2)(I:=I2))
  70  (fobj : C1 -> C2          ) :=
  71 { mf_F          :> Functor C1 C2 fobj
  72 ; mf_i          :  I2 ≅ mf_F I1
  73 ; mf_first      :  ∀ a,              mf_F >>>> bin_first  (mf_F a)  <~~~>  bin_first  a >>>> mf_F
  74 ; mf_second     :  ∀ a,              mf_F >>>> bin_second (mf_F a)  <~~~>  bin_second a >>>> mf_F
  75 ; mf_consistent :  ∀ a b,            #(mf_first a b) ~~ #(mf_second b a)
  76 ; mf_center     :  forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
  77 ; mf_cancell    :  ∀ b,     #(pmon_cancell _) ~~ #mf_i ⋉ _ >>> #(mf_first  b I1) >>> mf_F \ #(pmon_cancell b)
  78 ; mf_cancelr    :  ∀ a,     #(pmon_cancelr _) ~~ _ ⋊ #mf_i >>> #(mf_second a I1) >>> mf_F \ #(pmon_cancelr a)
  79 ; mf_assoc      :  ∀ a b c, #(pmon_assoc _ _ _)  >>> _ ⋊ #(mf_second _ _) >>>        #(mf_second _ _) ~~
  80                             #(mf_second _ _) ⋉ _ >>>     #(mf_second _ _) >>> mf_F \ #(pmon_assoc a c b)
  81 }.
  82 Coercion mf_F : PreMonoidalFunctor >-> Functor.
  83
  84 Definition PreMonoidalFunctorsCompose
  85   `{PM1   :PreMonoidalCat(C:=C1)(I:=I1)}
  86   `{PM2   :PreMonoidalCat(C:=C2)(I:=I2)}
  87    {fobj12:C1 -> C2                    }
  88    (PMF12 :PreMonoidalFunctor PM1 PM2 fobj12)
  89   `{PM3   :PreMonoidalCat(C:=C3)(I:=I3)}
  90    {fobj23:C2 -> C3                    }
  91    (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23)
  92    : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12).
  93    admit.
  94    Defined.
  95
  96 (*******************************************************************************)
  97 (* Braided and Symmetric Categories                                            *)
  98
  99 Class BraidedCat `(mc:PreMonoidalCat) :=
 100 { br_niso        : forall a, bin_first a <~~~> bin_second a
 101 ; br_swap        := fun a b => ni_iso (br_niso b) a
 102 ; triangleb      : forall a:C,     #(pmon_cancelr a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell a)
 103 ; hexagon1       : forall {a b c}, #(pmon_assoc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc _ _ _)
 104                                    ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc _ _ _) >>> b ⋊ #(br_swap _ _)
 105 ; hexagon2       : forall {a b c}, #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc _ _ _)⁻¹
 106                                    ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
 107 }.
 108
 109 Class SymmetricCat `(bc:BraidedCat) :=
 110 { symcat_swap  :  forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
 111 }.
 112
 113
 114 Section PreMonoidalSubCategory.
 115
 116   Context `(pm:PreMonoidalCat(I:=pmI)).
 117   Context  {Pobj}{Pmor}(S:SubCategory pm Pobj Pmor).
 118   Context  (Pobj_unit:Pobj pmI).
 119   Context  (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)).
 120   Implicit Arguments Pobj_closed [[a][b]].
 121   Context  (Pmor_first: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
 122                             Pmor _ _ (Pobj_closed pa pc) (Pobj_closed pb pc) (f ⋉ c)).
 123   Context  (Pmor_second: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
 124                             Pmor _ _ (Pobj_closed pc pa) (Pobj_closed pc pb) (c ⋊ f)).
 125   Context  (Pmor_assoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
 126                             Pmor _ _
 127                             (Pobj_closed (Pobj_closed pa pb) pc)
 128                             (Pobj_closed pa (Pobj_closed pb pc))
 129                             #(pmon_assoc a c b)).
 130   Context  (Pmor_unassoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
 131                             Pmor _ _
 132                             (Pobj_closed pa (Pobj_closed pb pc))
 133                             (Pobj_closed (Pobj_closed pa pb) pc)
 134                             #(pmon_assoc a c b)⁻¹).
 135   Context  (Pmor_cancell: forall {a}(pa:Pobj a),
 136                             Pmor _ _ (Pobj_closed Pobj_unit pa) pa
 137                             #(pmon_cancell a)).
 138   Context  (Pmor_uncancell: forall {a}(pa:Pobj a),
 139                             Pmor _ _ pa (Pobj_closed Pobj_unit pa)
 140                             #(pmon_cancell a)⁻¹).
 141   Context  (Pmor_cancelr: forall {a}(pa:Pobj a),
 142                             Pmor _ _ (Pobj_closed pa Pobj_unit) pa
 143                             #(pmon_cancelr a)).
 144   Context  (Pmor_uncancelr: forall {a}(pa:Pobj a),
 145                             Pmor _ _ pa (Pobj_closed pa Pobj_unit)
 146                             #(pmon_cancelr a)⁻¹).
 147   Implicit Arguments Pmor_first [[a][b][c][f]].
 148   Implicit Arguments Pmor_second [[a][b][c][f]].
 149
 150   Definition PreMonoidalSubCategory_bobj (x y:S) :=
 151     existT Pobj _ (Pobj_closed (projT2 x) (projT2 y)).
 152
 153   Definition PreMonoidalSubCategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
 154     (PreMonoidalSubCategory_bobj x a)~~{S}~~>(PreMonoidalSubCategory_bobj y a).
 155     unfold hom; simpl; intros.
 156     destruct f.
 157     destruct a as [a apf].
 158     destruct x as [x xpf].
 159     destruct y as [y ypf].
 160     simpl in *.
 161     exists (x0 ⋉ a).
 162     apply Pmor_first; auto.
 163     Defined.
 164
 165   Definition PreMonoidalSubCategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
 166     (PreMonoidalSubCategory_bobj a x)~~{S}~~>(PreMonoidalSubCategory_bobj a y).
 167     unfold hom; simpl; intros.
 168     destruct f.
 169     destruct a as [a apf].
 170     destruct x as [x xpf].
 171     destruct y as [y ypf].
 172     simpl in *.
 173     exists (a ⋊ x0).
 174     apply Pmor_second; auto.
 175     Defined.
 176
 177   Instance PreMonoidalSubCategory_first (a:S)
 178     : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj x a) :=
 179     { fmor := fun x y f => PreMonoidalSubCategory_first_fmor a f }.
 180     unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
 181     apply (fmor_respects (-⋉x)); auto.
 182     unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0;  simpl in *.
 183     apply (fmor_preserves_id (-⋉x)); auto.
 184     unfold PreMonoidalSubCategory_first_fmor; intros;
 185       destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
 186     apply (fmor_preserves_comp (-⋉x)); auto.
 187     Defined.
 188
 189   Instance PreMonoidalSubCategory_second (a:S)
 190     : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj a x) :=
 191     { fmor := fun x y f => PreMonoidalSubCategory_second_fmor a f }.
 192     unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
 193     apply (fmor_respects (x⋊-)); auto.
 194     unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0;  simpl in *.
 195     apply (fmor_preserves_id (x⋊-)); auto.
 196     unfold PreMonoidalSubCategory_second_fmor; intros;
 197       destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
 198     apply (fmor_preserves_comp (x⋊-)); auto.
 199     Defined.
 200
 201   Instance PreMonoidalSubCategory_is_Binoidal : BinoidalCat S PreMonoidalSubCategory_bobj :=
 202     { bin_first := PreMonoidalSubCategory_first
 203     ; bin_second := PreMonoidalSubCategory_second }.
 204
 205   Definition PreMonoidalSubCategory_assoc
 206     : forall a b,
 207       (PreMonoidalSubCategory_second a >>>> PreMonoidalSubCategory_first b) <~~~>
 208       (PreMonoidalSubCategory_first  b >>>> PreMonoidalSubCategory_second a).
 209     admit.
 210     Defined.
 211
 212   Definition PreMonoidalSubCategory_assoc_ll
 213     : forall a b,
 214       PreMonoidalSubCategory_second (a⊗b) <~~~>
 215       PreMonoidalSubCategory_second b >>>> PreMonoidalSubCategory_second a.
 216     intros.
 217     admit.
 218     Defined.
 219
 220   Definition PreMonoidalSubCategory_assoc_rr
 221     : forall a b,
 222       PreMonoidalSubCategory_first (a⊗b) <~~~>
 223       PreMonoidalSubCategory_first a >>>> PreMonoidalSubCategory_first b.
 224     intros.
 225     admit.
 226     Defined.
 227
 228   Definition PreMonoidalSubCategory_I := existT _ pmI (Pobj_unit).
 229
 230   Definition PreMonoidalSubCategory_cancelr : PreMonoidalSubCategory_first PreMonoidalSubCategory_I <~~~> functor_id _.
 231     admit.
 232     Defined.
 233
 234   Definition PreMonoidalSubCategory_cancell : PreMonoidalSubCategory_second PreMonoidalSubCategory_I <~~~> functor_id _.
 235     admit.
 236     Defined.
 237
 238   Instance PreMonoidalSubCategory_PreMonoidal : PreMonoidalCat PreMonoidalSubCategory_is_Binoidal PreMonoidalSubCategory_I :=
 239   { pmon_assoc           := PreMonoidalSubCategory_assoc
 240   ; pmon_assoc_rr        := PreMonoidalSubCategory_assoc_rr
 241   ; pmon_assoc_ll        := PreMonoidalSubCategory_assoc_ll
 242   ; pmon_cancelr         := PreMonoidalSubCategory_cancelr
 243   ; pmon_cancell         := PreMonoidalSubCategory_cancell
 244   }.
 245   admit.
 246   admit.
 247   admit.
 248   admit.
 249   admit.
 250   admit.
 251   admit.
 252   Defined.
 253
 254 End PreMonoidalSubCategory.