+(*
+ Lemma all_lemma Γ κ σ l :
+(@typeMap (κ :: Γ)
+ (@HaskTApp (κ :: Γ) κ (@weakF Γ κ ★ σ) (@FreshHaskTyVar Γ κ) @@
+ @weakL Γ κ l)) = (@typeMap Γ (@HaskTAll Γ κ σ @@ l)).
+*)
+
+(*
+ Definition flatten : forall Γ Δ ξ τ, Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
+ refine (fix flatten Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') : Expr Γ' (map coMap Δ') (typeMap ○ ξ') (typeMap τ') :=
+ match exp as E in Expr G D X T return Expr G (map coMap D) (typeMap ○ X) (typeMap T) with
+ | EGlobal Γ Δ ξ t wev => EGlobal _ _ _ _ wev
+ | EVar Γ Δ ξ ev => EVar _ _ _ ev
+ | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
+ | EApp Γ Δ ξ t1 t2 lev e1 e2 => EApp _ _ _ _ _ _ (flatten _ _ _ _ e1) (flatten _ _ _ _ e2)
+ | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in _
+ | ELet Γ Δ ξ tv t l ev elet ebody => let case_ELet := tt in _
+ | ELetRec Γ Δ ξ lev t tree branches ebody => let case_ELetRec := tt in _
+ | ECast Γ Δ ξ t1 t2 γ lev e => let case_ECast := tt in _
+ | ENote Γ Δ ξ t n e => ENote _ _ _ _ n (flatten _ _ _ _ e)
+ | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in _
+ | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in _
+ | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => let case_ECoApp := tt in _
+ | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in _
+ | ECase Γ Δ ξ l tc tbranches atypes e alts' => let case_ECase := tt in _
+
+ | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in _
+ | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in _
+ end); clear exp ξ' τ' Γ' Δ'.
+
+ destruct case_ELit.
+ simpl.
+ rewrite lit_lemma.
+ apply ELit.
+
+ destruct case_ELam.
+ set (flatten _ _ _ _ e) as q.
+ rewrite update_typeMap in q.
+ apply (@ELam _ _ _ _ _ _ _ _ v q).
+
+ destruct case_ELet.
+ set (flatten _ _ _ _ ebody) as ebody'.
+ set (flatten _ _ _ _ elet) as elet'.
+ rewrite update_typeMap in ebody'.
+ apply (@ELet _ _ _ _ _ _ _ _ _ elet' ebody').
+
+ destruct case_EEsc.
+ admit.
+ destruct case_EBrak.
+ admit.
+
+ destruct case_ECast.
+ apply flatten in e.
+ eapply ECast in e.
+ apply e.
+ apply flattenCoercion in γ.
+ apply γ.
+
+ destruct case_ETyApp.
+ apply flatten in e.
+ simpl in e.
+ unfold HaskTAll in e.
+ unfold typeMap_ in e.
+ simpl in e.
+ eapply ETyApp in e.
+ rewrite <- foo in e.
+ apply e.
+
+ destruct case_ECoLam.
+ apply flatten in e.
+ simpl in e.
+ set (@ECoLam _ _ _ _ _ _ _ _ _ _ e) as x.
+ simpl in x.
+ simpl.
+ unfold typeMap_.
+ simpl.
+ apply x.
+
+ destruct case_ECoApp.
+ simpl.
+ apply flatten in e.
+ eapply ECoApp.
+ unfold mkHaskCoercionKind in *.
+ simpl in γ.
+ apply flattenCoercion in γ.
+ unfold coMap in γ at 2.
+ apply γ.
+ apply e.
+
+ destruct case_ETyLam.
+ apply flatten in e.
+ set (@ETyLam Unique _ Γ (map coMap Δ) (typeMap ○ ξ) κ (fun ite x => typeMap (σ x ite))) as e'.
+ unfold HaskTAll in *.
+ unfold typeMap_ in *.
+ rewrite <- foo in e'.
+ unfold typeMap in e'.
+ simpl in e'.
+ apply ETyLam.
+
+Set Printing Implicit.
+idtac.
+idtac.
+
+
+ admit.
+
+ destruct case_ECase.
+ admit.
+
+ destruct case_ELetRec.
+ admit.
+ Defined.
+
+ (* This proof will work for any dynamic semantics you like, so
+ * long as those semantics are an ND_Relation (associativity,
+ * neutrality, etc) *)
+ Context (dynamic_semantics : @ND_Relation _ Rule).
+
+ Section SystemFC_Category.
+
+ Context {Γ:TypeEnv}
+ {Δ:CoercionEnv Γ}.
+
+ Definition Context := Tree ??(LeveledHaskType Γ ★).
+
+ Notation "a |= b" := (Γ >> Δ > a |- b).
+
+ (*
+ SystemFCa
+ PCF
+ SystemFCa_two_level
+ SystemFCa_initial_GArrow
+ *)
+
+ Context (nd_eqv:@ND_Relation _ (@URule Γ Δ)).
+ Check (@ProgrammingLanguage).
+ Context (PL:@ProgrammingLanguage (LeveledHaskType Γ ★)
+ (fun x y => match x with x1|=x2 => match y with y1|=y2 => @URule Γ Δ)).
+ Definition JudgmentsFC := @Judgments_Category_CartesianCat _ (@URule Γ Δ) nd_eqv.
+ Definition TypesFC := @TypesL _ (@URule Γ Δ) nd_eqv.
+
+ (* 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).
+
+ Definition JudgmentsFCAtLevel := FullSubcategory JudgmentsFC JudgmentsAtLevel.
+ Definition TypesFCAtLevel := FullSubcategory TypesFC ContextAtLevel.
+ End SingleLevel.
+
+ End SystemFC_Category.
+
+ Implicit Arguments TypesFC [ ].