∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {B : C} {α : Type u_3} (X : α → C)
  (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (π : (a : α) → X a ⟶ B)
  [inst_1 : CategoryTheory.EffectiveEpiFamily X π] {W : C} (e : c.pt ⟶ W),
  (∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt),
      CategoryTheory.CategoryStruct.comp g₁ (hc.desc (CategoryTheory.Limits.Cofan.mk B π)) =
          CategoryTheory.CategoryStruct.comp g₂ (hc.desc (CategoryTheory.Limits.Cofan.mk B π)) →
        CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) →
    ∀ (m : (CategoryTheory.Limits.Cofan.mk B π).pt ⟶ W)
      (hm : CategoryTheory.CategoryStruct.comp (hc.desc (CategoryTheory.Limits.Cofan.mk B π)) m = e),
      m =
        CategoryTheory.EffectiveEpiFamily.desc X π (fun a => CategoryTheory.CategoryStruct.comp (c.ι.app { as := a }) e)
          ⋯