proposition: Lemma coproduct_nat_trans_univ_prop (A : [C, D]) (f : (F : [C,D]) --> A) (g : (G : [C,D]) --> A) : ∏ t : ∑ fg : (BinCoproduct_of_functors:[C,D]) --> A, (coproduct_nat_trans_in1 : (F:[C,D]) --> BinCoproduct_of_functors)· fg = f × (coproduct_nat_trans_in2: (G : [C,D]) --> BinCoproduct_of_functors)· fg = g, t = tpair (λ fg : (BinCoproduct_of_functors:[C,D]) --> A, (coproduct_nat_trans_in1 : (F:[C,D]) --> BinCoproduct_of_functors)· fg = f × (coproduct_nat_trans_in2 : (G:[C,D]) --> BinCoproduct_of_functors) · fg = g) (coproduct_nat_trans A f g) (make_dirprod (coproduct_nat_trans_In1Commutes A f g) (coproduct_nat_trans_In2Commutes A f g)).
proof: Proof. intro t. simpl in *. destruct t as [t1 [ta tb]]. simpl in *. apply subtypePath. - intro. apply isapropdirprod; apply isaset_nat_trans; apply D. - simpl. apply nat_trans_eq. + apply D. + intro c. unfold coproduct_nat_trans. simpl. unfold coproduct_nat_trans_data. simpl. apply BinCoproductArrowUnique. * 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.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.ProductCategory