X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FProgrammingLanguage.v;h=0636a6e947a33ffe45a706a890138a9a67a85221;hp=e29903a4524935a6f1d2f88460878e90a4f687a0;hb=e539b49ae3148ab1967b5ea0709734171180b86d;hpb=4e5aa4bcc6024aa7add9c1bf1c2ad9fd2a6a3685

diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v
index e29903a..0636a6e 100644
--- a/src/ProgrammingLanguage.v
+++ b/src/ProgrammingLanguage.v
@@ -116,7 +116,7 @@ Section Programming_Language.
       simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
       Defined.
 
-    Definition Types_binoidal : EBinoidalCat TypesL.
+    Definition Types_binoidal : EBinoidalCat TypesL (@T_Branch _).
       refine
         {| ebc_first  := Types_first
          ; ebc_second := Types_second
@@ -171,28 +171,28 @@ Section Programming_Language.
 
     Instance Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a :=
       { ni_iso := fun c => Types_assoc_iso a c b }.
-      admit.
+      admit.   (* need to add this as an obligation in ProgrammingLanguage class *)
       Defined.
 
     Instance Types_cancelr   : Types_first [] <~~~> functor_id _ :=
       { ni_iso := Types_cancelr_iso }.
       intros; simpl.
-      admit.
+      admit.   (* need to add this as an obligation in ProgrammingLanguage class *)
       Defined.
 
     Instance Types_cancell   : Types_second [] <~~~> functor_id _ :=
       { ni_iso := Types_cancell_iso }.
-      admit.
+      admit.   (* need to add this as an obligation in ProgrammingLanguage class *)
       Defined.
 
     Instance Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a :=
       { ni_iso := fun c => Types_assoc_iso a b c }.
-      admit.
+      admit.   (* need to add this as an obligation in ProgrammingLanguage class *)
       Defined.
 
     Instance Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b :=
       { ni_iso := fun c => iso_inv _ _ (Types_assoc_iso c a b) }.
-      admit.
+      admit.   (* need to add this as an obligation in ProgrammingLanguage class *)
       Defined.
 
     Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
@@ -241,9 +241,9 @@ Section Programming_Language.
           auto.
       intros; simpl; reflexivity.
       intros; simpl; reflexivity.
-      admit.  (* assoc   central *)
-      admit.  (* cancelr central *)
-      admit.  (* cancell central *)
+      admit.  (* assoc   is central: need to add this as an obligation in ProgrammingLanguage class *)
+      admit.  (* cancelr is central: need to add this as an obligation in ProgrammingLanguage class *)
+      admit.  (* cancell is central: need to add this as an obligation in ProgrammingLanguage class *)
       Defined.
 
     Definition TypesEnrichedInJudgments : SurjectiveEnrichment.