1 (*********************************************************************************************************************************)
2 (* HaskProofCategory: *)
4 (* Natural Deduction proofs of the well-typedness of a Haskell term form a category *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import NaturalDeduction.
12 Require Import Coq.Strings.String.
13 Require Import Coq.Lists.List.
15 Require Import HaskKinds.
16 Require Import HaskCoreTypes.
17 Require Import HaskLiteralsAndTyCons.
18 Require Import HaskStrongTypes.
19 Require Import HaskProof.
20 Require Import NaturalDeduction.
21 Require Import NaturalDeductionCategory.
23 Require Import Algebras_ch4.
24 Require Import Categories_ch1_3.
25 Require Import Functors_ch1_4.
26 Require Import Isomorphisms_ch1_5.
27 Require Import ProductCategories_ch1_6_1.
28 Require Import OppositeCategories_ch1_6_2.
29 Require Import Enrichment_ch2_8.
30 Require Import Subcategories_ch7_1.
31 Require Import NaturalTransformations_ch7_4.
32 Require Import NaturalIsomorphisms_ch7_5.
33 Require Import MonoidalCategories_ch7_8.
34 Require Import Coherence_ch7_8.
36 Require Import HaskStrongTypes.
37 Require Import HaskStrong.
38 Require Import HaskProof.
39 Require Import HaskStrongToProof.
40 Require Import HaskProofToStrong.
41 Require Import ProgrammingLanguage.
45 Section HaskProofCategory.
47 Implicit Arguments RURule [[Γ][Δ][h][c]].
49 Context (ndr_systemfc:@ND_Relation _ Rule).
51 (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
52 (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
53 (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *)
54 Inductive Rule_PCF {Γ}{Δ} : ∀ h c, Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c) -> Type :=
55 | PCF_RCanL : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanL t a ))
56 | PCF_RCanR : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanR t a ))
57 | PCF_RuCanL : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanL t a ))
58 | PCF_RuCanR : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanR t a ))
59 | PCF_RAssoc : ∀ t a b c , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RAssoc t a b c ))
60 | PCF_RCossa : ∀ t a b c , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCossa t a b c ))
61 | PCF_RLeft : ∀ h c x , Rule (mapOptionTree (ext_tree_left x) h) (mapOptionTree (ext_tree_left x) c)
62 | PCF_RRight : ∀ h c x , Rule (mapOptionTree (ext_tree_right x) h) (mapOptionTree (ext_tree_right x) c)
63 | PCF_RExch : ∀ t a b , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RExch t a b ))
64 | PCF_RWeak : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RWeak t a ))
65 | PCF_RCont : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCont t a ))
67 | PCF_RLit : ∀ Σ τ , Rule_PCF [ ] [_>>_>_|-_] (RLit Γ Δ Σ τ )
68 | PCF_RNote : ∀ Σ τ l n , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RNote Γ Δ Σ τ l n)
69 | PCF_RVar : ∀ σ l, Rule_PCF [ ] [_>>_>_|-_] (RVar Γ Δ σ l)
70 | PCF_RLam : ∀ Σ tx te q , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RLam Γ Δ Σ tx te q )
71 | PCF_RApp : ∀ Σ tx te p l, Rule_PCF ([_>>_>_|-_],,[_>>_>_|-_]) [_>>_>_|-_] (RApp Γ Δ Σ tx te p l)
72 | PCF_RLet : ∀ Σ σ₁ σ₂ p l, Rule_PCF ([_>>_>_|-_],,[_>>_>_|-_]) [_>>_>_|-_] (RLet Γ Δ Σ σ₁ σ₂ p l)
73 | PCF_RBindingGroup : ∀ b c d e , Rule_PCF ([_>>_>_|-_],,[_>>_>_|-_]) [_>>_>_|-_] (RBindingGroup _ _ b c d e)
74 | PCF_REmptyGroup : Rule_PCF [ ] [_>>_>_|-_] (REmptyGroup _ _ ).
76 (* | PCF_RLetRec : ∀ Σ₁ τ₁ τ₂ lev , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).*)
77 Implicit Arguments Rule_PCF [ ].
79 (* need int/boolean case *)
80 (* | PCF_RCase : ∀ T κlen κ θ l x , Rule_PCF (RCase Γ Δ T κlen κ θ l x) (* FIXME: only for boolean and int *)*)
82 Definition PCFR Γ Δ h c := { r:_ & Rule_PCF Γ Δ h c r }.
84 (* this wraps code-brackets, with the specified environment classifier, around a type *)
85 Definition brakifyType {Γ} (ec:HaskTyVar Γ ★)(lt:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
87 t @@ l => HaskBrak ec t @@ l
90 Definition brakifyu {Γ}{Δ}(v:HaskTyVar Γ ★)(j:UJudg Γ Δ) : UJudg Γ Δ :=
93 Γ >> Δ > mapOptionTree (brakifyType v) Σ |- mapOptionTree (brakifyType v) τ
97 (* An organized deduction has been reorganized into contiguous blocks whose
98 * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth. The boolean
99 * indicates if non-PCF rules have been used *)
100 Inductive OrgR : bool -> nat -> forall Γ Δ, Tree ??(UJudg Γ Δ) -> Tree ??(UJudg Γ Δ) -> Type :=
102 | org_pcf : forall n Γ Δ h c b,
103 PCFR Γ Δ h c -> OrgR b n Γ Δ h c
105 | org_fc : forall n Γ Δ h c,
106 ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c) -> OrgR true n Γ Δ h c
108 | org_nest : forall n Γ Δ h c b v,
110 OrgR b (S n) _ _ (mapOptionTree (brakifyu v) h) (mapOptionTree (brakifyu v) c)
113 Definition OrgND b n Γ Δ := ND (OrgR b n Γ Δ).
115 Definition mkEsc {Γ}{Δ}(j:Tree ??(UJudg Γ Δ)) v h
117 (mapOptionTree (@UJudg2judg Γ Δ) h)
118 (mapOptionTree (fun j => @UJudg2judg Γ Δ (brakifyu v j)) h).
122 Definition mkBrak {Γ}{Δ}(j:Tree ??(UJudg Γ Δ)) v h
124 (mapOptionTree (fun j => @UJudg2judg Γ Δ (brakifyu v j)) h)
125 (mapOptionTree (@UJudg2judg Γ Δ ) h).
129 (* any proof in organized form can be "dis-organized" *)
130 Definition unOrgR b n Γ Δ : forall h c, OrgR b n Γ Δ h c ->
131 ND Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c).
142 rewrite <- mapOptionTree_compose.
143 rewrite <- mapOptionTree_compose.
146 eapply nd_comp; [ idtac | apply (mkEsc c) ].
150 Definition unOrgND b n Γ Δ h c :
151 ND (OrgR b n Γ Δ) h c -> ND Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c)
152 := nd_map' (@UJudg2judg Γ Δ) (unOrgR b n Γ Δ).
154 Instance OrgNDR b n Γ Δ : @ND_Relation _ (OrgR b n Γ Δ) :=
155 { ndr_eqv := fun a b f g => (unOrgND _ _ _ _ _ _ f) === (unOrgND _ _ _ _ _ _ g) }.
172 Hint Constructors Rule_Flat.
174 Definition SystemFC_SC n : @SequentCalculus _ (RuleSystemFCa n) _ (mkJudg Γ Δ).
175 apply Build_SequentCalculus.
181 apply sfc_flat with (r:=RVar _ _ _ _).
184 apply sfc_flat with (r:=REmptyGroup _ _).
186 eapply nd_comp; [ apply nd_llecnac | idtac ].
187 eapply nd_comp; [ eapply nd_prod | idtac ].
191 apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
195 Existing Instance SystemFC_SC.
197 Lemma systemfc_cut n : ∀a b c,
198 ND (RuleSystemFCa n) ([Γ > Δ > a |- b],, [Γ > Δ > b |- c]) [Γ > Δ > a |- c].
203 Lemma systemfc_cutrule n
204 : @CutRule _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfc n) (SystemFC_SC n).
205 apply Build_CutRule with (nd_cut:=systemfc_cut n).
211 Definition systemfc_left n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > a,, b |- a,, c].
212 eapply nd_comp; [ apply nd_llecnac | idtac ].
213 eapply nd_comp; [ eapply nd_prod | idtac ].
216 apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
219 apply nd_seq_reflexive.
223 Definition systemfc_right n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > b,,a |- c,,a].
224 eapply nd_comp; [ apply nd_rlecnac | idtac ].
225 eapply nd_comp; [ eapply nd_prod | idtac ].
227 apply (nd_seq_reflexive a).
229 apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
234 Definition systemfc_expansion n
235 : @SequentExpansion _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfca n) (SystemFC_SC n) (systemfc_cutrule n).
236 Check (@Build_SequentExpansion).
237 apply (@Build_SequentExpansion _ _ _ _ (ndr_systemfca n) _ _ (systemfc_left n) (systemfc_right n)).
238 refine {| se_expand_left:=systemfc_left n
239 ; se_expand_right:=systemfc_right n |}.
244 Instance SystemFCa n Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR true n Γ Δ) :=
245 { pl_eqv := OrgNDR true n Γ Δ
246 ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
249 ; pl_sequent_join := _
251 apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
252 apply nd_rule; apply org_fc; apply nd_rule; simpl. apply (RURule _ _ _ _ (RCossa _ a b c)).
253 apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RAssoc _ a b c)).
254 apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RCanL _ a )).
255 apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RCanR _ a )).
256 apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RuCanL _ a )).
257 apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RuCanR _ a )).
260 (* "flat" SystemFC: no brackets allowed *)
261 Instance SystemFC Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR true O Γ Δ) :=
262 { pl_eqv := OrgNDR true O Γ Δ
263 ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
266 ; pl_sequent_join := _
271 Instance PCF n Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR false n Γ Δ) :=
272 { pl_eqv := OrgNDR false n Γ Δ
273 ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
276 ; pl_sequent_join := _
278 apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
279 apply nd_rule; apply org_pcf; simpl; exists (RCossa _ a b c); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
280 apply nd_rule; apply org_pcf; simpl; exists (RAssoc _ a b c); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
281 apply nd_rule; apply org_pcf; simpl; exists (RCanL _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
282 apply nd_rule; apply org_pcf; simpl; exists (RCanR _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
283 apply nd_rule; apply org_pcf; simpl; exists (RuCanL _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
284 apply nd_rule; apply org_pcf; simpl; exists (RuCanR _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
288 Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
290 (* | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx t'*)
291 | _ => code2garrow0 ec unitType t
294 Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
295 match ty as TY in RawHaskType _ K return RawHaskType TV K with
296 | TCode ec t => code2garrow _ ec t
297 | TApp _ _ t1 t2 => TApp (typeMap t1) (typeMap t2)
298 | TAll _ f => TAll _ (fun tv => typeMap (f tv))
299 | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
303 | TyFunApp tf rhtl => (* FIXME *) TyFunApp tf rhtl
306 Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
308 (* | t @@ nil => (fun TV ite => typeMap (t TV ite)) @@ lev*)
309 | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
313 (* gathers a tree of guest-language types into a single host-language types via the tensor *)
314 Definition tensorizeType {Γ} (lt:Tree ??(LeveledHaskType Γ ★)) : HaskType Γ ★.
318 Definition mkGA {Γ} : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★.
322 Definition guestJudgmentAsGArrowType {Γ}{Δ} (lt:UJudg Γ Δ) : LeveledHaskType Γ ★ :=
325 (mkGA (tensorizeType x) (tensorizeType y)) @@ nil
328 Fixpoint obact n {Γ}{Δ}(X:Tree ??(UJudg Γ Δ)) : Tree ??(LeveledHaskType Γ ★) :=
330 | 0 => mapOptionTree guestJudgmentAsGArrowType X
331 | S n' => let t := obact n' X
332 in [guestJudgmentAsGArrowType (Γ >> Δ > [] |- t )]
336 * Here it is, what you've all been waiting for! When reading this,
337 * it might help to have the definition for "Inductive ND" (see
338 * NaturalDeduction.v) handy as a cross-reference.
340 Definition FlatteningFunctor_fmor {Γ}{Δ}
342 (h~~{JudgmentsL _ _ (PCF 0 Γ Δ)}~~>c) ->
343 ((obact 0 h)~~{TypesL _ _ (SystemFC Γ Δ)}~~>(obact 0 c)).
344 unfold hom; unfold ob; unfold ehom; simpl; unfold mon_i; unfold obact; intros.
348 (* the proof from no hypotheses of no conclusions (nd_id0) becomes REmptyGroup *)
349 apply nd_rule; apply org_fc; simpl. apply nd_rule. apply REmptyGroup.
351 (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
352 apply nd_rule; apply org_fc; simpl. apply nd_rule. destruct (guestJudgmentAsGArrowType h). apply RVar.
354 (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;REmptyGroup *)
355 apply nd_rule; apply org_fc; simpl.
356 eapply nd_comp; [ idtac | apply (nd_rule (RURule _ _ _ _ (RWeak _ _))) ].
357 apply nd_rule. apply REmptyGroup.
359 (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RBindingGroup;;RCont *)
360 eapply nd_comp; [ idtac | eapply nd_rule; eapply org_fc; apply (nd_rule (RURule _ _ _ _ (RCont _ _))) ].
361 eapply nd_comp; [ apply nd_llecnac | idtac ].
362 set (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ)) (mapOptionTree guestJudgmentAsGArrowType h)) as q.
367 apply nd_rule; eapply org_fc.
372 (* nd_prod becomes nd_llecnac;;nd_prod;;RBindingGroup *)
374 apply (nd_llecnac ;; nd_prod IHX1 IHX2).
375 apply nd_rule; apply org_fc; simpl.
376 eapply nd_rule. apply RBindingGroup.
378 (* nd_comp becomes pl_subst (aka nd_cut) *)
380 apply (nd_llecnac ;; nd_prod IHX1 IHX2).
381 clear IHX1 IHX2 X1 X2.
382 apply (@nd_cut _ _ _ _ _ _ (@pl_subst _ _ _ _ (SystemFC Γ Δ))).
384 (* nd_cancell becomes RVar;;RuCanL *)
386 [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RuCanL _ _)) ].
387 apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ))).
389 (* nd_cancelr becomes RVar;;RuCanR *)
391 [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RuCanR _ _)) ].
392 apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ))).
394 (* nd_llecnac becomes RVar;;RCanL *)
396 [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RCanL _ _)) ].
397 apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ))).
399 (* nd_rlecnac becomes RVar;;RCanR *)
401 [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RCanR _ _)) ].
402 apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ))).
404 (* nd_assoc becomes RVar;;RAssoc *)
406 [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RAssoc _ _ _ _)) ].
407 apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ))).
409 (* nd_coss becomes RVar;;RCossa *)
411 [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RCossa _ _ _ _)) ].
412 apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ))).
414 (* now, the interesting stuff: the inference rules of Judgments(PCF) become GArrow-parameterized terms *)
415 refine (match r as R in OrgR B N G D H C return
418 | O => if B then True
419 else ND (OrgR true 0 G D)
421 [G >> D > mapOptionTree guestJudgmentAsGArrowType H |- mapOptionTree guestJudgmentAsGArrowType C]
423 | org_pcf n Γ Δ h c b r => _
424 | org_fc n Γ Δ h c r => _
425 | org_nest n Γ Δ h c b v q => _
426 end); destruct n; try destruct b; try apply I.
430 rename r0 into r; rename h0 into h; rename c0 into c; rename Γ0 into Γ; rename Δ0 into Δ.
432 refine (match r as R in Rule_PCF _ _ H C _ with
433 | PCF_RURule h c r => let case_RURule := tt in _
434 | PCF_RLit Σ τ => let case_RLit := tt in _
435 | PCF_RNote Σ τ l n => let case_RNote := tt in _
436 | PCF_RVar σ l=> let case_RVar := tt in _
437 | PCF_RLam Σ tx te q => let case_RLam := tt in _
438 | PCF_RApp Σ tx te p l=> let case_RApp := tt in _
439 | PCF_RLet Σ σ₁ σ₂ p l=> let case_RLet := tt in _
440 | PCF_RBindingGroup b c d e => let case_RBindingGroup := tt in _
441 | PCF_REmptyGroup => let case_REmptyGroup := tt in _
442 (* | PCF_RCase T κlen κ θ l x => let case_RCase := tt in _*)
443 (* | PCF_RLetRec Σ₁ τ₁ τ₂ lev => let case_RLetRec := tt in _*)
446 rename r0 into r; rename h0 into h; rename c0 into c.
448 destruct case_RURule.
450 | RLeft a b c r => let case_RLeft := tt in _
451 | RRight a b c r => let case_RRight := tt in _
452 | RCanL a b => let case_RCanL := tt in _
453 | RCanR a b => let case_RCanR := tt in _
454 | RuCanL a b => let case_RuCanL := tt in _
455 | RuCanR a b => let case_RuCanR := tt in _
456 | RAssoc a b c d => let case_RAssoc := tt in _
457 | RCossa a b c d => let case_RCossa := tt in _
458 | RExch a b c => let case_RExch := tt in _
459 | RWeak a b => let case_RWeak := tt in _
460 | RCont a b => let case_RCont := tt in _
471 destruct case_RuCanL.
475 destruct case_RuCanR.
479 destruct case_RAssoc.
483 destruct case_RCossa.
491 destruct case_RRight.
511 (* hey cool, I figured out how to pass CoreNote's through... *)
527 (* ga_curry, but try to avoid this someday in the future if the argument type isn't a function *)
535 (* ga_comp! perhaps this means the ga_curry avoidance can be done by turning lambdas into lets? *)
538 destruct case_RBindingGroup.
539 (* ga_first+ga_second; technically this assumes a specific evaluation order, which is bad *)
542 destruct case_REmptyGroup.
547 Instance FlatteningFunctor {n}{Γ}{Δ} : Functor (JudgmentsL _ _ (PCF n Γ Δ)) (TypesL _ _ (SystemFCa n Γ Δ)) obact :=
548 { fmor := FlatteningFunctor_fmor }.
549 unfold hom; unfold ob; unfold ehom; intros; simpl.
552 Definition productifyType {Γ} (lt:Tree ??(LeveledHaskType Γ ★)) : LeveledHaskType Γ ★.
556 Definition exponent {Γ} : LeveledHaskType Γ ★ -> LeveledHaskType Γ ★ -> LeveledHaskType Γ ★.
560 Definition brakify {Γ}(Σ τ:Tree ??(LeveledHaskType Γ ★)) := exponent (productifyType Σ) (productifyType τ).
562 Definition brakifyJudg (j:Judg) : Judg :=
565 Γ > Δ > [] |- [brakify Σ τ]
568 Definition brakifyUJudg (j:Judg) : Judg :=
571 Γ > Δ > [] |- [brakify Σ τ]
577 Context (ndr_pcf :forall n Γ Δ, @ND_Relation _ (@RulePCF Γ Δ n)).
580 Instance PCF n Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) (@RulePCF Γ Δ n) :=
582 ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
583 ; pl_sc := _ (*@SequentCalculus Judg Rule _ sequent*)
584 ; pl_subst := _ (*@CutRule Judg Rule _ sequent pl_eqv pl_sc*)
585 ; pl_sequent_join := _ (*@SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst*)
589 Inductive RuleX : nat -> Tree ??Judg -> Tree ??Judg -> Type :=
590 | x_flat : forall n h c (r:Rule h c), Rule_Flat r -> RuleX n h c
591 | x_nest : forall n Γ Δ h c, ND (@RulePCF Γ Δ n) h c ->
592 RuleX (S n) (mapOptionTree brakifyJudg h) (mapOptionTree brakifyJudg c).
597 Context (ndr:@ND_Relation _ (RuleX (S n))).
599 Definition SystemFCa' := Judgments_Category ndr.
601 Definition ReificationFunctor_fmor Γ Δ
603 (h~~{JudgmentsL _ _ (PCF n Γ Δ)}~~>c) ->
604 ((mapOptionTree brakifyJudg h)~~{SystemFCa'}~~>(mapOptionTree brakifyJudg c)).
605 unfold hom; unfold ob; simpl.
612 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
613 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
614 unfold ReificationFunctor_fmor; simpl.
616 unfold ReificationFunctor_fmor; simpl.
618 unfold ReificationFunctor_fmor; simpl.
622 Definition FlatteningFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakify).
623 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
624 unfold ReificationFunctor_fmor; simpl.
626 unfold ReificationFunctor_fmor; simpl.
628 unfold ReificationFunctor_fmor; simpl.
632 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
633 refine {| plsmme_pl := PCF n Γ Δ |}.
637 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
638 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
642 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
647 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
649 (* ... and the retraction exists *)
652 (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so
653 * it falls within (SystemFCa n) for some n. This function calculates that "n" and performs the translation *)
655 Definition HaskProof_to_SystemFCa :
656 forall h c (pf:ND Rule h c),
657 { n:nat & h ~~{JudgmentsL (SystemFCa_SMME n)}~~> c }.
660 (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
663 Definition makeTree : Tree ??(LeveledHaskType Γ ★) -> HaskType Γ ★.
667 Definition flattenType n (j:JudgmentsN n) : TypesN n.
670 refine (mapOptionTree _ j).
672 destruct j as [ Γ' Δ' Σ τ ].
673 assert (Γ'=Γ). admit.
677 refine (HaskBrak _ ( (makeTree Σ) ---> (makeTree τ) )); intros.
681 Definition FlattenFunctor_fmor n :
683 (h~~{JudgmentsN n}~~>c) ->
684 ((flattenType n h)~~{TypesN n}~~>(flattenType n c)).
686 unfold hom in *; simpl.
694 Definition FlattenFunctor n : Functor (JudgmentsN n) (TypesN n) (flattenType n).
695 refine {| fmor := FlattenFunctor_fmor n |}; intros.
702 Implicit Arguments Rule_PCF [ [h] [c] ].
703 Implicit Arguments BoundedRule [ ].
707 Definition code2garrow0 {Γ}(ec t1 t2:RawHaskType Γ ★) : RawHaskType Γ ★.
710 Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
712 (* | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx t'*)
713 | _ => code2garrow0 ec unitType t
716 Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
717 match ty as TY in RawHaskType _ K return RawHaskType TV K with
718 | TCode ec t => code2garrow _ ec t
719 | TApp _ _ t1 t2 => TApp (typeMap t1) (typeMap t2)
720 | TAll _ f => TAll _ (fun tv => typeMap (f tv))
721 | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
725 | TyFunApp tf rhtl => (* FIXME *) TyFunApp tf rhtl
728 Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
730 (* | t @@ nil => (fun TV ite => typeMap (t TV ite)) @@ lev*)
731 | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
734 Definition coMap {Γ}(ck:HaskCoercionKind Γ) :=
735 fun TV ite => match ck TV ite with
736 | mkRawCoercionKind _ t1 t2 => mkRawCoercionKind _ (typeMap t1) (typeMap t2)
739 Definition flattenCoercion {Γ}{Δ}{ck}(hk:HaskCoercion Γ Δ ck) : HaskCoercion Γ (map coMap Δ) (coMap ck).
743 Lemma update_typeMap Γ (lev:HaskLevel Γ) ξ v t
744 : (typeMap ○ (update_ξ ξ lev ((⟨v, t ⟩) :: nil)))
745 = ( update_ξ (typeMap ○ ξ) lev ((⟨v, typeMap_ t ⟩) :: nil)).
749 Lemma foo κ Γ σ τ : typeMap_ (substT σ τ) = substT(Γ:=Γ)(κ₁:=κ) (fun TV ite => typeMap ○ σ TV ite) τ.
753 Lemma lit_lemma lit Γ : typeMap_ (literalType lit) = literalType(Γ:=Γ) lit.
758 Definition flatten : forall h c, Rule h c -> @ND Judg Rule (mapOptionTree flattenJudgment h) (mapOptionTree flattenJudgment c).
760 refine (match r as R in Rule H C return ND Rule (mapOptionTree flattenJudgment H) (mapOptionTree flattenJudgment C) with
761 | RURule a b c d e => let case_RURule := tt in _
762 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
763 | RLit Γ Δ l _ => let case_RLit := tt in _
764 | RVar Γ Δ σ p => let case_RVar := tt in _
765 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
766 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
767 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
768 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
769 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
770 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
771 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
772 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
773 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
774 | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
775 | REmptyGroup _ _ => let case_REmptyGroup := tt in _
776 | RBrak Σ a b c n m => let case_RBrak := tt in _
777 | REsc Σ a b c n m => let case_REsc := tt in _
778 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
779 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
782 destruct case_RURule.
794 eapply nd_rule. simpl. apply RNote; auto.
799 set (@RNote Γ Δ Σ τ l) as q.
802 Definition flatten' {h}{c} (pf:ND Rule h c) := nd_map' flattenJudgment flatten pf.
805 @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
807 refine (fix flatten : forall Γ Δ Σ τ
808 (pf:SCND Rule [] [Γ > Δ > Σ |- τ ]) :
809 SCND Rule [] [Γ > Δ > mapOptionTree typeMap Σ |- mapOptionTree typeMap τ ] :=
811 | scnd_comp : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c]
812 | scnd_weak : forall c , SCND c []
813 | scnd_leaf : forall ht c , SCND ht [c] -> SCND ht [c]
814 | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2)
815 Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
819 Lemma all_lemma Γ κ σ l :
821 (@HaskTApp (κ :: Γ) κ (@weakF Γ κ ★ σ) (@FreshHaskTyVar Γ κ) @@
822 @weakL Γ κ l)) = (@typeMap Γ (@HaskTAll Γ κ σ @@ l)).
826 Definition flatten : forall Γ Δ ξ τ, Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
827 refine (fix flatten Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') : Expr Γ' (map coMap Δ') (typeMap ○ ξ') (typeMap τ') :=
828 match exp as E in Expr G D X T return Expr G (map coMap D) (typeMap ○ X) (typeMap T) with
829 | EGlobal Γ Δ ξ t wev => EGlobal _ _ _ _ wev
830 | EVar Γ Δ ξ ev => EVar _ _ _ ev
831 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
832 | EApp Γ Δ ξ t1 t2 lev e1 e2 => EApp _ _ _ _ _ _ (flatten _ _ _ _ e1) (flatten _ _ _ _ e2)
833 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in _
834 | ELet Γ Δ ξ tv t l ev elet ebody => let case_ELet := tt in _
835 | ELetRec Γ Δ ξ lev t tree branches ebody => let case_ELetRec := tt in _
836 | ECast Γ Δ ξ t1 t2 γ lev e => let case_ECast := tt in _
837 | ENote Γ Δ ξ t n e => ENote _ _ _ _ n (flatten _ _ _ _ e)
838 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in _
839 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in _
840 | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => let case_ECoApp := tt in _
841 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in _
842 | ECase Γ Δ ξ l tc tbranches atypes e alts' => let case_ECase := tt in _
844 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in _
845 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in _
846 end); clear exp ξ' τ' Γ' Δ'.
854 set (flatten _ _ _ _ e) as q.
855 rewrite update_typeMap in q.
856 apply (@ELam _ _ _ _ _ _ _ _ v q).
859 set (flatten _ _ _ _ ebody) as ebody'.
860 set (flatten _ _ _ _ elet) as elet'.
861 rewrite update_typeMap in ebody'.
862 apply (@ELet _ _ _ _ _ _ _ _ _ elet' ebody').
873 apply flattenCoercion in γ.
876 destruct case_ETyApp.
879 unfold HaskTAll in e.
880 unfold typeMap_ in e.
886 destruct case_ECoLam.
889 set (@ECoLam _ _ _ _ _ _ _ _ _ _ e) as x.
896 destruct case_ECoApp.
900 unfold mkHaskCoercionKind in *.
902 apply flattenCoercion in γ.
903 unfold coMap in γ at 2.
907 destruct case_ETyLam.
909 set (@ETyLam Unique _ Γ (map coMap Δ) (typeMap ○ ξ) κ (fun ite x => typeMap (σ x ite))) as e'.
910 unfold HaskTAll in *.
911 unfold typeMap_ in *.
912 rewrite <- foo in e'.
913 unfold typeMap in e'.
917 Set Printing Implicit.
927 destruct case_ELetRec.
931 (* This proof will work for any dynamic semantics you like, so
932 * long as those semantics are an ND_Relation (associativity,
933 * neutrality, etc) *)
934 Context (dynamic_semantics : @ND_Relation _ Rule).
936 Section SystemFC_Category.
941 Definition Context := Tree ??(LeveledHaskType Γ ★).
943 Notation "a |= b" := (Γ >> Δ > a |- b).
949 SystemFCa_initial_GArrow
952 Context (nd_eqv:@ND_Relation _ (@URule Γ Δ)).
953 Check (@ProgrammingLanguage).
954 Context (PL:@ProgrammingLanguage (LeveledHaskType Γ ★)
955 (fun x y => match x with x1|=x2 => match y with y1|=y2 => @URule Γ Δ)).
956 Definition JudgmentsFC := @Judgments_Category_CartesianCat _ (@URule Γ Δ) nd_eqv.
957 Definition TypesFC := @TypesL _ (@URule Γ Δ) nd_eqv.
959 (* The full subcategory of SystemFC(Γ,Δ) consisting only of judgments involving types at a fixed level. Note that
960 * code types are still permitted! *)
962 Context (lev:HaskLevel Γ).
964 Inductive ContextAtLevel : Context -> Prop :=
965 | contextAtLevel_nil : ContextAtLevel []
966 | contextAtLevel_leaf : forall τ, ContextAtLevel [τ @@ lev]
967 | contextAtLevel_branch : forall b1 b2, ContextAtLevel b1 -> ContextAtLevel b2 -> ContextAtLevel (b1,,b2).
969 Inductive JudgmentsAtLevel : JudgmentsFC -> Prop :=
970 | judgmentsAtLevel_nil : JudgmentsAtLevel []
971 | judgmentsAtLevel_leaf : forall c1 c2, ContextAtLevel c1 -> ContextAtLevel c2 -> JudgmentsAtLevel [c1 |= c2]
972 | judgmentsAtLevel_branch : forall j1 j2, JudgmentsAtLevel j1 -> JudgmentsAtLevel j2 -> JudgmentsAtLevel (j1,,j2).
974 Definition JudgmentsFCAtLevel := FullSubcategory JudgmentsFC JudgmentsAtLevel.
975 Definition TypesFCAtLevel := FullSubcategory TypesFC ContextAtLevel.
978 End SystemFC_Category.
980 Implicit Arguments TypesFC [ ].
983 Section EscBrak_Functor.
987 (Σ₁:Tree ??(@LeveledHaskType V)).
989 Definition EscBrak_Functor_Fobj
990 : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past
991 := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
992 let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])).
995 Definition EscBrak_Functor_Fmor
996 : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b),
997 (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b).
1007 Lemma esc_then_brak_is_id : forall a,
1008 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak)
1009 (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))).
1013 Lemma brak_then_esc_is_id : forall a,
1014 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc)
1015 (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)).
1019 Instance EscBrak_Functor
1020 : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj :=
1021 { fmor := fun a b f => EscBrak_Functor_Fmor a b f }.
1022 intros; unfold EscBrak_Functor_Fmor; simpl in *.
1023 apply ndr_comp_respects; try reflexivity.
1024 apply ndr_comp_respects; try reflexivity.
1026 intros; unfold EscBrak_Functor_Fmor; simpl in *.
1027 set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
1029 apply esc_then_brak_is_id.
1030 intros; unfold EscBrak_Functor_Fmor; simpl in *.
1031 set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q.
1032 repeat setoid_rewrite q.
1033 apply ndr_comp_respects; try reflexivity.
1034 apply ndr_comp_respects; try reflexivity.
1035 repeat setoid_rewrite <- q.
1036 apply ndr_comp_respects; try reflexivity.
1037 setoid_rewrite brak_then_esc_is_id.
1039 set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
1044 End EscBrak_Functor.
1048 Ltac rule_helper_tactic' :=
1050 | [ H : ?A = ?A |- _ ] => clear H
1051 | [ H : [?A] = [] |- _ ] => inversion H; clear H
1052 | [ H : [] = [?A] |- _ ] => inversion H; clear H
1053 | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H
1054 | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H
1055 | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H
1056 | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H
1057 | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H
1058 | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H
1059 (* | [ H : Sequent T |- _ ] => destruct H *)
1060 (* | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*)
1061 | [ H : [?A] = [?B] |- _ ] => inversion H; clear H
1062 | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst
1063 | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl
1064 | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H
1067 Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
1071 Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
1075 Definition append_brak_to_id : forall {c},
1077 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )
1078 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
1082 Definition append_brak : forall {h c}
1085 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )),
1088 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
1090 refine (fix append_brak h c nd {struct nd} :=
1096 (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) ->
1097 ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
1099 | nd_id0 => let case_nd_id0 := tt in _
1100 | nd_id1 h => let case_nd_id1 := tt in _
1101 | nd_weak h => let case_nd_weak := tt in _
1102 | nd_copy h => let case_nd_copy := tt in _
1103 | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
1104 | nd_comp _ _ _ top bot => let case_nd_comp := tt in _
1105 | nd_rule _ _ rule => let case_nd_rule := tt in _
1106 | nd_cancell _ => let case_nd_cancell := tt in _
1107 | nd_cancelr _ => let case_nd_cancelr := tt in _
1108 | nd_llecnac _ => let case_nd_llecnac := tt in _
1109 | nd_rlecnac _ => let case_nd_rlecnac := tt in _
1110 | nd_assoc _ _ _ => let case_nd_assoc := tt in _
1111 | nd_cossa _ _ _ => let case_nd_cossa := tt in _
1112 end) (refl_equal _) (refl_equal _)
1114 simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *.
1115 destruct case_nd_id0. apply nd_id0.
1116 destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak.
1117 destruct case_nd_weak. apply nd_weak.
1119 destruct case_nd_copy.
1121 destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
1122 inversion H0; subst.
1128 destruct case_nd_prod.
1130 apply (append_brak _ _ lpf).
1131 apply (append_brak _ _ rpf).
1133 destruct case_nd_comp.
1134 apply append_brak in bot.
1135 apply (nd_comp top bot).
1137 destruct case_nd_cancell.
1138 eapply nd_comp; [ apply nd_cancell | idtac ].
1139 apply append_brak_to_id.
1141 destruct case_nd_cancelr.
1142 eapply nd_comp; [ apply nd_cancelr | idtac ].
1143 apply append_brak_to_id.
1145 destruct case_nd_llecnac.
1146 eapply nd_comp; [ idtac | apply nd_llecnac ].
1147 apply append_brak_to_id.
1149 destruct case_nd_rlecnac.
1150 eapply nd_comp; [ idtac | apply nd_rlecnac ].
1151 apply append_brak_to_id.
1153 destruct case_nd_assoc.
1154 eapply nd_comp; [ apply nd_assoc | idtac ].
1155 repeat rewrite fixit.
1156 apply append_brak_to_id.
1158 destruct case_nd_cossa.
1159 eapply nd_comp; [ idtac | apply nd_cossa ].
1160 repeat rewrite fixit.
1161 apply append_brak_to_id.
1163 destruct case_nd_rule
1169 Definition append_brak {h c} : forall
1171 (fixify Γ ((⟨n, Σ₁ ⟩) :: past) h )
1174 (fixify Γ past (EscBrak_Functor_Fobj h))
1180 End HaskProofCategory.