proposition: Lemma PreAdditive_unel_zero (Z : Zero A) (x y : A) : to_unel x y = ZeroArrow Z x y.
proof: Proof. unfold ZeroArrow. rewrite <- (id_left (ZeroArrowFrom y)). assert (X : identity Z = to_unel Z Z). { apply ZeroEndo_is_identity. } rewrite -> X. clear X. set (Y := to_postmor_unel A Z (@ZeroArrowFrom A Z y)). unfold to_postmor in Y. unfold to_unel. rewrite Y. clear Y. set (Y' := to_premor_unel A y (@ZeroArrowTo A Z x)). unfold to_premor in Y'. rewrite Y'. clear Y'. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels