From 8cb97991a95d5761a28ca94767b8fe637d1411d9 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 19:18:09 -0700 Subject: [PATCH] fix proof that Judgments(L) is Cartesian --- src/NaturalDeduction.v | 3 +++ src/NaturalDeductionCategory.v | 14 ++++++++++---- src/ProgrammingLanguage.v | 8 ++++---- src/categories | 2 +- 4 files changed, 18 insertions(+), 9 deletions(-) diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index 5cf67db..855b66a 100644 --- a/src/NaturalDeduction.v +++ b/src/NaturalDeduction.v @@ -227,6 +227,9 @@ Section Natural_Deduction. (* products and composition must distribute over each other *) ; ndr_prod_preserves_comp : forall `(f:a/⋯⋯/b)`(f':a'/⋯⋯/b')`(g:b/⋯⋯/c)`(g':b'/⋯⋯/c'), (f;;g)**(f';;g') === (f**f');;(g**g') + (* products and duplication must distribute over each other *) + ; ndr_prod_preserves_copy : forall `(f:a/⋯⋯/b), nd_copy a;; f**f === f ;; nd_copy b + (* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *) ; ndr_structural_indistinguishable : forall `(f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v index 1bd8bf2..5e3432b 100644 --- a/src/NaturalDeductionCategory.v +++ b/src/NaturalDeductionCategory.v @@ -164,8 +164,14 @@ Section Judgments_Category. Defined. Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal. - apply Build_DiagonalCat. - intros; unfold bin_obj; simpl; unfold hom; simpl; apply nd_copy. + refine {| copy_nt := _ |}. + intros. + refine {| nt_component := nd_copy |}. + intros. + unfold hom in *; unfold ob in *; unfold eqv. + simpl. + rewrite ndr_prod_preserves_copy; auto. + reflexivity. Defined. Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal. @@ -177,7 +183,7 @@ Section Judgments_Category. apply ndr_structural_indistinguishable; auto. apply nd_structural_comp; auto. apply nd_structural_comp; auto. - apply nd_structural_copy; auto. + unfold copy; simpl; apply nd_structural_copy; auto. apply nd_structural_prod; auto. apply nd_structural_comp; auto. apply weak'_structural. @@ -187,7 +193,7 @@ Section Judgments_Category. apply ndr_structural_indistinguishable; auto. apply nd_structural_comp; auto. apply nd_structural_comp; auto. - apply nd_structural_copy; auto. + unfold copy; simpl; apply nd_structural_copy; auto. apply nd_structural_prod; auto. apply nd_structural_comp; auto. apply weak'_structural. diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index d1a0875..b00d1ad 100644 --- a/src/ProgrammingLanguage.v +++ b/src/ProgrammingLanguage.v @@ -248,11 +248,11 @@ Section Programming_Language. apply al_subst_associativity'. Defined. - Definition TypesLEnrichedInJudgments0 : Enrichment. + Definition TypesEnrichedInJudgments : Enrichment. refine {| enr_c := TypesLFC |}. Defined. - Definition TypesL_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ). + Definition Types_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ). (* eapply Build_EFunctor; intros. eapply MonoidalCat_all_central. @@ -262,11 +262,11 @@ Section Programming_Language. admit. Defined. - Definition TypesL_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ). + Definition Types_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ). admit. Defined. - Definition TypesL_binoidal : BinoidalCat TypesLFC (@T_Branch _). + Definition Types_binoidal : BinoidalCat TypesLFC (@T_Branch _). refine {| bin_first := TypesL_first ; bin_second := TypesL_second diff --git a/src/categories b/src/categories index 77fb389..06467b1 160000 --- a/src/categories +++ b/src/categories @@ -1 +1 @@ -Subproject commit 77fb38900253b1bc9c4552d474f8564fda398d09 +Subproject commit 06467b1762fe54767eb1d64e7b7f1798eea8cc27 -- 1.7.10.4