proposition: Lemma abgr_Additive_premor_postmor_is_iso {Add : CategoryWithAdditiveStructure} (x y : Add) {f : x --> y} (H1 : @is_z_isomorphism abgr_Abelian _ _ (to_premor_monoidfun Add x y x f)) (H2 : @is_z_isomorphism abgr_Abelian _ _ (to_postmor_monoidfun Add y x y f)) : is_z_isomorphism f.
proof: Proof. use make_is_z_isomorphism. - exact (((is_z_isomorphism_mor H1) : (monoidfun (to_abgr x x) (to_abgr y x))) ((identity x) : to_abgr x x)). - exact (abgr_Additive_premor_postmor_is_iso_inverses _ _ H1 H2). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.Algebra.BinaryOperations UniMath.Algebra.Groups UniMath.Algebra.Monoids UniMath.NumberSystems.Integers UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinDirectSums