X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeductionCategory.v;h=0a413e75ff8ccb8c7588e6a10790a5db62705d3e;hp=b64ac4ba9f91e3cb10b37aa7025ae55f339d8208;hb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f;hpb=b096aab78240e38ff69c120367e65be60cbc54f5

diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v
index b64ac4b..0a413e7 100644
--- a/src/NaturalDeductionCategory.v
+++ b/src/NaturalDeductionCategory.v
@@ -36,6 +36,7 @@ Section Judgments_Category.
 
   Notation "pf1 === pf2" := (@ndr_eqv _ _ nd_eqv _ _ pf1 pf2).
 
+  (* there is a category whose objects are judgments and whose morphisms are proofs *)
   Instance Judgments_Category : Category (Tree ??Judgment) (fun h c => h /⋯⋯/ c) :=
   { id   := fun h          => nd_id _
   ; comp := fun a b c f g  => f ;; g
@@ -51,6 +52,7 @@ Section Judgments_Category.
   intros; apply ndr_comp_associativity.
   Defined.
 
+  (* it is monoidal, with the judgment-tree-formation operator as its tensor *)
   Definition Judgments_Category_monoidal_endofunctor_fobj : Judgments_Category ×× Judgments_Category -> Judgments_Category :=
     fun xy => (fst_obj _ _ xy),,(snd_obj _ _ xy).
   Definition Judgments_Category_monoidal_endofunctor_fmor :
@@ -201,9 +203,6 @@ Section Judgments_Category.
     apply nd_structural_cancelr; auto.
     Defined.
 
-
-  (* Structure ExpressionAlgebra (sig:Signature) := *)
-
 End Judgments_Category.
 
 Close Scope pf_scope.