* it might help to have the definition for "Inductive ND" (see
* NaturalDeduction.v) handy as a cross-reference.
*)
+(*
Definition FlatteningFunctor_fmor {Γ}{Δ}{ec}
: forall h c,
(h~~{JudgmentsL _ _ (PCF _ Γ Δ ec)}~~>c) ->
- ((obact ec h)~~{TypesL _ _ (SystemFCa _ Γ Δ)}~~>(obact ec c)).
+ ((obact ec h)~~{TypesL _ _ (SystemFCa Γ Δ)}~~>(obact ec c)).
set (@nil (HaskTyVar Γ ★)) as lev.
(* 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; [ apply nd_llecnac | idtac ].
- set (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))
+ set (snd_initial(SequentND:=@pl_snd _ _ _ _ (SystemFCa Γ Δ))
(mapOptionTree guestJudgmentAsGArrowType h @@@ lev)) as q.
eapply nd_comp.
eapply nd_prod.
eapply nd_comp.
apply (nd_llecnac ;; nd_prod IHX1 IHX2).
clear IHX1 IHX2 X1 X2.
- apply (@nd_cut _ _ _ _ _ _ (@pl_subst _ _ _ _ (SystemFCa _ Γ Δ))).
+ (*
+ apply (@snd_cut _ _ _ _ _ _ (@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
+ *)
+ admit.
(* nd_cancell becomes RVar;;RuCanL *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL _))) ].
- apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))).
+ apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
auto.
(* nd_cancelr becomes RVar;;RuCanR *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR _))) ].
- apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))).
+ apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
auto.
(* nd_llecnac becomes RVar;;RCanL *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL _))) ].
- apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))).
+ apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
auto.
(* nd_rlecnac becomes RVar;;RCanR *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR _))) ].
- apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))).
+ apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
auto.
(* nd_assoc becomes RVar;;RAssoc *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
- apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))).
+ apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
auto.
(* nd_cossa becomes RVar;;RCossa *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
- apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))).
+ apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
auto.
destruct r as [r rp].
Defined.
- Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF _ Γ Δ ec)) (TypesL _ _ (SystemFCa _ Γ Δ)) (obact ec) :=
+ Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF _ Γ Δ ec)) (TypesL _ _ (SystemFCa Γ Δ)) (obact ec) :=
{ fmor := FlatteningFunctor_fmor }.
admit.
admit.
*)
(* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
-
+*)
End HaskProofFlattener.