proposition: Proposition mor_from_HSET_coend_eq (X : hSet) (f g : HSET_coend → X) (x : HSET_coend) (p : ∏ (y : C) (h : F y y), f (HSET_coend_in y h) = g (HSET_coend_in y h)) : f x = g x.
proof: Proof. use (eqtohomot (mor_to_coend_eq F (pr2 HSET_coend_colimit) X _)). intro y. use funextsec. intro h. apply p. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Univalence UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Profunctors.Core UniMath.CategoryTheory.Limits.Coends UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Coequalizers