X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FProgrammingLanguageReification.v;h=f6a2a8e5d3eb32773336444c99a80d89a7c17063;hp=589f7486749ae860b3ec0d2891187add896b2607;hb=ff46afb5b5a682dd9f2e246afb889bb2f1be9f15;hpb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f

diff --git a/src/ProgrammingLanguageReification.v b/src/ProgrammingLanguageReification.v
index 589f748..f6a2a8e 100644
--- a/src/ProgrammingLanguageReification.v
+++ b/src/ProgrammingLanguageReification.v
@@ -29,6 +29,28 @@ Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 Require Import ProgrammingLanguage.
 
+(*
+  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    : SurjectiveEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl)
+  }.
+  Coercion plsmme_pl   : ProgrammingLanguageSMME >-> ProgrammingLanguage.
+  Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
+*)
+
+  Context
+  `(Guest        : ProgrammingLanguage)
+  `(Host         : ProgrammingLanguage)
+   (HostMonoidal : MonoidalEnrichment (TypesEnrichedInJudgments Host))
+   (HostMonic    : MonicEnrichment    (TypesEnrichedInJudgments Host)).
+
+Definition TwoLevelLanguage (Guest Host:ProgrammingLanguageSMME)
+  := Reification Guest Host (me_i Host).
+
 Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
 | NLevelLanguage_zero : forall lang,    NLevelLanguage O lang
 | NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n,
@@ -37,3 +59,4 @@ Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
 Definition OmegaLevelLanguage : Type :=
   { f : nat -> ProgrammingLanguageSMME
   & forall n, TwoLevelLanguage (f n) (f (S n)) }.
+