English
Any two instances of HasZeroMorphisms C are equal; there is a subsingleton of zero-morphism structures.
Русский
Любые две инстанции HasZeroMorphisms C равны; существует единый (одиночный) нуль-морфизм-структура.
LaTeX
$$$\\forall I,J : HasZeroMorphisms\\, C,\\; I = J$$$
Lean4
/-- If you're tempted to use this lemma "in the wild", you should probably
carefully consider whether you've made a mistake in allowing two
instances of `HasZeroMorphisms` to exist at all.
See, particularly, the note on `zeroMorphismsOfZeroObject` below.
-/
theorem ext (I J : HasZeroMorphisms C) : I = J := by
apply ext_aux
intro X Y
have : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (I.zero X Y).zero := by apply I.zero_comp X (J.zero Y Y).zero
have that : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (J.zero X Y).zero := by apply J.comp_zero (I.zero X Y).zero Y
rw [← this, ← that]
