Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
Require Import Subcategories_ch7_1.
(******************************************************************************)
}.
Notation "f × g" := (commutative_morprod f g).
-Section BinoidalCat_from_Bifunctor.
- Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).
- Definition BinoidalCat_from_Bifunctor_first (a:C) : Functor C C (fun b => Fobj (pair_obj b a)).
- apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
- @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;
- [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
- | abstract (set (fmor_preserves_id(F)) as q; apply q)
- | abstract (etransitivity;
- [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
- | set (fmor_respects(F)) as q; apply q ];
- split; simpl; auto) ].
- Defined.
- Definition BinoidalCat_from_Bifunctor_second (a:C) : Functor C C (fun b => Fobj (pair_obj a b)).
- apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
- @fmor _ _ _ _ _ _ _ F (pair_obj a a0) (pair_obj a b) (pair_mor (pair_obj a a0) (pair_obj a b) (id a) f))); intros;
- [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
- | abstract (set (fmor_preserves_id(F)) as q; apply q)
- | abstract (etransitivity;
- [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
- | set (fmor_respects(F)) as q; apply q ];
- split; simpl; auto) ].
- Defined.
-
- Definition BinoidalCat_from_Bifunctor : BinoidalCat C (fun a b => Fobj (pair_obj a b)).
- refine {| bin_first := BinoidalCat_from_Bifunctor_first
- ; bin_second := BinoidalCat_from_Bifunctor_second
- |}.
- Defined.
-
- Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat BinoidalCat_from_Bifunctor.
- abstract (intros; apply Build_CommutativeCat; intros; apply Build_CentralMorphism; intros; simpl; (
- etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ]; symmetry;
- etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ];
- apply (fmor_respects(F));
- split;
- [ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
- | etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
- Defined.
-
-End BinoidalCat_from_Bifunctor.