lots of cleanup

[coq-hetmet.git] / src / NaturalDeductionCategory.v

diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v
index 1bd8bf2..0a413e7 100644 (file)
--- 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 :
@@ -164,8 +166,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 +185,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 +195,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.
@@ -195,44 +203,6 @@ Section Judgments_Category.
     apply nd_structural_cancelr; auto.
     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"
-   * lets us avoid duplicating code for both the antecedent and
-   * succedent of sequent deductions. *)
-  Class TreeStructuralRules  {T:Type}(rep:Tree ??T -> Judgment) :=
-  { tsr_eqv           : @ND_Relation Judgment Rule where "pf1 === pf2" := (@ndr_eqv _ _ tsr_eqv _ _ pf1 pf2)
-  ; tsr_ant_assoc     : forall {a b c}, Rule [rep ((a,,b),,c)]     [rep ((a,,(b,,c)))]
-  ; tsr_ant_cossa     : forall {a b c}, Rule [rep (a,,(b,,c))]     [rep (((a,,b),,c))]
-  ; tsr_ant_cancell   : forall {a    }, Rule [rep (  [],,a  )]     [rep (        a  )]
-  ; tsr_ant_cancelr   : forall {a    }, Rule [rep (a,,[]    )]     [rep (        a  )]
-  ; tsr_ant_llecnac   : forall {a    }, Rule [rep (      a  )]     [rep (  [],,a    )]
-  ; tsr_ant_rlecnac   : forall {a    }, Rule [rep (      a  )]     [rep (  a,,[]    )]
-  }.
-
-  Section Sequents.
-    Context {S:Type}.   (* type of sequent components *)
-    Context (sequent:S->S->Judgment).
-    Notation "a |= b" := (sequent a b).
-
-    Class SequentCalculus :=
-    { nd_seq_reflexive : forall a, ND Rule [ ] [ a |= a ]
-    }.
-    
-    Class CutRule :=
-    { nd_cutrule_seq       :> SequentCalculus
-    ; nd_cut               :  forall a b c,  [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
-    ; nd_cut_associativity :  forall {a b c d},
-      ((nd_cut a b c) ** (nd_id1 (c|=d))) ;; (nd_cut a c d)
-        ===
-        nd_assoc ;; ((nd_id1 (a|=b)) ** (nd_cut b c d) ;; (nd_cut a b d))
-    ; nd_cut_left_identity  : forall a b, ((    (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell
-    ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a)    );; nd_cut b _ _) === nd_cancelr
-    }.
-  End Sequents.
-
-  (* Structure ExpressionAlgebra (sig:Signature) := *)
-
 End Judgments_Category.
 
 Close Scope pf_scope.