+ 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
+ }.
+ unfold functor_fobj; unfold fmor; simpl;
+ apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto.
+
+ unfold functor_fobj; unfold fmor; simpl;
+ apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto.
+
+ intros; unfold eqv; simpl; auto.
+
+ intros; unfold eqv; simpl; auto.
+
+ intros; unfold eqv; simpl.
+ apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ apply ndr_prod_respects; try reflexivity.
+ apply ndr_structural_indistinguishable; auto.
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ apply ndr_prod_respects; try reflexivity.
+ apply ndr_structural_indistinguishable; auto.
+
+ intros; unfold eqv; simpl.
+ apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ apply ndr_prod_respects; try reflexivity.
+ apply ndr_structural_indistinguishable; auto.
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ apply ndr_prod_respects; try reflexivity.
+ apply ndr_structural_indistinguishable; auto.
+
+ intros; unfold eqv; simpl.
+ apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ apply ndr_prod_respects; try reflexivity.
+ apply ndr_structural_indistinguishable; auto.
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ symmetry.
+ etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ apply ndr_prod_respects; try reflexivity.
+ apply ndr_structural_indistinguishable; auto.
+
+ Defined.
+
+ Instance Judgments_Category_monoidal : MonoidalCat Judgments_Category_premonoidal.
+ apply Build_MonoidalCat.
+ apply Build_CommutativeCat.
+ intros; apply Build_CentralMorphism; intros; unfold eqv; simpl in *.
+
+ setoid_rewrite <- (ndr_prod_preserves_comp (nd_id a) g f (nd_id d)).
+ setoid_rewrite <- (ndr_prod_preserves_comp f (nd_id _) (nd_id _) g).
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ reflexivity.
+
+ setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) f g (nd_id _)).
+ setoid_rewrite <- (ndr_prod_preserves_comp g (nd_id _) (nd_id _) f).
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ reflexivity.
+ Defined.
+
+ Instance Judgments_Category_Terminal : TerminalObject Judgments_Category [].
+ refine {| drop := nd_weak' ; drop_unique := _ |}.