proposition: Lemma PushoutCokernel {M:PreAdditive} {A B C D E:M} (i:A-->B) (p:B-->C) (j:B-->D) (p':D-->E) (j':C-->E) : isCokernel' i p -> isPushout' (M:=M) j p p' j' -> isCokernel' (i·j) p'.
proof: Proof. intros [b co] [e po]. split. - rewrite assoc'. rewrite e. rewrite assoc. rewrite b. apply zeroLeft. - intros T h v. rewrite assoc' in v. assert (Q := co T (j·h) v); cbn in Q. generalize Q; clear Q. apply iscontrweqb. use make_weq. + intros [k w]; exists (j'·k). rewrite assoc. rewrite <- e. rewrite assoc'. rewrite w. reflexivity. + cbn beta. intros [l w]; unfold hfiber. assert (PO := po T h l (!w)); clear po. generalize PO; clear PO. apply iscontrweqb. refine (weqcomp (weqtotal2asstor _ _) _). apply weqfibtototal; intros m. cbn. apply weqiff. { split. - intros [x y]. split. + exact x. + exact (maponpaths pr1 y). - intros [x y]. exists x. induction y. apply maponpaths, to_has_homsets. } { apply isofhleveltotal2. - apply to_has_homsets. - intros u. refine ((_:isofhlevel 2 _) _ _). apply isofhleveltotal2. + apply to_has_homsets. + intros n. apply hlevelntosn. apply to_has_homsets. } { apply isapropdirprod; apply to_has_homsets. } 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