Lemma isExactisEpi {x y : ob A} {f : x --> y} (isE : isEpi f) (H : f · ZeroArrow (to_Zero A) y (to_Zero A) = ZeroArrow (to_Zero A) x (to_Zero A)) : isExact f (ZeroArrow (to_Zero A) y (to_Zero A)) H. Proof. unfold isExact. use make_isKernel. - intros w h H'. use unique_exists. + use KernelIn. * exact h. * rewrite <- (ZeroArrow_comp_right _ _ _ _ _ h). apply cancel_precomposition. apply isE. rewrite CokernelCompZero. rewrite ZeroArrow_comp_right. apply idpath. + cbn. use KernelCommutes. + intros y'. apply hs. + intros y' X. cbn. cbn in X. use (KernelArrowisMonic (to_Zero A) (Abelian.Image f)). rewrite X. apply pathsinv0. use KernelCommutes. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Limits.Zero. 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.Core.Isos. 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.