∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {B X : C} {f : X ⟶ B} (hf : CategoryTheory.RegularEpi f)
  {W : C} (x : X ⟶ W),
  (∀ {Z : C} (g₁ g₂ : Z ⟶ X),
      CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
        CategoryTheory.CategoryStruct.comp g₁ x = CategoryTheory.CategoryStruct.comp g₂ x) →
    CategoryTheory.CategoryStruct.comp hf.left x = CategoryTheory.CategoryStruct.comp hf.right x