src/BinoidalCategories.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 Subcategories_ch7_1.
   8
   9 (******************************************************************************)
  10 (* Binoidal Categories (not in Awodey)                                        *)
  11 (******************************************************************************)
  12
  13 Class BinoidalCat
  14 `( C                  :  Category                               )
  15 ( bin_obj'            :  C -> C -> C                            ) :=
  16 { bin_obj             := bin_obj' where "a ⊗ b" := (bin_obj a b)
  17 ; bin_first           :  forall a:C, Functor C C (fun x => x⊗a)
  18 ; bin_second          :  forall a:C, Functor C C (fun x => a⊗x)
  19 ; bin_c               := C
  20 }.
  21 Coercion bin_c : BinoidalCat >-> Category.
  22 Notation "a ⊗ b"  := (@bin_obj _ _ _ _ _ a b)                              : category_scope.
  23 Notation "C ⋊ f"  := (@fmor _ _ _ _ _ _ _ (@bin_second _ _ _ _ _ C) _ _ f) : category_scope.
  24 Notation "g ⋉ C"  := (@fmor _ _ _ _ _ _ _ (@bin_first _ _ _ _ _ C) _ _ g)  : category_scope.
  25 Notation "C ⋊ -"  := (@bin_second _ _ _ _ _ C)                             : category_scope.
  26 Notation "- ⋉ C"  := (@bin_first _ _ _ _ _ C)                              : category_scope.
  27
  28 Class CentralMorphism `{BinoidalCat}`(f:a~>b) : Prop :=
  29 { centralmor_first  : forall `(g:c~>d), (f ⋉ _ >>> _ ⋊ g) ~~ (_ ⋊ g >>> f ⋉ _)
  30 ; centralmor_second : forall `(g:c~>d), (g ⋉ _ >>> _ ⋊ f) ~~ (_ ⋊ f >>> g ⋉ _)
  31 }.
  32
  33 Class CommutativeCat `(BinoidalCat) :=
  34 { commutative_central  :  forall `(f:a~>b), CentralMorphism f
  35 ; commutative_morprod  := fun `(f:a~>b)`(g:a~>b) => f ⋉ _ >>> _ ⋊ g
  36 }.
  37 Notation "f × g"    := (commutative_morprod f g).
  38
  39 Section BinoidalCat_from_Bifunctor.
  40   Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).
  41   Definition BinoidalCat_from_Bifunctor_first (a:C) : Functor C C (fun b => Fobj (pair_obj b a)).
  42   apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
  43     @fmor _ _ _ _ _ _ _ F (pair_obj a0 a) (pair_obj b a) (pair_mor (pair_obj a0 a) (pair_obj b a) f (id a)))); intros; simpl;
  44     [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
  45     | abstract (set (fmor_preserves_id(F)) as q; apply q)
  46     | abstract (etransitivity;
  47       [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
  48       | set (fmor_respects(F)) as q; apply q ];
  49       split; simpl; auto) ].
  50   Defined.
  51   Definition BinoidalCat_from_Bifunctor_second (a:C) : Functor C C (fun b => Fobj (pair_obj a b)).
  52   apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
  53     @fmor _ _ _ _ _ _ _ F (pair_obj a a0) (pair_obj a b) (pair_mor (pair_obj a a0) (pair_obj a b) (id a) f))); intros;
  54     [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
  55     | abstract (set (fmor_preserves_id(F)) as q; apply q)
  56     | abstract (etransitivity;
  57       [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
  58       | set (fmor_respects(F)) as q; apply q ];
  59       split; simpl; auto) ].
  60   Defined.
  61
  62   Definition BinoidalCat_from_Bifunctor : BinoidalCat C (fun a b => Fobj (pair_obj a b)).
  63    refine {| bin_first  := BinoidalCat_from_Bifunctor_first
  64            ; bin_second := BinoidalCat_from_Bifunctor_second
  65           |}.
  66    Defined.
  67
  68   Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat BinoidalCat_from_Bifunctor.
  69   abstract (intros; apply Build_CommutativeCat; intros; apply Build_CentralMorphism; intros; simpl; (
  70     etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ]; symmetry;
  71     etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ];
  72     apply (fmor_respects(F));
  73     split;
  74       [ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
  75       | etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
  76   Defined.
  77
  78 End BinoidalCat_from_Bifunctor.