Lemma PEq_isMonic' {c d : ob A} (f : c --> d) : isMonic f <-> (∏ (a a' : PseudoElem c), PEq (PseudoIm a f) (PseudoIm a' f) -> PEq a a'). Proof. split. - intros isM. intros a a' X. use make_PEq. + exact (PEqOb X). + exact (PEqEpi1 X). + exact (PEqEpi2 X). + apply isM. set (tmp := PEqEq X). cbn in tmp. rewrite assoc in tmp. rewrite assoc in tmp. apply tmp. - intros X. use (dirprod_pr2 (PEq_isMonic f)). intros d' a X0. apply pathsinv0. use PEq_Zero_Eq'. + exact (PseudoOb a). + use (X a (PZero (PseudoOb a))). use (PEq_trans X0). use PEq_symm. use PEq_ZeroIm. 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.