Lemma isExact'_Eq {x y z : ob A} (f : x --> y) (g : y --> z) (H : f · g = ZeroArrow (to_Zero A) _ _) : f · CokernelArrow (Abelian.CoImage g) = ZeroArrow (to_Zero A) _ _. Proof. unfold Abelian.CoImage. set (fact := factorization2 g). unfold factorization2_epi in fact. cbn in fact. unfold Abelian.CoImage in fact. apply (factorization2_is_monic g). rewrite ZeroArrow_comp_left. rewrite <- assoc. apply (maponpaths (λ gg : _, f · gg)) in fact. use (pathscomp0 (! fact)). exact H. 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.