proposition: Lemma PairPushoutCokernel {M :PreAdditive} {A B C A':M} (i : A --> B) (p : B --> C) (pr : isKernelCokernelPair i p) (r : A --> A') (po : Pushout i r) (j := PushoutIn2 po) (pp := PairPushoutMap pr r po) : isCokernel' j (pr1 pp).
proof: Proof. set (s := PushoutIn1 po). induction pp as [q [e1 e2]]; change (isCokernel' j q); change (hProptoType (s · q = p)) in e1; change (hProptoType (j · q = 0)) in e2. exists e2. intros T h e. assert (L : i · (s · h) = 0). { refine (assoc _ _ _ @ _). intermediate_path (r · j · h). { apply (maponpaths (λ s, s · h)). exact (PushoutSqrCommutes po). } refine (! assoc _ _ _ @ _). induction (!e). apply zeroRight. } assert (V := iscontrpr1 ((pr22 pr) T (s · h) L)); clear L. induction V as [k e3]. use iscontraprop1. { apply invproofirrelevance; intros φ φ'. apply subtypePath_prop. induction φ as [φ e4]; induction φ' as [φ' e5]; cbn. use (_ : isEpi q). { apply (isEpi_precomp M s q). rewrite e1. apply (CokernelIsEpi i p). apply pr. } exact (e4 @ ! e5). } exists k. use (MorphismsOutofPushoutEqual (isPushout_Pushout po)); fold s j. { refine (assoc _ _ _ @ _ @ e3). apply (maponpaths (λ s, s · k)). exact e1. } { refine (assoc _ _ _ @ _ @ ! e). rewrite e2. apply zeroLeft. } Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Subcategory.Full UniMath.MoreFoundations.Propositions