proposition: Lemma Coproducts_from_Colims : Colims_of_shape I_graph C -> Coproducts I C.
proof: Proof. intros H F. set (HF := H (coproducts_diagram F)). use make_Coproduct. + apply (colim HF). + intros i; apply (colimIn HF). + apply (make_isCoproduct _ _ C); intros c Fic. use unique_exists. - now apply colimArrow, Coproducts_cocone. - abstract (simpl; intro i; apply (colimArrowCommutes HF)). - abstract (intros y; apply impred; intro i; apply C). - abstract (intros f Hf; apply colimArrowUnique; simpl in *; intros i; apply Hf). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.whiskering