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.
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.
- unfold hom; unfold ob; unfold ehom; simpl; unfold mon_i; unfold obact; intros.
+ unfold hom; unfold ob; unfold ehom; simpl; unfold pmon_I; unfold obact; intros.
induction X; simpl.
- (* the proof from no hypotheses of no conclusions (nd_id0) becomes REmptyGroup *)
- apply nd_rule; apply (org_fc _ _ (REmptyGroup _ _ )). auto.
+ (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *)
+ apply nd_rule; apply (org_fc _ _ (RVoid _ _ )). auto.
(* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
apply nd_rule; apply (org_fc _ _ (RVar _ _ _ _)). auto.
- (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;REmptyGroup *)
+ (* 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 _)))
; auto ].
eapply nd_rule.
- eapply (org_fc _ _ (REmptyGroup _ _)); auto.
+ eapply (org_fc _ _ (RVoid _ _)); auto.
- (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RBindingGroup;;RCont *)
+ (* 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.
apply q.
apply q.
apply nd_rule.
- eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )).
+ eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )).
auto.
auto.
- (* nd_prod becomes nd_llecnac;;nd_prod;;RBindingGroup *)
+ (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *)
eapply nd_comp.
apply (nd_llecnac ;; nd_prod IHX1 IHX2).
apply nd_rule.
- eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )).
+ eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )).
auto.
(* nd_comp becomes pl_subst (aka nd_cut) *)
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].
| PCF_RLam Σ tx te => let case_RLam := tt in _
| PCF_RApp Σ tx te p => let case_RApp := tt in _
| PCF_RLet Σ σ₁ σ₂ p => let case_RLet := tt in _
- | PCF_RBindingGroup b c d e => let case_RBindingGroup := tt in _
- | PCF_REmptyGroup => let case_REmptyGroup := tt in _
+ | PCF_RJoin b c d e => let case_RJoin := tt in _
+ | PCF_RVoid => let case_RVoid := tt in _
(*| PCF_RCase T κlen κ θ l x => let case_RCase := tt in _*)
(*| PCF_RLetRec Σ₁ τ₁ τ₂ lev => let case_RLetRec := tt in _*)
end); simpl in *.
(* ga_comp! perhaps this means the ga_curry avoidance can be done by turning lambdas into lets? *)
admit.
- destruct case_REmptyGroup.
+ destruct case_RVoid.
(* ga_id u *)
admit.
- destruct case_RBindingGroup.
+ destruct case_RJoin.
(* ga_first+ga_second; technically this assumes a specific evaluation order, which is bad *)
admit.
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.
projects / coq-hetmet.git / blobdiff