proposition: Lemma AbelianPushoutMonic2 {x y z : A} (f : Monic A x y) (g : x --> z) (Po : Pushout f g) : Monics.isMonic (PushoutIn2 Po).
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.AbelianToAdditive UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinDirectSums