-(* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
-(*
-Definition SurjectiveEnrichment `(ec:ECategory(Hom:=Vhom)(V:=V)(bin_obj':=Vbobj)(EI:=EI)) :=
- @treeDecomposition _ _
+(* in the paper this is called simply an "enrichment" *)
+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_i : enr_v_ob
+; enr_v_bobj : enr_v -> enr_v -> enr_v
+; enr_v_bin : BinoidalCat enr_v enr_v_bobj
+; enr_v_pmon : PreMonoidalCat enr_v_bin enr_v_i
+; enr_v_mon : MonoidalCat enr_v_pmon
+; 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
+; enr_c_bin : EBinoidalCat enr_c
+; enr_c_i : enr_c
+; enr_c_pm : PreMonoidalCat enr_c_bin enr_c_i
+; enr_c_center := Center enr_c_bin
+; enr_c_center_mon := Center_is_Monoidal enr_c_pm
+}.
+Coercion enr_c : Enrichment >-> ECategory.
+
+(* Coq grinds down into a performance bog when I try to use this *)
+Definition WeaklySurjectiveEnrichment (ec:Enrichment) :=
+ @treeDecomposition (enr_v ec) (option (ec*ec))