split MonoidalCategories into Binoidal and PreMonoidal

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

diff --git a/src/Enrichment_ch2_8.v b/src/Enrichment_ch2_8.v
index 32a7701..84cc674 100644 (file)
--- a/src/Enrichment_ch2_8.v
+++ b/src/Enrichment_ch2_8.v
@@ -10,6 +10,8 @@ Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
 Require Import Coherence_ch7_8.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
 Require Import MonoidalCategories_ch7_8.
 
 (******************************************************************************)
@@ -374,14 +376,14 @@ Structure Enrichment :=
 Coercion enr_c     : Enrichment >-> ECategory.
 
 (* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
-Structure SurjectiveEnrichment :=
-{ se_enr    :  Enrichment
-; se_decomp :  @treeDecomposition (enr_v se_enr) (option ((enr_c_obj se_enr)*(enr_c_obj se_enr)))
+Structure SurjectiveEnrichment (e:Enrichment) :=
+{ se_enr    := e
+; se_decomp :  @treeDecomposition (enr_v e) (option ((enr_c_obj e)*(enr_c_obj e)))
                   (fun t => match t with
-                            | None   => enr_v_i se_enr
-                            | Some x => match x with pair y z => enr_c_hom se_enr y z end
+                            | None   => enr_v_i e
+                            | Some x => match x with pair y z => enr_c_hom e y z end
                             end)
-                  (fun d1 d2:enr_v se_enr => enr_v_fobj se_enr (pair_obj d1 d2))
+                  (fun d1 d2:enr_v e => enr_v_fobj e (pair_obj d1 d2))
 }.
 Coercion se_enr  : SurjectiveEnrichment >-> Enrichment.