major revision: MonoidalCat is now a subclass of PreMonoidalCat

[coq-categories.git] / src / BinoidalCategories.v

diff --git a/src/BinoidalCategories.v b/src/BinoidalCategories.v
index ff08c3d..dddf786 100644 (file)
--- a/src/BinoidalCategories.v
+++ b/src/BinoidalCategories.v
@@ -3,7 +3,6 @@ Require Import Preamble.
 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.
 
 (******************************************************************************)
@@ -36,43 +35,3 @@ Class CommutativeCat `(BinoidalCat) :=
 }.
 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.