X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeductionCategory.v;h=ef3119f11f7e48901c003837411f19be797b02d7;hp=23ddb566cf26bcbe39602898d03c1155691c21ec;hb=85e4f0fd6b0673c1cc763eeb2585b7dc3d388455;hpb=70939a4eb9560ceeea3e9cf176ac5a36f9201ac4

diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v
index 23ddb56..ef3119f 100644
--- a/src/NaturalDeductionCategory.v
+++ b/src/NaturalDeductionCategory.v
@@ -154,6 +154,10 @@ Section Judgments_Category.
     apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto.
     Defined.
 
+  Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal.
+    admit.
+    Defined.
+
   (* Given some mapping "rep" that turns a (Tree ??T) intoto Judgment,
    * this asserts that we have sensible structural rules with respect
    * to that mapping.  Doing all of this "with respect to a mapping"