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 Subcategories_ch7_1.
8 (******************************************************************************)
9 (* Binoidal Categories (not in Awodey) *)
10 (******************************************************************************)
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)
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.
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 ⋉ _)
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
36 Notation "f × g" := (commutative_morprod f g).