- (* 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,,[] )]
- }.
+ Instance Judgments_Category_Terminal : Terminal Judgments_Category.
+ refine {| one := [] ; drop := nd_weak' ; drop_unique := _ |}.
+ abstract (intros; unfold eqv; simpl; apply ndr_void_proofs_irrelevant).
+ Defined.
+
+ Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal.
+ 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.
+ refine {| car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal
+ ; car_one := iso_id [] |}
+ ; intros; unfold hom; simpl
+ ; unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl.
+
+ apply ndr_structural_indistinguishable; auto.
+ apply nd_structural_comp; auto.
+ apply nd_structural_comp; auto.
+ unfold copy; simpl; apply nd_structural_copy; auto.
+ apply nd_structural_prod; auto.
+ apply nd_structural_comp; auto.
+ apply weak'_structural.
+ apply nd_structural_id0; auto.
+ apply nd_structural_cancell; auto.
+
+ apply ndr_structural_indistinguishable; auto.
+ apply nd_structural_comp; auto.
+ apply nd_structural_comp; auto.
+ unfold copy; simpl; apply nd_structural_copy; auto.
+ apply nd_structural_prod; auto.
+ apply nd_structural_comp; auto.
+ apply weak'_structural.
+ apply nd_structural_id0; auto.
+ apply nd_structural_cancelr; auto.
+ Defined.