- (* 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).
+ Context ehom KE (K_bin:@EBinoidalCat _ _ VK _ _ _
+ (PreMonoidalFullSubcategory_PreMonoidal Host_Cartesian VK Pobj_unit Pobj_closed)
+ (TypesL Host) ehom KE (bin_obj(BinoidalCat:=Host_Monoidal))).