Proposition isCoproduct_from_colims_unique {y : C} (gs : ∏ (i : I), f i --> y) : isaprop (∑ g, ∏ (i : I), fs i · g = gs i). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. use impred ; intro. apply homset_property. } use colimArrowUnique' ; cbn. intro i. exact (pr2 φ₁ i @ !(pr2 φ₂ i)). Qed.
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.