proposition: Theorem Coproducts_from_Colims : Coproducts I C.
proof: Proof. intros f. exact (make_Coproduct _ _ _ _ _ (isCoproduct_from_colims f)). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Coproducts