X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FEnrichments.v;h=7c24bfa99c7aa4984492cf745e010303f3c12ec2;hp=5fa684e739a2fecd5ab51d3217ecb3ff1d330e6c;hb=e539b49ae3148ab1967b5ea0709734171180b86d;hpb=4e5aa4bcc6024aa7add9c1bf1c2ad9fd2a6a3685

diff --git a/src/Enrichments.v b/src/Enrichments.v
index 5fa684e..7c24bfa 100644
--- a/src/Enrichments.v
+++ b/src/Enrichments.v
@@ -37,7 +37,8 @@ Structure Enrichment :=
 ; 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_bobj       :  enr_c_obj -> enr_c_obj -> enr_c_obj
+; enr_c_bin        :  EBinoidalCat enr_c enr_c_bobj
 ; enr_c_i          :  enr_c
 ; enr_c_pm         :  PreMonoidalCat enr_c_bin enr_c_i
 ; enr_c_center     := Center enr_c_bin
@@ -67,7 +68,8 @@ Structure SurjectiveEnrichment :=
 ; senr_v_pmon     :  PreMonoidalCat senr_v_bin senr_v_i
 ; senr_v_mon      :  MonoidalCat senr_v_pmon
 ; senr_c          :  ECategory senr_v_mon senr_c_obj senr_c_hom
-; senr_c_bin      :  EBinoidalCat senr_c
+; senr_c_bobj     :  senr_c_obj -> senr_c_obj -> senr_c_obj
+; senr_c_bin      :  EBinoidalCat senr_c senr_c_bobj
 ; senr_c_i        :  senr_c
 ; senr_c_pm       :  PreMonoidalCat senr_c_bin senr_c_i
 }.