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 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 Require Import BinoidalCategories.
  13
  14 (* not in Awodey *)
  15 Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
  16 { pmon_I          := I
  17 ; pmon_bin        := bc
  18 ; pmon_cat        := C
  19 ; pmon_assoc      : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
  20 ; pmon_cancelr    :                               (bin_first I) <~~~> functor_id C
  21 ; pmon_cancell    :                              (bin_second I) <~~~> functor_id C
  22 ; 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))
  23 ; 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))
  24                              (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
  25 ; pmon_assoc_rr   :  forall a b, (bin_first  (a⊗b)) <~~~> (bin_first  a >>>> bin_first  b)
  26 ; pmon_assoc_ll   :  forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
  27 ; pmon_coherent_r :  forall a c d:C,  #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
  28 ; pmon_coherent_l :  forall a c d:C,  #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
  29 }.
  30 (*
  31  * Premonoidal categories actually have three associators (the "f"
  32  * indicates the position in which the operation is natural:
  33  *
  34  *  assoc    : (A ⋊ f) ⋉ C <->  A ⋊ (f ⋉  C)
  35  *  assoc_rr : (f ⋉ B) ⋉ C <->  f ⋉ (B  ⊗ C)
  36  *  assoc_ll : (A ⋊ B) ⋊ f <-> (A ⊗  B) ⋊ f
  37  *
  38  * Fortunately, in a monoidal category these are all the same natural
  39  * isomorphism (and in any case -- monoidal or not -- the objects in
  40  * the left column are all the same and the objects in the right
  41  * column are all the same).  This formalization assumes that is the
  42  * case even for premonoidal categories with non-central maps, in
  43  * order to keep the complexity manageable.  I don't know much about
  44  * the consequences of having them and letting them be different; you
  45  * might need extra versions of the triangle/pentagon diagrams.
  46  *)
  47
  48 Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I ].
  49 Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I ].
  50 Implicit Arguments pmon_assoc   [ Ob Hom C bin_obj' bc I ].
  51 Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
  52
  53 (* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
  54 Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b
  55   : #((pmon_cancelr mn) (a ⊗ b)) ~~ #((pmon_assoc mn a EI) b) >>> (a ⋊-) \ #((pmon_cancelr mn) b).
  56   set (pmon_pentagon EI EI a b) as penta. unfold pmon_pentagon in penta.
  57   set (pmon_triangle a b) as tria. unfold pmon_triangle in tria.
  58   apply (fmor_respects(bin_second EI)) in tria.
  59   set (@fmor_preserves_comp) as fpc.
  60   setoid_rewrite <- fpc in tria.
  61   set (ni_commutes (pmon_assoc mn a b)) as xx.
  62   (* FIXME *)
  63   Admitted.
  64
  65 Class PreMonoidalFunctor
  66 `(PM1:PreMonoidalCat(C:=C1)(I:=I1))
  67 `(PM2:PreMonoidalCat(C:=C2)(I:=I2))
  68  (fobj : C1 -> C2          ) :=
  69 { mf_F                :> Functor C1 C2 fobj
  70 ; mf_preserves_i      :  mf_F I1 ≅ I2
  71 ; mf_preserves_first  :  forall a,   bin_first a >>>> mf_F  <~~~>  mf_F >>>> bin_first  (mf_F a)
  72 ; mf_preserves_second :  forall a,  bin_second a >>>> mf_F  <~~~>  mf_F >>>> bin_second (mf_F a)
  73 ; mf_preserves_center :  forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
  74 }.
  75 Coercion mf_F : PreMonoidalFunctor >-> Functor.
  76
  77 (*******************************************************************************)
  78 (* Braided and Symmetric Categories                                            *)
  79
  80 Class BraidedCat `(mc:PreMonoidalCat) :=
  81 { br_niso        : forall a, bin_first a <~~~> bin_second a
  82 ; br_swap        := fun a b => ni_iso (br_niso b) a
  83 ; triangleb      : forall a:C,     #(pmon_cancelr mc a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell mc a)
  84 ; hexagon1       : forall {a b c}, #(pmon_assoc mc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc mc _ _ _)
  85                                    ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc mc _ _ _) >>> b ⋊ #(br_swap _ _)
  86 ; hexagon2       : forall {a b c}, #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc mc _ _ _)⁻¹
  87                                    ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
  88 }.
  89
  90 Class SymmetricCat `(bc:BraidedCat) :=
  91 { symcat_swap  :  forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
  92 }.