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

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"