X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FBinoidalCategories.v;h=774e8eb3edf8c640ed447d1fda647831abc8015c;hp=ff08c3d0dee391705c99c59e585119013095b4de;hb=90844bf411c7cddcd92d48c0b020e5775ace0849;hpb=21607813788d83fb58ce128df442a4ee3edfbdaf

diff --git a/src/BinoidalCategories.v b/src/BinoidalCategories.v
index ff08c3d..774e8eb 100644
--- a/src/BinoidalCategories.v
+++ b/src/BinoidalCategories.v
@@ -1,9 +1,8 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 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.