{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      {f : Y ⟶ X} →
        CategoryTheory.EffectiveEpiStruct f →
          {W : C} →
            (e : Y ⟶ W) →
              (∀ {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) →
                (X ⟶ W)