Definition functor_precat_binproduct_cone : BinProduct [C, D] F G. Proof. use make_BinProduct. - apply BinProduct_of_functors. - apply binproduct_nat_trans_pr1. - apply binproduct_nat_trans_pr2. - use make_isBinProduct. + intros A f g. exists (tpair _ (binproduct_nat_trans A f g) (make_dirprod (binproduct_nat_trans_Pr1Commutes _ _ _ ) (binproduct_nat_trans_Pr2Commutes _ _ _ ))). apply binproduct_nat_trans_univ_prop. 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.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.Combinatorics.StandardFiniteSets. Section BinProductFromIso. End BinProductFromIso. Section BinProductsFromProducts. End BinProductsFromProducts. Section ProductsFromBinProducts. End ProductsFromBinProducts.