X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=src%2FProgrammingLanguage.v;h=0636a6e947a33ffe45a706a890138a9a67a85221;hb=de0467013b4c29f630066c9052c56afa89ebc75b;hp=933785af591887f446bc8a85fd9d556ae7ca4045;hpb=64d416692bda1d36c33b5efa245d46dcf546ad4a;p=coq-hetmet.git

diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v
index 933785a..0636a6e 100644
--- a/src/ProgrammingLanguage.v
+++ b/src/ProgrammingLanguage.v
@@ -34,11 +34,11 @@ Section Programming_Language.
 
   Context {T    : Type}.               (* types of the language *)
 
-  Context (Judg : Type).
-  Context (sequent : Tree ??T -> Tree ??T -> Judg).
+  Definition PLJudg := (Tree ??T) * (Tree ??T).
+  Definition sequent := @pair (Tree ??T) (Tree ??T).
      Notation "cs |= ss" := (sequent cs ss) : pl_scope.
 
-  Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}.
+  Context {Rule : Tree ??PLJudg -> Tree ??PLJudg -> Type}.
 
   Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope.
 
@@ -47,11 +47,11 @@ Section Programming_Language.
   Open Scope pl_scope.
 
   Class ProgrammingLanguage :=
-  { pl_eqv0               :  @ND_Relation Judg Rule
-  ; pl_snd                :> @SequentND Judg Rule _ sequent
-  ; pl_cnd                :> @ContextND Judg Rule T sequent pl_snd
-  ; pl_eqv1               :> @SequentND_Relation Judg Rule _ sequent pl_snd pl_eqv0
-  ; pl_eqv                :> @ContextND_Relation Judg Rule _ sequent pl_snd pl_cnd pl_eqv0 pl_eqv1
+  { pl_eqv0               :  @ND_Relation PLJudg Rule
+  ; pl_snd                :> @SequentND PLJudg Rule _ sequent
+  ; pl_cnd                :> @ContextND PLJudg Rule T sequent pl_snd
+  ; pl_eqv1               :> @SequentND_Relation PLJudg Rule _ sequent pl_snd pl_eqv0
+  ; pl_eqv                :> @ContextND_Relation PLJudg Rule _ sequent pl_snd pl_cnd pl_eqv0 pl_eqv1
   }.
   Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3.
 
@@ -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,39 +171,37 @@ 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 }.
-      intros; unfold eqv; simpl.
-      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 Types_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
+    Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
       { pmon_assoc    := Types_assoc
       ; pmon_cancell  := Types_cancell
       ; pmon_cancelr  := Types_cancelr
       ; pmon_assoc_rr := Types_assoc_rr
       ; pmon_assoc_ll := Types_assoc_ll
       }.
-(*
       apply Build_Pentagon.
         intros; simpl.
         eapply cndr_inert. apply pl_eqv.
@@ -241,54 +239,26 @@ Section Programming_Language.
         auto.
         eapply cndr_inert. apply pl_eqv. auto.
           auto.
-*)
-admit.
-admit.
       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 : Enrichment.
+    Definition TypesEnrichedInJudgments : SurjectiveEnrichment.
       refine
-        {| enr_v_mon := Judgments_Category_monoidal _
-         ; enr_c_pm  := Types_PreMonoidal
-         ; enr_c_bin := Types_binoidal
+        {| senr_c_pm     := TypesL_PreMonoidal
+         ; senr_v        := JudgmentsL
+         ; senr_v_bin    := Judgments_Category_binoidal _
+         ; senr_v_pmon   := Judgments_Category_premonoidal _
+         ; senr_v_mon    := Judgments_Category_monoidal _
+         ; senr_c_bin    := Types_binoidal
+         ; senr_c        := TypesL
         |}.
       Defined.
 
-    Structure HasProductTypes :=
-    {
-    }.
-
-    (*
-    Lemma CartesianEnrMonoidal (e:PreMonoidalEnrichment)
-      `(C:CartesianCat(Ob:= _)(Hom:= _)(C:=Underlying (enr_c e))) : MonoidalEnrichment e.
-      admit.
-      Defined.
-      *)
-
-    (* need to prove that if we have cartesian tuples we have cartesian contexts *)
-    (*
-    Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
-      admit.
-      Defined.
-      *)
   End LanguageCategory.
 
 End Programming_Language.
-(*
-Structure ProgrammingLanguageSMME :=
-{ plsmme_t       : Type
-; plsmme_judg    : Type
-; plsmme_sequent : Tree ??plsmme_t -> Tree ??plsmme_t -> plsmme_judg
-; plsmme_rule    : Tree ??plsmme_judg -> Tree ??plsmme_judg -> Type
-; plsmme_pl      : @ProgrammingLanguage plsmme_t plsmme_judg plsmme_sequent plsmme_rule
-; plsmme_smme    : SurjectiveMonicMonoidalEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl)
-}.
-Coercion plsmme_pl   : ProgrammingLanguageSMME >-> ProgrammingLanguage.
-Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
-*) 
 Implicit Arguments ND [ Judgment ].