setoid_rewrite <- ndr_prod_preserves_comp.
apply (ndr_builtfrom_structural (f;;g)); auto.
Defined.
- Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (fun x y => x,,y) :=
+ Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (@T_Branch (??Judgment)) :=
{ bin_first := jud_first
; bin_second := jud_second }.
; pmon_assoc_ll := jud_mon_assoc_ll
}.
unfold functor_fobj; unfold fmor; simpl;
- apply Build_Pentagon; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto.
+ apply Build_Pentagon; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto 10.
unfold functor_fobj; unfold fmor; simpl;
- apply Build_Triangle; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto.
+ apply Build_Triangle; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto 10.
intros; unfold eqv; simpl; auto; reflexivity.
intros; unfold eqv; simpl; auto; reflexivity.
intros; unfold eqv; simpl; apply Judgments_Category_Commutative.