Lemma Coproducts_from_Colims : Colims_of_shape I_graph C -> Coproducts I C. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.whiskering.