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.
9 (******************************************************************************)
10 (* Binoidal Categories (not in Awodey) *)
11 (******************************************************************************)
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)
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.
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 ⋉ _)
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
37 Notation "f × g" := (commutative_morprod f g).
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) ].
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) ].
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
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));
74 [ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
75 | etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
78 End BinoidalCat_from_Bifunctor.