+ (* a premonoidal category enriched in aforementioned full subcategory *)
+ Context (Kehom:(Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host)) -> @ob _ _ VK).
+ Context (KE :@ECategory (@ob _ _ VK) (@hom _ _ VK) VK _ VKM (pmon_I VKM) VKM (Center (TypesL_PreMonoidal Host)) Kehom).
+ Context {kbo :(Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host))}.
+ Context (kbc :@BinoidalCat (Center (TypesL_PreMonoidal Host)) _ (Underlying KE) kbo).