-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)))
- (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
- end)
- (fun d1 d2:enr_v se_enr => enr_v_fobj se_enr (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.