proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monics UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.FunctorCategory UniMath.Combinatorics.StandardFiniteSets