+Require Import ProgrammingLanguageCategory.
+Require Import Enrichments.
+
+Section ProgrammingLanguageReification.
+
+ Definition TwoLevelLanguage `(Guest:ProgrammingLanguage) `(Host:ProgrammingLanguage)
+ := Reification (TypesEnrichedInJudgments Guest) (TypesEnrichedInJudgments Host) [].
+
+ Inductive NLevelLanguage : forall (n:nat) `(PL:ProgrammingLanguage), Type :=
+ | NLevelLanguage_zero : forall `(lang:ProgrammingLanguage),
+ NLevelLanguage O lang
+ | NLevelLanguage_succ : forall `(L1:ProgrammingLanguage) `(L2:ProgrammingLanguage) n,
+ TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
+
+ (*
+ Definition OmegaLevelLanguage : Type :=
+ { f : nat -> ProgrammingLanguage
+ & forall n, TwoLevelLanguage (f n) (f (S n)) }.
+ *)
+
+End ProgrammingLanguageReification.