src/BinoidalCategories.v

   1 Generalizable All Variables.
   2 Require Import Notations.
   3 Require Import Categories_ch1_3.
   4 Require Import Functors_ch1_4.
   5 Require Import Isomorphisms_ch1_5.
   6 Require Import Subcategories_ch7_1.
   7
   8 (******************************************************************************)
   9 (* Binoidal Categories (not in Awodey)                                        *)
  10 (******************************************************************************)
  11
  12 Class BinoidalCat
  13 `( C                  :  Category                               )
  14 ( bin_obj'            :  C -> C -> C                            ) :=
  15 { bin_obj             := bin_obj' where "a ⊗ b" := (bin_obj a b)
  16 ; bin_first           :  forall a:C, Functor C C (fun x => x⊗a)
  17 ; bin_second          :  forall a:C, Functor C C (fun x => a⊗x)
  18 ; bin_c               := C
  19 }.
  20 Coercion bin_c : BinoidalCat >-> Category.
  21 Notation "a ⊗ b"  := (@bin_obj _ _ _ _ _ a b)                              : category_scope.
  22 Notation "C ⋊ f"  := (@fmor _ _ _ _ _ _ _ (@bin_second _ _ _ _ _ C) _ _ f) : category_scope.
  23 Notation "g ⋉ C"  := (@fmor _ _ _ _ _ _ _ (@bin_first _ _ _ _ _ C) _ _ g)  : category_scope.
  24 Notation "C ⋊ -"  := (@bin_second _ _ _ _ _ C)                             : category_scope.
  25 Notation "- ⋉ C"  := (@bin_first _ _ _ _ _ C)                              : category_scope.
  26
  27 Class CentralMorphism `{BinoidalCat}`(f:a~>b) : Prop :=
  28 { centralmor_first  : forall `(g:c~>d), (f ⋉ _ >>> _ ⋊ g) ~~ (_ ⋊ g >>> f ⋉ _)
  29 ; centralmor_second : forall `(g:c~>d), (g ⋉ _ >>> _ ⋊ f) ~~ (_ ⋊ f >>> g ⋉ _)
  30 }.
  31
  32 Class CommutativeCat `(BinoidalCat) :=
  33 { commutative_central  :  forall `(f:a~>b), CentralMorphism f
  34 ; commutative_morprod  := fun `(f:a~>b)`(g:a~>b) => f ⋉ _ >>> _ ⋊ g
  35 }.
  36 Notation "f × g"    := (commutative_morprod f g).
  37