∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : Y ⟶ X}
  (self : CategoryTheory.EffectiveEpiStruct f) {W : C} (e : Y ⟶ W)
  (h :
    ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
      CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
        CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e)
  (m : X ⟶ W), CategoryTheory.CategoryStruct.comp f m = e → m = self.desc e ⋯