- Definition Center_bobj : Center pm -> Center pm -> Center pm.
- apply PreMonoidalSubCategory_bobj.
- intros; auto.
- Defined.
-
- Definition Center_is_Binoidal : BinoidalCat (Center pm) Center_bobj.
- apply PreMonoidalSubCategory_is_Binoidal.
- intros.
- apply first_preserves_centrality; auto.
- intros.
- apply second_preserves_centrality; auto.
+ Definition Center_is_Binoidal : BinoidalCat (Center pm) bin_obj'.
+ apply PreMonoidalWideSubcategory_is_Binoidal.
+ intros; apply first_preserves_centrality; auto.
+ intros; apply second_preserves_centrality; auto.