Lemma AbelianPushoutMonic2 {x y z : A} (f : Monic A x y) (g : x --> z) (Po : Pushout f g) : Monics.isMonic (PushoutIn2 Po). Proof. set (DS := to_BinDirectSums (AbelianToAdditive A) y z). set (Po' := Pushout_from_Coequalizer_BinCoproduct A _ _ _ f g (BinDirectSum_BinCoproduct _ DS) (Abelian.Coequalizer A (f · (to_In1 DS)) (g · (to_In2 DS)))). set (iso := z_iso_from_Pushout_to_Pushout Po Po'). apply (isMonic_postcomp A _ (PushoutArrow Po Po' (PushoutIn1 Po') (PushoutIn2 Po') (PushoutSqrCommutes Po'))). rewrite (PushoutArrow_PushoutIn2 Po _ (PushoutIn1 Po') (PushoutIn2 Po') (PushoutSqrCommutes Po')). set (CE := Coequalizer A (f · to_In1 (A:=AbelianToPreAdditive A) DS) (g · to_In2 (A:=AbelianToPreAdditive A) DS)). set (CK := AdditiveCoequalizerToCokernel (AbelianToAdditive A) _ _ CE). set (M1 := @isMonic_to_binop_BinDirectSum1' (AbelianToAdditive A) x y z f g DS). set (K := MonicToKernel' A (make_Monic _ _ M1) CK). use (@to_isMonic (AbelianToAdditive A)). intros z0 g0 H. cbn in H. rewrite assoc in H. set (φ := KernelIn _ K z0 (g0 · to_In2 (A:=AbelianToPreAdditive A) DS) H). set (KComm := KernelCommutes (to_Zero A) K z0 (g0 · to_In2 (A:=AbelianToPreAdditive A) DS) H). fold φ in KComm. assert (e1 : φ = ZeroArrow (to_Zero A) _ _). { use (MonicisMonic _ f). rewrite ZeroArrow_comp_left. cbn in KComm. assert (e2 : (MonicArrow _ f) = (@to_binop (AbelianToAdditive A) _ _ (f · to_In1 (A:=AbelianToPreAdditive A) DS) (@to_inv (AbelianToAdditive A) _ _ (g · to_In2 (A:=AbelianToPreAdditive A) DS))) · to_Pr1 DS). { rewrite to_postmor_linear'. rewrite <- assoc. rewrite PreAdditive_invlcomp. rewrite <- assoc. set (tmp := to_IdIn1 DS). cbn in tmp. cbn. rewrite tmp. clear tmp. set (tmp := to_Unel2' DS). cbn in tmp. rewrite tmp. clear tmp. rewrite ZeroArrow_comp_right. rewrite id_right. apply pathsinv0. set (tmp := @to_runax'' (AbelianToAdditive A) (to_Zero A) _ _ f). exact tmp. } rewrite e2. clear e2. rewrite assoc. cbn in KComm. cbn. rewrite KComm. rewrite <- assoc. set (tmp := to_Unel2' DS). cbn in tmp. rewrite tmp. clear tmp. apply ZeroArrow_comp_right. } use (to_In2_isMonic _ DS). cbn in KComm. use (pathscomp0 (! KComm)). rewrite e1. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. 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.opp_precat. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. 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.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.BinDirectSums.