+ abstract
+ (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl;
+ apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto).
+ abstract
+ (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl;
+ apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto).
+ Defined.
+
+ 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.
+ apply Build_DiagonalCat.
+ intros; unfold bin_obj; simpl; unfold hom; simpl; apply nd_copy.
+ 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.
+ 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.
+ 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.