Definition isCoproduct_from_colims : isCoproduct I C f x fs. Proof. intros y gs. use iscontraprop1. - apply isCoproduct_from_colims_unique. - simple refine (_ ,, _). + use colimArrow. use make_cocone. * exact gs. * intros u v F. induction F. + intro i. exact (colimArrowCommutes L _ _ i). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Coproducts. Section CoproductsFromColims. Section CoproductsFromColim. End CoproductsFromColim. End CoproductsFromColims.