Lemma make_ShortShortExact_isCokernel_isKernel (SSED : ShortShortExactData A (to_Zero A)) (H : isCokernel (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. use ShortShortExact_from_isCokernel_isKernel. set (CK := make_Cokernel _ _ _ _ H). set (e1 := factorization2 (Mor2 SSED)). cbn in e1. unfold CoImage. assert (e : is_z_isomorphism (CoIm_to_Im (Mor2 SSED) · KernelArrow (Abelian.Image (Mor2 SSED)))). { use monic_epi_is_iso. - exact (factorization2_is_monic (Mor2 SSED)). - use isEpi_precomp. + exact (Ob2 SSED). + exact (CokernelArrow (Abelian.CoImage (Mor2 SSED))). + rewrite <- e1. use (CokernelArrowisEpi (to_Zero A) CK). } use Cokernel_up_to_iso_isCokernel. + exact CK. + exact (z_iso_inv (make_z_iso _ _ e)). + apply (maponpaths (λ g : _, g · (inv_from_z_iso (make_z_iso _ _ e)))) in e1. use (pathscomp0 _ (! e1)). clear e1. rewrite <- assoc. cbn. rewrite (is_inverse_in_precat1 e). rewrite id_right. 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.