unbreak lots more stuff

diff --git a/src/All.v b/src/All.v
index 25fa85d..d4956dd 100644 (file)
--- a/src/All.v
+++ b/src/All.v
@@ -1,7 +1,6 @@
 Require Import ExtractionMain.
-Require Import ProgrammingLanguageGeneralizedArrow.
-Require Import ProgrammingLanguageFlattening.
 Require Import ProgrammingLanguageArrow.
 Require Import ProgrammingLanguageReification.
+Require Import ProgrammingLanguageFlattening.
 Require Import ReificationsIsomorphicToGeneralizedArrows.
 

diff --git a/src/Enrichments.v b/src/Enrichments.v
index 5fa684e..7c24bfa 100644 (file)
--- a/src/Enrichments.v
+++ b/src/Enrichments.v
@@ -37,7 +37,8 @@ Structure Enrichment :=
 ; enr_c_obj        :  Type
 ; enr_c_hom        :  enr_c_obj -> enr_c_obj -> enr_v
 ; enr_c            :  ECategory enr_v_mon enr_c_obj enr_c_hom
-; enr_c_bin        :  EBinoidalCat enr_c
+; enr_c_bobj       :  enr_c_obj -> enr_c_obj -> enr_c_obj
+; enr_c_bin        :  EBinoidalCat enr_c enr_c_bobj
 ; enr_c_i          :  enr_c
 ; enr_c_pm         :  PreMonoidalCat enr_c_bin enr_c_i
 ; enr_c_center     := Center enr_c_bin
@@ -67,7 +68,8 @@ Structure SurjectiveEnrichment :=
 ; senr_v_pmon     :  PreMonoidalCat senr_v_bin senr_v_i
 ; senr_v_mon      :  MonoidalCat senr_v_pmon
 ; senr_c          :  ECategory senr_v_mon senr_c_obj senr_c_hom
-; senr_c_bin      :  EBinoidalCat senr_c
+; senr_c_bobj     :  senr_c_obj -> senr_c_obj -> senr_c_obj
+; senr_c_bin      :  EBinoidalCat senr_c senr_c_bobj
 ; senr_c_i        :  senr_c
 ; senr_c_pm       :  PreMonoidalCat senr_c_bin senr_c_i
 }.

diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v
index 303baef..f246cbe 100644 (file)
--- a/src/GeneralizedArrow.v
+++ b/src/GeneralizedArrow.v
@@ -26,24 +26,19 @@ Require Import PreMonoidalCenter.
 Require Import PreMonoidalCategories.
 Require Import BinoidalCategories.
 
-Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) :=
-{ ga_functor_obj      : enr_v K -> ce
-; ga_functor          : Functor            (enr_v_mon K) (enr_c_pm ce) ga_functor_obj
-; ga_functor_monoidal : PreMonoidalFunctor (enr_v_mon K) (enr_c_pm ce) ga_functor
+Class GeneralizedArrow (K:Enrichment)(C:Enrichment) :=
+{ ga_functor_obj      : enr_v K -> C
+; ga_functor          : Functor            (enr_v_mon K) (enr_c_pm C) ga_functor_obj
+; ga_functor_monoidal : PreMonoidalFunctor (enr_v_mon K) (enr_c_pm C) ga_functor
 
 (* We require that the host language (but NOT the guest language) be pure, i.e. all morphisms central, to simplify
  * things.  If this doesn't suit you, just consider the "host language" here to be the pure sublanguage of the
  * host language, and toss on the inclusion functor to the full language *)
-; ga_host_lang_pure   : CommutativeCat (enr_c_pm ce)
-
-(*
-; ga_functor          : Functor         (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor_obj
-; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor
-*)
+; ga_host_lang_pure   : CommutativeCat (enr_c_pm C)
 }.
 Coercion ga_functor_monoidal : GeneralizedArrow >-> PreMonoidalFunctor.
 
-Implicit Arguments GeneralizedArrow    [ [ce] ].
-Implicit Arguments ga_functor_obj      [ K ce C ].
-Implicit Arguments ga_functor          [ K ce C ].
-Implicit Arguments ga_functor_monoidal [ K ce C ].
+Implicit Arguments GeneralizedArrow    [ ].
+Implicit Arguments ga_functor_obj      [ K C ].
+Implicit Arguments ga_functor          [ K C ].
+Implicit Arguments ga_functor_monoidal [ K C ].

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index 9ff0d4d..b5e3147 100644 (file)
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -916,7 +916,7 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0]
     apply (fmor_respects (-⋉ F b)).
     apply iso_comp2.
     Qed.
-*)
+
   Lemma cancell_coherent (b:enr_v K) :
    #(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
    (#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>>
@@ -1162,7 +1162,7 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0]
     apply assoc_coherent.
     Defined.
 
-  Definition garrow_from_reification : GeneralizedArrow K CM :=
+  Definition garrow_from_reification : GeneralizedArrow K C :=
     {| ga_functor_monoidal := garrow_monoidal
      ; ga_host_lang_pure   := reification_host_lang_pure _ _ _ reification
     |}.

diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v
index fcc2a37..7b70e6e 100644 (file)
--- a/src/HaskProofFlattener.v
+++ b/src/HaskProofFlattener.v
@@ -116,13 +116,12 @@ Section HaskProofFlattener.
     admit.
     Defined.
 
-  Definition guestJudgmentAsGArrowType {Γ}{Δ}{ec}(lt:PCFJudg Γ Δ ec) : HaskType Γ ★ :=
+  Definition guestJudgmentAsGArrowType {Γ}{Δ}(lt:PCFJudg Γ Δ) : HaskType Γ ★ :=
     match lt with
-      pcfjudg x y =>
-      (mkGA (tensorizeType x) (tensorizeType y)) 
+      (x,y) => (mkGA (tensorizeType x) (tensorizeType y)) 
     end.
 
-  Definition obact {Γ}{Δ} ec (X:Tree ??(PCFJudg Γ Δ ec)) : Tree ??(LeveledHaskType Γ ★) :=
+  Definition obact {Γ}{Δ} (X:Tree ??(PCFJudg Γ Δ)) : Tree ??(LeveledHaskType Γ ★) :=
     mapOptionTree guestJudgmentAsGArrowType X @@@ nil.
 
   Hint Constructors Rule_Flat.
@@ -133,11 +132,11 @@ Section HaskProofFlattener.
    * it might help to have the definition for "Inductive ND" (see
    * NaturalDeduction.v) handy as a cross-reference.
    *)
-(*
+  Hint Constructors Rule_Flat.
   Definition FlatteningFunctor_fmor {Γ}{Δ}{ec}
     : forall h c,
-      (h~~{JudgmentsL _ _ (PCF _ Γ Δ ec)}~~>c) ->
-      ((obact ec h)~~{TypesL _ _ (SystemFCa Γ Δ)}~~>(obact ec c)).
+      (h~~{JudgmentsL (PCF Γ Δ ec)}~~>c) ->
+      ((obact(Δ:=ec) h)~~{TypesL (SystemFCa Γ Δ)}~~>(obact(Δ:=ec) c)).
 
     set (@nil (HaskTyVar Γ ★)) as lev.
 
@@ -146,40 +145,49 @@ Section HaskProofFlattener.
     induction X; simpl.
 
     (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *)
-    apply nd_rule; apply (org_fc _ _ (RVoid _ _ )). auto.
+    apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVoid _ _)). apply Flat_RVoid.
 
     (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
-    apply nd_rule; apply (org_fc _ _ (RVar _ _ _ _)). auto.
+    apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)). apply Flat_RVar.
 
     (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *)
     eapply nd_comp;
       [ idtac
       | eapply nd_rule
-      ; eapply (org_fc  _ _ (RArrange _ _ _ _ _ (RWeak _)))
+      ; eapply (org_fc  _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RWeak _)))
       ; auto ].
       eapply nd_rule.
-      eapply (org_fc _ _ (RVoid _ _)); auto.
-    
+      eapply (org_fc _ _ [] [(_,_)] (RVoid _ _)); auto. apply Flat_RVoid.
+      apply Flat_RArrange.
+
     (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *)
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RCont _))) ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCont _))) ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
-      set (snd_initial(SequentND:=@pl_snd  _ _ _ _ (SystemFCa Γ Δ))
-        (mapOptionTree guestJudgmentAsGArrowType h @@@ lev)) as q.
+      set (snd_initial(SequentND:=pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))
+        (mapOptionTree (guestJudgmentAsGArrowType(Δ:=ec)) h @@@ lev)) as q.
       eapply nd_comp.
       eapply nd_prod.
       apply q.
       apply q.
       apply nd_rule. 
-      eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )).
-      auto.
-      auto.
+      eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
+      destruct h; simpl.
+      destruct o.
+      simpl.
+      apply Flat_RJoin.
+      apply Flat_RJoin.
+      apply Flat_RJoin.
+      apply Flat_RArrange.
 
     (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *)
     eapply nd_comp.
       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
       apply nd_rule.
-      eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )).
-      auto.
+      eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
+      apply (Flat_RJoin Γ Δ (mapOptionTree guestJudgmentAsGArrowType h1 @@@ nil)
+       (mapOptionTree guestJudgmentAsGArrowType h2 @@@ nil)
+       (mapOptionTree guestJudgmentAsGArrowType c1 @@@ nil)
+       (mapOptionTree guestJudgmentAsGArrowType c2 @@@ nil)).
 
     (* nd_comp becomes pl_subst (aka nd_cut) *)
     eapply nd_comp.
@@ -192,39 +200,39 @@ Section HaskProofFlattener.
 
     (* nd_cancell becomes RVar;;RuCanL *)
     eapply nd_comp;
-      [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL _))) ].
-      apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
-      auto.
+      [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanL _))) ].
+      apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
+      apply Flat_RArrange.
 
     (* nd_cancelr becomes RVar;;RuCanR *)
     eapply nd_comp;
-      [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR _))) ].
-      apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
-      auto.
+      [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanR _))) ].
+      apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
+      apply Flat_RArrange.
 
     (* nd_llecnac becomes RVar;;RCanL *)
     eapply nd_comp;
-      [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL _))) ].
-      apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
-      auto.
+      [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanL _))) ].
+      apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
+      apply Flat_RArrange.
 
     (* nd_rlecnac becomes RVar;;RCanR *)
     eapply nd_comp;
-      [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR _))) ].
-      apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
-      auto.
+      [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanR _))) ].
+      apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
+      apply Flat_RArrange.
 
     (* nd_assoc becomes RVar;;RAssoc *)
     eapply nd_comp;
-      [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
-      apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
-      auto.
+      [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
+      apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
+      apply Flat_RArrange.
 
     (* nd_cossa becomes RVar;;RCossa *)
     eapply nd_comp;
-      [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
-      apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
-      auto.
+      [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
+      apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
+      apply Flat_RArrange.
 
       destruct r as [r rp].
       refine (match rp as R in @Rule_PCF _ _ _ H C _ with
@@ -316,9 +324,11 @@ Section HaskProofFlattener.
       destruct case_RNote.
         eapply nd_comp.
         eapply nd_rule.
-        eapply (org_fc _ _ (RVar _ _ _ _)) . auto.
+        eapply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)) . auto.
+        apply Flat_RVar.
         apply nd_rule.
-        apply (org_fc _ _ (RNote _ _ _ _ _ n)). auto.
+        apply (org_fc _ _ [(_,_)] [(_,_)] (RNote _ _ _ _ _ n)). auto.
+        apply Flat_RNote.
         
       destruct case_RVar.
         (* ga_id *)
@@ -346,23 +356,23 @@ Section HaskProofFlattener.
 
       Defined.
 
-  Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF _ Γ Δ ec)) (TypesL _ _ (SystemFCa Γ Δ)) (obact ec) :=
+  Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
     { fmor := FlatteningFunctor_fmor }.
     admit.
     admit.
     admit.
     Defined.
-(*
-    Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
-      refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
-      unfold ReificationFunctor_fmor; simpl.
-      admit.
-      unfold ReificationFunctor_fmor; simpl.
-      admit.
-      unfold ReificationFunctor_fmor; simpl.
-      admit.
-      Defined.
 
+  (*
+  Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
+    refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
+    unfold ReificationFunctor_fmor; simpl.
+    admit.
+    unfold ReificationFunctor_fmor; simpl.
+    admit.
+    unfold ReificationFunctor_fmor; simpl.
+    admit.
+    Defined.
 
   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
     refine {| plsmme_pl := PCF n Γ Δ |}.
@@ -383,7 +393,7 @@ Section HaskProofFlattener.
     admit.
     (*  ... and the retraction exists *)
     Defined.
-*)
+  *)
   (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so
    * it falls within (SystemFCa n) for some n.  This function calculates that "n" and performs the translation *)
   (*
@@ -391,8 +401,7 @@ Section HaskProofFlattener.
     forall h c (pf:ND Rule h c),
       { n:nat & h ~~{JudgmentsL (SystemFCa_SMME n)}~~> c }.
       *)
-
   (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
-*)
+
 End HaskProofFlattener.
 

diff --git a/src/HaskProofStratified.v b/src/HaskProofStratified.v
index 5c5f68a..ee475da 100644 (file)
--- a/src/HaskProofStratified.v
+++ b/src/HaskProofStratified.v
@@ -55,18 +55,22 @@ Open Scope nd_scope.
  *)
 Section HaskProofStratified.
 
+  Section PCF.
+
   Context (ndr_systemfc:@ND_Relation _ Rule).
 
-  Inductive PCFJudg Γ (Δ:CoercionEnv Γ) (ec:HaskTyVar Γ ★) :=
-    pcfjudg : Tree ??(HaskType Γ ★) -> Tree ??(HaskType Γ ★) -> PCFJudg Γ Δ ec.
-    Implicit Arguments pcfjudg [ [Γ] [Δ] [ec] ].
+  Context Γ (Δ:CoercionEnv Γ).
+  Definition PCFJudg (ec:HaskTyVar Γ ★) :=
+    @prod (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
+  Definition pcfjudg (ec:HaskTyVar Γ ★) :=
+    @pair (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
 
   (* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg
    * from depth (depth) by wrapping brackets around everything in the
    * succedent and repopulating *)
-  Definition brakify {Γ}{Δ}{ec} (j:PCFJudg Γ Δ ec) : Judg :=
+  Definition brakify {ec} (j:PCFJudg ec) : Judg :=
     match j with
-      pcfjudg Σ τ => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil)
+      (Σ,τ) => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil)
       end.
 
   Definition pcf_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
@@ -77,13 +81,13 @@ Section HaskProofStratified.
                               end
       end) t.
 
-  Inductive MatchingJudgments {Γ}{Δ}{ec} : Tree ??(PCFJudg Γ Δ ec) -> Tree ??Judg -> Type :=
+  Inductive MatchingJudgments {ec} : Tree ??(PCFJudg ec) -> Tree ??Judg -> Type :=
     | match_nil    : MatchingJudgments [] []
     | match_branch : forall a b c d, MatchingJudgments a b -> MatchingJudgments c d -> MatchingJudgments (a,,c) (b,,d)
     | match_leaf   : 
       forall Σ τ lev,
         MatchingJudgments
-          [pcfjudg (pcf_vars ec Σ)                               τ         ]
+          [((pcf_vars ec Σ)         ,                              τ        )]
           [Γ > Δ >              Σ  |- (mapOptionTree (HaskBrak ec) τ @@@ lev)].
 
   Definition fc_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
@@ -94,56 +98,69 @@ Section HaskProofStratified.
                               end
       end) t.
 
-  Definition pcfjudg2judg {Γ}{Δ:CoercionEnv Γ} ec (cj:PCFJudg Γ Δ ec) :=
-    match cj with pcfjudg Σ τ => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
+  Definition pcfjudg2judg ec (cj:PCFJudg ec) :=
+    match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
 
   (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows     *)
   (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
   (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements        *)
-  Inductive Rule_PCF {Γ}{Δ:CoercionEnv Γ} (ec:HaskTyVar Γ ★)
-    : forall (h c:Tree ??(PCFJudg Γ Δ ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
-  | PCF_RArrange    : ∀ x y t     a,  Rule_PCF ec [pcfjudg _  _ ] [ pcfjudg _  _  ] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
-  | PCF_RLit        : ∀ lit        ,  Rule_PCF ec [           ] [ pcfjudg [] [_] ] (RLit   Γ Δ  lit (ec::nil))
-  | PCF_RNote       : ∀ Σ τ   n    ,  Rule_PCF ec [pcfjudg _ [_]] [ pcfjudg _ [_] ] (RNote  Γ Δ  (Σ@@@(ec::nil)) τ         (ec::nil) n)
-  | PCF_RVar        : ∀ σ          ,  Rule_PCF ec [           ] [ pcfjudg [_] [_] ] (RVar   Γ Δ    σ         (ec::nil)  )
-  | PCF_RLam        : ∀ Σ tx te    ,  Rule_PCF ec [pcfjudg (_,,[_]) [_] ] [ pcfjudg _ [_] ] (RLam   Γ Δ  (Σ@@@(ec::nil)) tx te  (ec::nil)  )
+  Inductive Rule_PCF (ec:HaskTyVar Γ ★)
+    : forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
+  | PCF_RArrange    : ∀ x y t     a,  Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
+  | PCF_RLit        : ∀ lit        ,  Rule_PCF ec [           ] [ ([],[_]) ] (RLit   Γ Δ  lit (ec::nil))
+  | PCF_RNote       : ∀ Σ τ   n    ,  Rule_PCF ec [(_,[_])] [(_,[_])] (RNote  Γ Δ  (Σ@@@(ec::nil)) τ         (ec::nil) n)
+  | PCF_RVar        : ∀ σ          ,  Rule_PCF ec [           ] [([_],[_])] (RVar   Γ Δ    σ         (ec::nil)  )
+  | PCF_RLam        : ∀ Σ tx te    ,  Rule_PCF ec [((_,,[_]),[_])] [(_,[_])] (RLam   Γ Δ  (Σ@@@(ec::nil)) tx te  (ec::nil)  )
 
   | PCF_RApp             : ∀ Σ Σ' tx te ,
-    Rule_PCF ec ([pcfjudg _ [_]],,[pcfjudg _ [_]]) [pcfjudg (_,,_) [_]]
+    Rule_PCF ec ([(_,[_])],,[(_,[_])]) [((_,,_),[_])]
     (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil))
 
   | PCF_RLet             : ∀ Σ Σ' σ₂   p,
-    Rule_PCF ec ([pcfjudg _ [_]],,[pcfjudg (_,,[_]) [_]]) [pcfjudg (_,,_) [_]]
+    Rule_PCF ec ([(_,[_])],,[((_,,[_]),[_])]) [((_,,_),[_])]
     (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil))
 
-  | PCF_RVoid      :                 Rule_PCF ec [           ] [ pcfjudg []  [] ] (RVoid   Γ Δ  )
+  | PCF_RVoid      :                 Rule_PCF ec [           ] [([],[])] (RVoid   Γ Δ  )
 (*| PCF_RLetRec          : ∀ Σ₁ τ₁ τ₂   ,  Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*)
-  | PCF_RJoin    : ∀ Σ₁ Σ₂ τ₁ τ₂,  Rule_PCF ec ([pcfjudg _ _],,[pcfjudg _ _]) [pcfjudg (_,,_) (_,,_)]
+  | PCF_RJoin    : ∀ Σ₁ Σ₂ τ₁ τ₂,  Rule_PCF ec ([(_,_)],,[(_,_)]) [((_,,_),(_,,_))]
     (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
   (* need int/boolean case *)
   Implicit Arguments Rule_PCF [ ].
 
-  Definition PCFRule Γ Δ lev h c := { r:_ & @Rule_PCF Γ Δ lev h c r }.
+  Definition PCFRule lev h c := { r:_ & @Rule_PCF lev h c r }.
+  End PCF.
+
+  Definition FCJudg Γ (Δ:CoercionEnv Γ) :=
+    @prod (Tree ??(LeveledHaskType Γ ★)) (Tree ??(LeveledHaskType Γ ★)).
+  Definition fcjudg2judg {Γ}{Δ}(fc:FCJudg Γ Δ) :=
+    match fc with
+      (x,y) => Γ > Δ > x |- y
+        end.
+  Coercion fcjudg2judg : FCJudg >-> Judg.
+
+  Definition pcfjudg2fcjudg {Γ}{Δ} ec (fc:PCFJudg Γ ec) : FCJudg Γ Δ :=
+    match fc with
+      (x,y) => (x @@@ (ec::nil),y @@@ (ec::nil))
+        end.
 
   (* An organized deduction has been reorganized into contiguous blocks whose
    * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth.  The boolean
    * indicates if non-PCF rules have been used *)
-  Inductive OrgR : Tree ??Judg -> Tree ??Judg -> Type :=
+  Inductive OrgR Γ Δ : Tree ??(FCJudg Γ Δ) -> Tree ??(FCJudg Γ Δ) -> Type :=
 
-  | org_fc        : forall h c (r:Rule h c),
+  | org_fc        : forall (h c:Tree ??(FCJudg Γ Δ))
+    (r:Rule (mapOptionTree fcjudg2judg h) (mapOptionTree fcjudg2judg c)),
     Rule_Flat r ->
-    OrgR h c
+    OrgR _ _ h c
 
-  | org_pcf      : forall Γ Δ ec h h' c c',
-    MatchingJudgments    h  h' ->
-    MatchingJudgments    c  c' ->
-    ND (PCFRule Γ Δ ec)  h  c  ->
-    OrgR                 h' c'.
+  | org_pcf      : forall ec h c,
+    ND (PCFRule Γ Δ ec)  h c  ->
+    OrgR        Γ Δ     (mapOptionTree (pcfjudg2fcjudg ec) h)  (mapOptionTree (pcfjudg2fcjudg ec) c).
 
-  Definition mkEsc {Γ}{Δ}{ec}(h:Tree ??(PCFJudg Γ Δ ec))
+  Definition mkEsc Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
     : ND Rule
-    (mapOptionTree brakify h)
-    (mapOptionTree (pcfjudg2judg ec) h).
+    (mapOptionTree (brakify Γ Δ) h)
+    (mapOptionTree (pcfjudg2judg Γ Δ ec) h).
     apply nd_replicate; intros.
     destruct o; simpl in *.
     induction t0.
@@ -154,10 +171,10 @@ Section HaskProofStratified.
     apply (Prelude_error "mkEsc got multi-leaf succedent").
     Defined.
 
-  Definition mkBrak {Γ}{Δ}{ec}(h:Tree ??(PCFJudg Γ Δ ec))
+  Definition mkBrak Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
     : ND Rule
-    (mapOptionTree (pcfjudg2judg ec) h)
-    (mapOptionTree brakify h).
+    (mapOptionTree (pcfjudg2judg Γ Δ ec) h)
+    (mapOptionTree (brakify Γ Δ) h).
     apply nd_replicate; intros.
     destruct o; simpl in *.
     induction t0.
@@ -175,8 +192,8 @@ Section HaskProofStratified.
       pcf_vars ec Σ = snd vars }.
       *)
 
-  Definition pcfToND : forall Γ Δ ec h c,
-    ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c).
+  Definition pcfToND Γ Δ : forall ec h c,
+    ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c).
     intros.
     eapply (fun q => nd_map' _ q X).
     intros.
@@ -186,19 +203,8 @@ Section HaskProofStratified.
     Defined.
     
   Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) :=
-    { ndr_eqv := fun a b f g => (pcfToND _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      Defined.
+    { ndr_eqv := fun a b f g => (pcfToND  _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
+    Admitted.
 
   (*
    * An intermediate representation necessitated by Coq's termination
@@ -218,8 +224,8 @@ Section HaskProofStratified.
       Alternating c
 
     | alt_pcf    : forall Γ Δ ec h c h' c',
-      MatchingJudgments    h  h' ->
-      MatchingJudgments    c  c' ->
+      MatchingJudgments Γ Δ  h  h' ->
+      MatchingJudgments Γ Δ  c  c' ->
       Alternating h' ->
       ND (PCFRule Γ Δ ec) h c ->
       Alternating c'.
@@ -229,8 +235,8 @@ Section HaskProofStratified.
   Lemma magic a b c d ec e :
     ClosedSIND(Rule:=Rule) [a > b > c |- [d @@  (ec :: e)]] ->
     ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@  (ec :: nil)]].
-  admit.
-  Defined.
+    admit.
+    Defined.
 
   Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ].
 
@@ -243,8 +249,8 @@ Section HaskProofStratified.
         | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _
         | T_Branch b1 b2                 => let case_branch := tt in fun eqpf => _
       end (refl_equal _))
-      with orgify_pcf   Γ Δ ec pcfj j (m:MatchingJudgments pcfj j)
-        (pf:ClosedSIND (mapOptionTree (pcfjudg2judg ec) pcfj)) {struct pf} : Alternating j :=
+      with orgify_pcf   Γ Δ ec pcfj j (m:MatchingJudgments Γ Δ pcfj j)
+        (pf:ClosedSIND (mapOptionTree (pcfjudg2judg Γ Δ ec) pcfj)) {struct pf} : Alternating j :=
         let case_pcf := tt in _
       for orgify_fc').
 
@@ -296,11 +302,11 @@ Section HaskProofStratified.
 
   Definition pcfify Γ Δ ec : forall Σ τ,
     ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]
-      -> ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ].
+      -> ND (PCFRule Γ Δ ec) [] [(Σ,τ)].
 
     refine ((
       fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn}
-      : ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ] :=
+      : ND (PCFRule Γ Δ ec) [] [(Σ,τ)] :=
      (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with
       | cnd_weak             => let case_nil    := tt in _
       | cnd_rule h c cnd' r  => let case_rule   := tt in _
@@ -314,13 +320,12 @@ Section HaskProofStratified.
       Admitted.
 
   (* any proof in organized form can be "dis-organized" *)
-  Definition unOrgR : forall h c, OrgR h c -> ND Rule h c.
+  (*
+  Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c.
     intros.
-
     induction X.
       apply nd_rule.
       apply r.
-
     eapply nd_comp.
       (*
       apply (mkEsc h).
@@ -329,31 +334,16 @@ Section HaskProofStratified.
       apply n.
       *)
       Admitted.
-
-  Definition unOrgND h c :  ND OrgR h c -> ND Rule h c := nd_map unOrgR.
+  Definition unOrgND Γ Δ h c :  ND (OrgR Γ Δ) h c -> ND Rule h c := nd_map (unOrgR Γ Δ).
+  *)
     
-  Instance OrgNDR : @ND_Relation _ OrgR :=
-    { ndr_eqv := fun a b f g => (unOrgND _ _ f) === (unOrgND _ _ g) }.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      Defined.
-
   Hint Constructors Rule_Flat.
 
-  Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [pcfjudg x z] [pcfjudg y z].
+  Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)].
     admit.
     Defined.
 
-  Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([ pcfjudg a b ],,[ pcfjudg b c ]) [ pcfjudg a c ].
+  Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([(a,b)],,[(b,c)]) [(a,c)].
     intros.
     destruct b.
     destruct o.
@@ -368,7 +358,7 @@ Section HaskProofStratified.
       apply RuCanL.
       eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
       apply nd_rule.
-(*
+      (*
       set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
       exists q.
       apply (PCF_RLet _ [] a h0 h).
@@ -376,15 +366,10 @@ Section HaskProofStratified.
     apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
     apply (Prelude_error "cut rule invoked with [a|=[]]  [[]|=c]").
     apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
-*)
-    admit.
-    admit.
-    admit.
-    admit.
-    admit.
-    Defined.
+    *)
+    Admitted.
 
-  Instance PCF_sequents Γ Δ lev : @SequentND _ (PCFRule Γ Δ lev) _ pcfjudg :=
+  Instance PCF_sequents Γ Δ lev ec : @SequentND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ ec) :=
     { snd_cut := PCF_cut Γ Δ lev }.
     apply Build_SequentND.
     intros.
@@ -405,78 +390,69 @@ Section HaskProofStratified.
       admit.
         Defined.
 
-  Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (a,,b) (a,,c)].
+  Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((a,,b),(a,,c))].
     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
     eapply nd_prod; [ apply snd_initial | apply nd_id ].
     apply nd_rule.
     set (@PCF_RJoin Γ Δ lev a b a c) as q'.
     refine (existT _ _ _).
     apply q'.
-    Defined.
+    Admitted.
 
-  Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (b,,a) (c,,a)].
+  Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((b,,a),(c,,a))].
     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
     eapply nd_prod; [ apply nd_id | apply snd_initial ].
     apply nd_rule.
     set (@PCF_RJoin Γ Δ lev b a c a) as q'.
     refine (existT _ _ _).
     apply q'.
-    Defined.
+    Admitted.
 
-  Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ pcfjudg _ :=
+  Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ lev) _ :=
   { cnd_expand_left  := fun a b c => PCF_left  Γ Δ lev c a b
   ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
-    admit.
-    admit.
-    admit.
-    admit.
-    admit.
-    admit.
-    Defined.
-
-  Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) OrgND.
-    admit.
-    Defined.
 
-  Instance OrgPCF_ContextND_Relation Γ Δ lev : ContextND_Relation (PCF_sequent_join Γ Δ lev).
-    admit.
-    Defined.
-(*
-  (* 5.1.3 *)
-  Instance PCF Γ Δ lev : @ProgrammingLanguage _ pcfjudg (PCFRule Γ Δ lev) :=
-  { pl_eqv                := OrgPCF_ContextND_Relation Γ Δ lev
-  ; pl_snd                := PCF_sequents Γ Δ lev
-  }.
-  (*
-    apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
-
-    apply nd_rule. unfold PCFRule. simpl.
+    intros; apply nd_rule. unfold PCFRule. simpl.
       exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
-      apply (PCF_RArrange lev ((a,,b),,c) (a,,(b,,c)) x).
+      apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
 
-    apply nd_rule. unfold PCFRule. simpl.
+    intros; apply nd_rule. unfold PCFRule. simpl.
       exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
-      apply (PCF_RArrange lev (a,,(b,,c)) ((a,,b),,c) x).
+      apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
 
-    apply nd_rule. unfold PCFRule. simpl.
+    intros; apply nd_rule. unfold PCFRule. simpl.
       exists (RArrange _ _ _ _ _ (RCanL _)).
-      apply (PCF_RArrange lev ([],,a) _ _).
+      apply (PCF_RArrange _ _ lev ([],,a) _ _).
 
-    apply nd_rule. unfold PCFRule. simpl.
+    intros; apply nd_rule. unfold PCFRule. simpl.
       exists (RArrange _ _ _ _ _ (RCanR _)).
-      apply (PCF_RArrange lev (a,,[]) _ _).
+      apply (PCF_RArrange _ _ lev (a,,[]) _ _).
 
-    apply nd_rule. unfold PCFRule. simpl.
+    intros; apply nd_rule. unfold PCFRule. simpl.
       exists (RArrange _ _ _ _ _ (RuCanL _)).
-      apply (PCF_RArrange lev _ ([],,a) _).
+      apply (PCF_RArrange _ _ lev _ ([],,a) _).
 
-    apply nd_rule. unfold PCFRule. simpl.
+    intros; apply nd_rule. unfold PCFRule. simpl.
       exists (RArrange _ _ _ _ _ (RuCanR _)).
-      apply (PCF_RArrange lev _ (a,,[]) _).
+      apply (PCF_RArrange _ _ lev _ (a,,[]) _).
       Defined.
-*)
 
-  Definition SystemFCa_cut Γ Δ : forall a b c, ND OrgR ([ Γ > Δ > a |- b ],,[ Γ > Δ > b |- c ]) [ Γ > Δ > a |- c ].
+  Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev).
+    admit.
+    Defined.
+
+  Definition OrgPCF_ContextND_Relation Γ Δ lev
+    : @ContextND_Relation _ _ _ _ _ (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev) (OrgPCF_SequentND_Relation Γ Δ lev).
+    admit.
+    Defined.
+
+  (* 5.1.3 *)
+  Instance PCF Γ Δ lev : ProgrammingLanguage :=
+  { pl_cnd     := PCF_sequent_join Γ Δ lev
+  ; pl_eqv     := OrgPCF_ContextND_Relation Γ Δ lev
+  }.
+
+  Definition SystemFCa_cut Γ Δ : forall a b c, ND (OrgR Γ Δ) ([(a,b)],,[(b,c)]) [(a,c)].
     intros.
     destruct b.
     destruct o.
@@ -484,11 +460,14 @@ Section HaskProofStratified.
     destruct o.
 
     (* when the cut is a single leaf and the RHS is a single leaf: *)
+    (*
     eapply nd_comp.
       eapply nd_prod.
       apply nd_id.
       eapply nd_rule.
-      apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [l])).
+      set (@org_fc) as ofc.
+      set (RArrange Γ Δ _ _ _ (RuCanL [l0])) as rule.
+      apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [_])).
       auto.
       eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
       apply nd_rule.
@@ -499,18 +478,21 @@ Section HaskProofStratified.
       apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2). 
       auto.
       auto.
+      *)
+    admit.
     apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[]]").
     apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
     apply (Prelude_error "systemfc rule invoked with [a|=[]]  [[]|=c]").
     apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
     Defined.
 
-  Instance SystemFCa_sequents Γ Δ : @SequentND _ OrgR _ (mkJudg Γ Δ) :=
+  Instance SystemFCa_sequents Γ Δ : @SequentND _ (OrgR Γ Δ) _ _ :=
   { snd_cut := SystemFCa_cut Γ Δ }.
     apply Build_SequentND.
     intros.
     induction a.
     destruct a; simpl.
+    (*
     apply nd_rule.
       destruct l.
       apply org_fc with (r:=RVar _ _ _ _).
@@ -525,51 +507,82 @@ Section HaskProofStratified.
         apply org_fc with (r:=RJoin _ _ _ _ _ _). 
         auto.
       admit.
-        Defined.
+      *)
+      admit.
+      admit.
+      admit.
+      admit.
+      Defined.
 
-  Definition SystemFCa_left Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (a,,b) |- (a,,c)].
+  Definition SystemFCa_left Γ Δ a b c : ND (OrgR Γ Δ) [(b,c)] [((a,,b),(a,,c))].
+    admit.
+    (*
     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
     eapply nd_prod; [ apply snd_initial | apply nd_id ].
     apply nd_rule.
     apply org_fc with (r:=RJoin Γ Δ a b a c).
     auto.
+    *)
     Defined.
 
-  Definition SystemFCa_right Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (b,,a) |- (c,,a)].
+  Definition SystemFCa_right Γ Δ a b c : ND (OrgR Γ Δ) [(b,c)] [((b,,a),(c,,a))].
+    admit.
+    (*
     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
     eapply nd_prod; [ apply nd_id | apply snd_initial ].
     apply nd_rule.
     apply org_fc with (r:=RJoin Γ Δ b a c a).
     auto.
+    *)
     Defined.
 
-(*
-  Instance SystemFCa_sequent_join Γ Δ : @SequentExpansion _ _ _ _ _ (SystemFCa_sequents Γ Δ) (SystemFCa_cutrule Γ Δ) :=
-  { se_expand_left  := SystemFCa_left  Γ Δ 
-  ; se_expand_right := SystemFCa_right Γ Δ }.
-    admit.
-    admit.
+  Instance SystemFCa_sequent_join Γ Δ : @ContextND _ _ _ _ (SystemFCa_sequents Γ Δ) :=
+  { cnd_expand_left  := fun a b c => SystemFCa_left Γ Δ c a b
+  ; cnd_expand_right := fun a b c => SystemFCa_right Γ Δ c a b }.
+    (*
+    intros; apply nd_rule. simpl.
+      apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))).
+      auto.
+
+    intros; apply nd_rule. simpl.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto.
+
+    intros; apply nd_rule. simpl.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto.
+
+    intros; apply nd_rule. simpl.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto.
+
+    intros; apply nd_rule. simpl.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto.
+
+    intros; apply nd_rule. simpl.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto.
+      *)
+      admit.
+      admit.
+      admit.
+      admit.
+      admit.
+      admit.
+      Defined.
+
+  Instance OrgFC Γ Δ : @ND_Relation _ (OrgR Γ Δ).
+    Admitted.
+
+  Instance OrgFC_SequentND_Relation Γ Δ : SequentND_Relation (SystemFCa_sequent_join Γ Δ) (OrgFC Γ Δ).
     admit.
+    Defined.
+
+  Definition OrgFC_ContextND_Relation Γ Δ
+    : @ContextND_Relation _ _ _ _ _ (SystemFCa_sequent_join Γ Δ) (OrgFC Γ Δ) (OrgFC_SequentND_Relation Γ Δ).
     admit.
     Defined.
-*)
+
   (* 5.1.2 *)
-  Instance SystemFCa Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) OrgR.
-(*
-  { pl_eqv                := OrgNDR
-  ; pl_sn                 := SystemFCa_sequents     Γ Δ
-  ; pl_subst              := SystemFCa_cutrule      Γ Δ
-  ; pl_sequent_join       := SystemFCa_sequent_join Γ Δ
+  Instance SystemFCa Γ Δ : @ProgrammingLanguage (LeveledHaskType Γ ★) _ :=
+  { pl_eqv                := OrgFC_ContextND_Relation Γ Δ
+  ; pl_snd                := SystemFCa_sequents Γ Δ
   }.
-    apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
-    apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa a b c))). apply Flat_RArrange.
-    apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc a b c))). apply Flat_RArrange.
-    apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL  a    ))). apply Flat_RArrange.
-    apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR  a    ))). apply Flat_RArrange.
-    apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL a    ))). apply Flat_RArrange.
-    apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR a    ))). apply Flat_RArrange.
-*)
-admit.
-    Defined.
-*)
+
 End HaskProofStratified.

diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v
index e29903a..0636a6e 100644 (file)
--- a/src/ProgrammingLanguage.v
+++ b/src/ProgrammingLanguage.v
@@ -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,28 +171,28 @@ 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 }.
-      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 TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
@@ -241,9 +241,9 @@ Section Programming_Language.
           auto.
       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 : SurjectiveEnrichment.

diff --git a/src/ProgrammingLanguageArrow.v b/src/ProgrammingLanguageArrow.v
index f6a3940..5dbce6d 100644 (file)
--- a/src/ProgrammingLanguageArrow.v
+++ b/src/ProgrammingLanguageArrow.v
@@ -31,9 +31,8 @@ Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 
 Require Import ProgrammingLanguage.
-Require Import ProgrammingLanguageGeneralizedArrow.
 Require Import FreydCategories.
-
+Require Import Enrichments.
 Require Import GeneralizedArrow.
 
 Section ArrowInLanguage.
@@ -41,34 +40,36 @@ Section ArrowInLanguage.
   (* an Arrow In A Programming Language consists of... *)
 
   (* a host language: *)
-  Context `(Host:ProgrammingLanguage).
+  Context `(Host         : ProgrammingLanguage).
 
-  (* ... for which Types(L) is cartesian: *)
-  Context (center_of_TypesL:MonoidalCat (TypesL_PreMonoidal Host)).
+  Context  (Host_Monoidal  : MonoidalCat  (TypesL_PreMonoidal Host)).
+  Context  (Host_Cartesian : CartesianCat Host_Monoidal).
 
-  (* along with a full subcategory of Z(Types(L)) *)
-  Context {P}(VK:FullSubcategory (Center (TypesL_PreMonoidal Host)) P).
+  Context
+    {P}
+    (Pobj_unit   : P [])
+    (Pobj_closed : forall a b, P a → P b → P (bin_obj(BinoidalCat:=Center_is_PreMonoidal (TypesL_PreMonoidal Host)) a b)).
 
-  Context (Pobj_unit   : P []).
-  Context (Pobj_closed : forall a b, P a → P b → P (bin_obj(BinoidalCat:=Center_is_PreMonoidal (TypesL_PreMonoidal Host)) a b)).
-  Definition VKM :=
-    PreMonoidalFullSubcategory_PreMonoidal (Center_is_PreMonoidal (TypesL_PreMonoidal Host)) VK Pobj_unit Pobj_closed.
+  Context (VK : FullSubcategory Host_Cartesian P).
 
-  (* a premonoidal category enriched in aforementioned full subcategory *)
-  Context (Kehom:(Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host)) -> @ob _ _ VK).
-  Context (KE   :@ECategory (@ob _ _ VK) (@hom _ _ VK) VK _ VKM (pmon_I VKM) VKM (Center (TypesL_PreMonoidal Host)) Kehom).
-  Context {kbo  :(Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host))}.
-  Context (kbc  :@BinoidalCat (Center (TypesL_PreMonoidal Host)) _ (Underlying KE) kbo).
+  Context  ehom KE (K_bin:@EBinoidalCat _ _ VK _ _ _
+          (PreMonoidalFullSubcategory_PreMonoidal Host_Cartesian VK Pobj_unit Pobj_closed)
+          (TypesL Host) ehom KE (bin_obj(BinoidalCat:=Host_Monoidal))).
 
-  Definition one' := @one _ _ _ (car_terminal(CartesianCat:=CC))
-  Context (K :@PreMonoidalCat _ _ KE kbo kbc ).
-  Context (CC:CartesianCat (Center (TypesL_PreMonoidal Host))).
+  Context (K_premonoidal:PreMonoidalCat K_bin (one(TerminalObject:=Host_Cartesian))).
 
   Definition ArrowInProgrammingLanguage :=
-    @FreydCategory _ _ _ _ _ _ (Center (TypesL_PreMonoidal Host)) _ _ _ _ K.
+    @FreydCategory _ _ _ _ _ _ _ _ Host_Cartesian _ _ K_bin K_premonoidal.
+
+  Definition K_enrichment : Enrichment.
+    refine
+      {| enr_c_pm  := K_premonoidal
+       ; enr_v_mon := MonoidalFullSubcategory_Monoidal Host_Cartesian _ _ VK
+      |}.
+      Defined.
 
-  Definition ArrowsAreGeneralizedArrows (arrow:ArrowInProgrammingLanguage) : GeneralizedArrow K_enrichment Host.
-    refine {| ga_functor_monoidal := inclusion_functor_monoidal VK |}.
-    Defined.
+  Instance ArrowsAreGeneralizedArrows : GeneralizedArrow K_enrichment (TypesEnrichedInJudgments Host) :=
+    { ga_functor_monoidal :=
+        PreMonoidalFullSubcategoryInclusionFunctor_PreMonoidal Host_Cartesian VK Pobj_unit Pobj_closed Host_Cartesian }.
 
-End GArrowInLanguage.
+End ArrowInLanguage.

diff --git a/src/ProgrammingLanguageFlattening.v b/src/ProgrammingLanguageFlattening.v
index f01621b..4438dd2 100644 (file)
--- a/src/ProgrammingLanguageFlattening.v
+++ b/src/ProgrammingLanguageFlattening.v
@@ -15,6 +15,8 @@ Require Import Enrichment_ch2_8.
 Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
 Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
@@ -25,51 +27,66 @@ Require Import Reification.
 Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 Require Import GeneralizedArrow.
-Require Import GeneralizedArrowFromReification.
 Require Import ProgrammingLanguage.
 Require Import ProgrammingLanguageReification.
+Require Import SectionRetract_ch2_4.
+Require Import GeneralizedArrowFromReification.
+Require Import Enrichments.
 Require Import ReificationsAndGeneralizedArrows.
 
 Section Flattening.
 
-  Context (Guest:ProgrammingLanguageSMME) (Host :ProgrammingLanguageSMME).
+  Context `(Guest:ProgrammingLanguage) `(Host :ProgrammingLanguage).
   Context (GuestHost:TwoLevelLanguage Guest Host).
 
-  Definition FlatObject (x:TypesL _ _ Host) :=
+  Definition FlatObject (x:TypesL Host) :=
     forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
 
-  Definition FlatSubCategory := FullSubcategory (TypesL _ _ Host) FlatObject.
+  Instance FlatSubCategory : FullSubcategory (TypesL Host) FlatObject.
 
-    Context  (F:Retraction (TypesL _ _ Host) FlatSubCategory).
+    Context  (F:RetractionOfCategories (TypesL Host) (FullSubCategoriesAreCategories FlatSubCategory)).
 
-    Definition FlatteningOfReification :=
-      garrow_from_reification Guest Host GuestHost >>>> F.
+    Definition FlatteningOfReification HostMonic HostMonoidal :=
+      (ga_functor
+        (@garrow_from_reification
+          (TypesEnrichedInJudgments Guest)
+          (TypesEnrichedInJudgments Host)
+          HostMonic HostMonoidal GuestHost))
+        >>>> F.
 
-(*
-    Lemma FlatteningIsNotDestructive : 
-      FlatteningOfReification >>>> retraction_retraction F >>>> HomFunctor _ (me_i Host) ≃ GuestHost.
+    Lemma FlatteningIsNotDestructive HostMonic HostMonoidal : 
+      FlatteningOfReification HostMonic HostMonoidal >>>> retraction_retraction F >>>> HomFunctor _ []
+      ≃ (reification_rstar GuestHost).
       apply if_inv.
-      set (@roundtrip_reification_to_reification _ Guest _ _ Host GuestHost) as q.
-      unfold mf_f in *; simpl in *.
-      apply (if_comp q).
+      set (@roundtrip_reification_to_reification (TypesEnrichedInJudgments Guest) (TypesEnrichedInJudgments Host)
+        HostMonic HostMonoidal GuestHost) as q.
+      unfold mf_F in *; simpl in *.
+      eapply if_comp.
+      apply q.
       clear q.
-      unfold me_mf; simpl.
-      unfold mf_f; simpl.
-      refine (if_respects _ (if_id _)).
+      unfold mf_F; simpl.
+      unfold pmon_I.
+      apply (if_respects
+        (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost)
+        (FlatteningOfReification HostMonic HostMonoidal >>>> retraction_retraction F)
+        (HomFunctor (TypesL Host) [])
+        (HomFunctor (TypesL Host) [])); [ idtac | apply (if_id _) ].
       unfold FlatteningOfReification.
-      unfold mf_f; simpl.
-      eapply if_comp.
-      Focus 2.
-      eapply if_inv.
-      apply (if_associativity (garrow_functor Guest Host GuestHost) F (retraction_retraction F)).
-      eapply if_comp.
-      eapply if_inv.
-      apply if_right_identity.
-      refine (if_respects (if_id _) _).
+      unfold mf_F; simpl.
       apply if_inv.
+      eapply if_comp.
+      apply (if_associativity (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost) F
+               (retraction_retraction F)).
+      eapply if_comp; [ idtac | apply if_right_identity ].
+      apply (if_respects
+        (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost)
+        (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost)
+        (F >>>> retraction_retraction F)
+        (functor_id _)).
+      apply (if_id _).
       apply retraction_composes.
       Qed.
-*)
+
 End Flattening.
 
 

diff --git a/src/ProgrammingLanguageReification.v b/src/ProgrammingLanguageReification.v
index f6a2a8e..932c517 100644 (file)
--- a/src/ProgrammingLanguageReification.v
+++ b/src/ProgrammingLanguageReification.v
@@ -28,9 +28,29 @@ Require Import Reification.
 Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 Require Import ProgrammingLanguage.
+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.
 
 (*
-  Structure ProgrammingLanguageSMME :=
+  Structure ProgrammingLanguage :=
   { plsmme_t       : Type
   ; plsmme_judg    : Type
   ; plsmme_sequent : Tree ??plsmme_t -> Tree ??plsmme_t -> plsmme_judg
@@ -38,25 +58,6 @@ Require Import ProgrammingLanguage.
   ; 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.
+  Coercion plsmme_pl   : ProgrammingLanguage >-> ProgrammingLanguage.
+  Coercion plsmme_smme : ProgrammingLanguage >-> 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,
-                          TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
-
-Definition OmegaLevelLanguage : Type :=
-  { f : nat -> ProgrammingLanguageSMME
-  & forall n, TwoLevelLanguage (f n) (f (S n)) }.
-

diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v
index 1a5fea7..730d91d 100644 (file)
--- a/src/ReificationFromGeneralizedArrow.v
+++ b/src/ReificationFromGeneralizedArrow.v
@@ -26,7 +26,7 @@ Require Import RepresentableStructure_ch7_2.
 Require Import Reification.
 Require Import GeneralizedArrow.
 
-Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K C)
+Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K ce)
  : Reification K ce (enr_c_i ce).
   refine
   {| reification_r         := fun k:K => HomFunctor K k >>>> ga_functor garrow

diff --git a/src/ReificationsAndGeneralizedArrows.v b/src/ReificationsAndGeneralizedArrows.v
index 4056c77..7924a43 100644 (file)
--- a/src/ReificationsAndGeneralizedArrows.v
+++ b/src/ReificationsAndGeneralizedArrows.v
@@ -71,9 +71,8 @@ Section ReificationsEquivalentToGeneralizedArrows.
     Qed.
 
   Lemma roundtrip_garrow_to_garrow
-    `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (garrow : GeneralizedArrow K CM)
+    `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (garrow : GeneralizedArrow K ce)
     : garrow ≃ garrow_from_reification K C CM (reification_from_garrow K CM garrow).
-
     apply if_inv.
     eapply if_comp.
     eapply if_inv.

diff --git a/src/categories b/src/categories
index 1104780..0ecd73c 160000 (submodule)
--- a/src/categories
+++ b/src/categories
@@ -1 +1 @@
-Subproject commit 1104780d775bf36ff9f44ab287c22604ab47f0b5
+Subproject commit 0ecd73c172f67634fa956fb52b332e6effb5a04d