Lemma isExactisMonic {x y : ob A} {f : x --> y} (isM : isMonic f) (H : ZeroArrow (to_Zero A) (to_Zero A) x · f = ZeroArrow (to_Zero A) (to_Zero A) y) : isExact (ZeroArrow (to_Zero A) (to_Zero A) x) f H. Proof. unfold isExact. use make_isKernel. - intros w h H'. use unique_exists. + use KernelIn. * exact h. * rewrite <- (ZeroArrow_comp_left _ _ _ _ _ f) in H'. apply isM in H'. rewrite H'. apply ZeroArrow_comp_left. + cbn. use KernelCommutes. + intros y'. apply hs. + intros y' X. cbn in X. cbn. use (KernelArrowisMonic (to_Zero A) (Abelian.Image (ZeroArrow (to_Zero A) (to_Zero A) x))). 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.