∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y W : C} (f f_1 : Y ⟶ X) (e_f : f = f_1)
  [inst_1 : CategoryTheory.EffectiveEpi f] (e e_1 : Y ⟶ W) (e_e : e = e_1)
  (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),
  CategoryTheory.EffectiveEpi.desc f e h = CategoryTheory.EffectiveEpi.desc f_1 e_1 ⋯