Lemma AbelianPullbackEpi2 {x y z : A} (f : Epi A x z) (g : y --> z) (Pb : Pullback f g) : Epis.isEpi (PullbackPr2 Pb). 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.
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.