proposition: Proposition isCoproduct_from_colims_unique {y : C} (gs : ∏ (i : I), f i --> y) : isaprop (∑ g, ∏ (i : I), fs i · g = gs i).
proof: Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. use impred ; intro. apply homset_property. } use colimArrowUnique' ; cbn. intro i. exact (pr2 φ₁ i @ !(pr2 φ₂ i)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Coproducts