Lemma PEq_isMonic {c d : ob A} (f : c --> d) : isMonic f <-> (∏ (d' : ob A) (a : PseudoElem c), PEq (PseudoIm a f) (PZero d') -> ZeroArrow (to_Zero A) _ _ = a). Proof. split. - intros isM. intros d' a X. use isM. rewrite ZeroArrow_comp_left. set (tmp := PseudoIm a f). apply pathsinv0. use (PEq_Zero_Eq tmp). unfold tmp. clear tmp. use (PEq_istrans _ _ (PZero d')). + exact (PEq_to_hrel _ _ X). + use PEq_Zeros. - intros X. use (to_isMonic (AbelianToAdditive A)). intros z g H. exact (! ( X z (make_PseudoElem g) (PEq_Eq_Zero (PseudoIm (make_PseudoElem g) f) H))). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Opp. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Morphisms. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Abelian. Require Import UniMath.CategoryTheory.AbelianToAdditive. Require Import UniMath.CategoryTheory.AbelianPushoutPullback. Require Import UniMath.CategoryTheory.ShortExactSequences. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.BinDirectSums.