- Context (encodeTypeTree_reduce : @LeveledHaskType V -> @LeveledHaskType V -> @LeveledHaskType V).
- Context (encodeTypeTree_empty : @LeveledHaskType V).
- Context (encodeTypeTree_flat_empty : @CoreType V).
- Context (encodeTypeTree_flat_reduce : @CoreType V -> @CoreType V -> @CoreType V).
-
- Definition encodeTypeTree :=
- @treeReduce _ _ (fun x => match x with None => encodeTypeTree_empty | Some q => q end) encodeTypeTree_reduce.
- Definition encodeTypeTree_flat :=
- @treeReduce _ _ (fun x => match x with None => encodeTypeTree_flat_empty | Some q => q end) encodeTypeTree_flat_reduce.
- (* the full category of judgments *)
- Definition ob2judgment past :=
- fun q:Tree ??(@LeveledHaskType V) * Tree ??(@LeveledHaskType V) =>
- let (a,s):=q in (Γ > past : a |- (encodeTypeTree s) ).
- Definition SystemFC_Cat past :=
- @Judgments_Category_monoidal _ Rule
- (@ml_dynamic_semantics V)
- (Tree ??(@LeveledHaskType V) * Tree ??(@LeveledHaskType V))
- (ob2judgment past).
+
+ Context {Γ:TypeEnv}
+ {Δ:CoercionEnv Γ}.
+
+ Definition Context := Tree ??(LeveledHaskType Γ ★).
+
+ Notation "a |= b" := (Γ >> Δ > a |- b).
+
+ (* category of judgments in a fixed type/coercion context *)
+ Definition JudgmentsFC :=
+ @Judgments_Category_monoidal _ Rule dynamic_semantics (UJudg Γ Δ) UJudg2judg.
+
+ Definition identityProof t : [] ~~{JudgmentsFC}~~> [t |= t].
+ unfold hom; simpl.
+ admit.
+ Defined.
+
+ Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsFC}~~> [a |= c].
+ unfold hom; simpl.
+ admit.
+ Defined.
+
+ Definition TypesFC : ECategory JudgmentsFC Context (fun x y => [Γ >> Δ > x |- y]).
+ refine
+ {| eid := identityProof
+ ; ecomp := cutProof
+ |}; intros.
+ apply MonoidalCat_all_central.
+ apply MonoidalCat_all_central.
+ admit.
+ admit.
+ admit.
+ Defined.
+
+ Definition TypesEnrichedInJudgments : Enrichment.
+ refine {| enr_c := TypesFC |}.
+ Defined.
+
+(*
+ Definition TwoLevelLanguage L2 :=
+ { L1 : _ &
+ Reification (TypesEnrichedInJudgments L1) (TypesEnrichedInJudgments L2) }
+
+ Inductive NLevelLanguage : nat -> Language -> Type :=
+ | NLevelLanguage_zero : forall lang, NLevelLanguage O lang
+ | NLevelLanguage_succ : forall L1 L2 n, TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2
+
+ Definition OmegaLevelLanguage : Language -> Type :=
+ forall n:nat, NLevelLanguage n L.
+*)
+
+
+ (* The full subcategory of SystemFC(Γ,Δ) consisting only of judgments involving types at a fixed level. Note that
+ * code types are still permitted! *)
+ Section SingleLevel.
+ Context (lev:HaskLevel Γ).
+
+ Inductive ContextAtLevel : Context -> Prop :=
+ | contextAtLevel_nil : ContextAtLevel []
+ | contextAtLevel_leaf : forall τ, ContextAtLevel [τ @@ lev]
+ | contextAtLevel_branch : forall b1 b2, ContextAtLevel b1 -> ContextAtLevel b2 -> ContextAtLevel (b1,,b2).
+
+ Inductive JudgmentsAtLevel : JudgmentsFC -> Prop :=
+ | judgmentsAtLevel_nil : JudgmentsAtLevel []
+ | judgmentsAtLevel_leaf : forall c1 c2, ContextAtLevel c1 -> ContextAtLevel c2 -> JudgmentsAtLevel [c1 |= c2]
+ | judgmentsAtLevel_branch : forall j1 j2, JudgmentsAtLevel j1 -> JudgmentsAtLevel j2 -> JudgmentsAtLevel (j1,,j2).