fix proof that Judgments(L) is Cartesian

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 5cf67db..855b66a 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (submodule)
--- a/src/categories
+++ b/src/categories
@@ -1 +1 @@
-Subproject commit 77fb38900253b1bc9c4552d474f8564fda398d09
+Subproject commit 06467b1762fe54767eb1d64e7b7f1798eea8cc27