{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          CategoryTheory.NormalEpi f →
            {X' Y' : C} →
              {f' : X' ⟶ Y'} → (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') → CategoryTheory.NormalEpi f'