∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P] {g₁ g₂ : ZeroHom N P}
  {f : ZeroHom M N}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)