proposition: Lemma AbelianPullbackEpi2 {x y z : A} (f : Epi A x z) (g : y --> z) (Pb : Pullback f g) : Epis.isEpi (PullbackPr2 Pb).
proof: Proof. set (DS := to_BinDirectSums (AbelianToAdditive A) x y). set (Pb' := Pullback_from_Equalizer_BinProduct A _ _ _ f g (BinDirectSum_BinProduct _ DS) (Abelian.Equalizer A ((to_Pr1 DS) · f) ((to_Pr2 DS) · g))). set (iso := z_iso_from_Pullback_to_Pullback Pb Pb'). apply (isEpi_precomp A (PullbackArrow Pb Pb' (PullbackPr1 Pb') (PullbackPr2 Pb') (PullbackSqrCommutes Pb'))). rewrite (PullbackArrow_PullbackPr2 Pb _ (PullbackPr1 Pb') (PullbackPr2 Pb') (PullbackSqrCommutes Pb')). set (E := Equalizer A ((to_Pr1 DS) · f) ((to_Pr2 DS) · g)). set (K := AdditiveEqualizerToKernel (AbelianToAdditive A) _ _ E). set (E1 := @isEpi_to_binop_BinDirectSum1' (AbelianToAdditive A) x y z f g DS). set (CK := EpiToCokernel' A (make_Epi _ _ E1) K). use (@to_isEpi (AbelianToAdditive A)). intros z0 g0 H. cbn in H. cbn. rewrite <- assoc in H. set (φ := CokernelOut _ CK z0 (to_Pr2 DS · g0) H). set (CKComm := CokernelCommutes (to_Zero A) CK z0 (to_Pr2 DS · g0) H). fold φ in CKComm. assert (e1 : φ = ZeroArrow (to_Zero A) _ _). { use (EpiisEpi _ f). rewrite ZeroArrow_comp_right. cbn in CKComm. assert (e2 : (EpiArrow _ f) = (to_In1 DS) · (@to_binop (AbelianToAdditive A) _ _ (to_Pr1 DS · f) (@to_inv (AbelianToAdditive A) _ _ (to_Pr2 DS · g)))). { rewrite to_premor_linear'. rewrite assoc. rewrite PreAdditive_invrcomp. rewrite assoc. set (tmp := to_IdIn1 DS). cbn in tmp. cbn. rewrite tmp. clear tmp. set (tmp := to_Unel1' DS). cbn in tmp. rewrite tmp. clear tmp. rewrite ZeroArrow_comp_left. rewrite id_left. apply pathsinv0. set (tmp := @to_runax'' (AbelianToAdditive A) (to_Zero A) _ _ f). exact tmp. } rewrite e2. clear e2. rewrite <- assoc. cbn in CKComm. cbn. rewrite CKComm. rewrite assoc. set (tmp := to_Unel1' DS). cbn in tmp. rewrite tmp. clear tmp. apply ZeroArrow_comp_left. } use (to_Pr2_isEpi _ DS). cbn in CKComm. use (pathscomp0 (! CKComm)). rewrite e1. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_right. 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