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. 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.
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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.ProductCategory.