-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))
-}.
-Coercion se_enr : SurjectiveEnrichment >-> Enrichment.
+
+Instance EBinoidalCat_is_binoidal `(ebc:EBinoidalCat(ec:=ec)) : BinoidalCat (Underlying ec) ebc_bobj.
+ apply Build_BinoidalCat.
+ apply (fun a => UnderlyingFunctor (ebc_first a)).
+ apply (fun a => UnderlyingFunctor (ebc_second a)).
+ Defined.
+
+Coercion EBinoidalCat_is_binoidal : EBinoidalCat >-> BinoidalCat.