Lemma make_ShortShortExact_isKernel_isKernel (SSED : ShortShortExactData A (to_Zero A)) (H : isKernel (to_Zero A) (Mor1 SSED) (Mor2 SSED) (ShortShortExactData_Eq (to_Zero A) SSED)) : isKernel (to_Zero A) (KernelArrow (Image SSED)) (Mor2 SSED) (Image_Eq SSED). Proof. set (K := make_Kernel _ _ _ _ H). set (e1 := factorization1 (Mor1 SSED)). cbn in e1. unfold Image. assert (e : is_z_isomorphism (CokernelArrow (Abelian.CoImage (Mor1 SSED)) · CoIm_to_Im (Mor1 SSED))). { use monic_epi_is_iso. - use isMonic_postcomp. + exact (Ob2 SSED). + exact (KernelArrow (Abelian.Image (Mor1 SSED))). + rewrite <- e1. use (KernelArrowisMonic (to_Zero A) K). - exact (factorization1_is_epi (Mor1 SSED)). } use Kernel_up_to_iso_isKernel. + exact K. + exact (z_iso_inv (make_z_iso _ _ e)). + apply (maponpaths (λ g : _, (inv_from_z_iso (make_z_iso _ _ e)) · g)) in e1. use (pathscomp0 _ (! e1)). clear e1. rewrite assoc. cbn. rewrite (is_inverse_in_precat2 e). rewrite id_left. apply idpath. 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.