Definition precategory_binproduct_data (C D : precategory_data) : precategory_data. Proof. exists (precategory_binproduct_ob_mor C D). split. - intro cd. exact (make_dirprod (identity (pr1 cd)) (identity (pr2 cd))). - intros cd cd' cd'' fg fg'. exact (make_dirprod (pr1 fg · pr1 fg') (pr2 fg · pr2 fg')). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.opp_precat.