Lemma binproduct_nat_trans_univ_prop (A : [C, D]) (f : A --> (F:[C,D])) (g : A --> (G:[C,D])) : ∏ t : ∑ fg : A --> (BinProduct_of_functors:[C,D]), fg · (binproduct_nat_trans_pr1 : (BinProduct_of_functors:[C,D]) --> F) = f × fg · (binproduct_nat_trans_pr2 : (BinProduct_of_functors:[C,D]) --> G) = g, t = tpair (λ fg : A --> (BinProduct_of_functors:[C,D]), fg · (binproduct_nat_trans_pr1 : (BinProduct_of_functors:[C,D]) --> F) = f × fg · (binproduct_nat_trans_pr2 : (BinProduct_of_functors:[C,D]) --> G) = g) (binproduct_nat_trans A f g) (make_dirprod (binproduct_nat_trans_Pr1Commutes A f g) (binproduct_nat_trans_Pr2Commutes A f g)). Proof. intro t. simpl in *. destruct t as [t1 [ta tb]]. simpl in *. apply subtypePath. - intro. simpl. apply isapropdirprod; apply isaset_nat_trans; apply D. - simpl. apply nat_trans_eq. + apply D. + intro c. unfold binproduct_nat_trans. simpl. unfold binproduct_nat_trans_data. apply BinProductArrowUnique. * apply (nat_trans_eq_pointwise ta). * apply (nat_trans_eq_pointwise tb). Qed.
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.