-
- 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"
- * 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_premonoidal : PreMonoidalCat Judgments_Category_binoidal [] :=
+ { pmon_cancelr := jud_mon_cancelr
+ ; pmon_cancell := jud_mon_cancell
+ ; pmon_assoc := jud_mon_assoc
+ ; pmon_assoc_rr := jud_mon_assoc_rr
+ ; pmon_assoc_ll := jud_mon_assoc_ll