-Structure Enrichment :=
-{ enr_v_ob : Type
-; enr_v_hom : enr_v_ob -> enr_v_ob -> Type
-; enr_v : Category enr_v_ob enr_v_hom
-; enr_v_fobj : prod_obj enr_v enr_v -> enr_v_ob
-; enr_v_f : Functor (enr_v ×× enr_v) enr_v enr_v_fobj
-; enr_v_i : enr_v_ob
-; enr_v_mon : MonoidalCat enr_v enr_v_fobj enr_v_f enr_v_i
-; enr_c_obj : Type
-; enr_c_hom : enr_c_obj -> enr_c_obj -> enr_v
-; enr_c : ECategory enr_v_mon enr_c_obj enr_c_hom
-}.
-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 (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 e
- | Some x => match x with pair y z => enr_c_hom e y z end
- end)
- (fun d1 d2:enr_v e => enr_v_fobj e (pair_obj d1 d2))
+Class EBinoidalCat `(ec:ECategory) :=
+{ ebc_bobj : ec -> ec -> ec
+; ebc_first : forall a:ec, EFunctor ec ec (fun x => ebc_bobj x a)
+; ebc_second : forall a:ec, EFunctor ec ec (fun x => ebc_bobj a x)
+; ebc_ec := ec (* this isn't a coercion - avoids duplicate paths *)