Lemma ShortShortExact_isKernel_to_object (D : @DTri PT) (X : ob PT) : isKernel (Abelian.to_Zero abgr_Abelian) (KernelArrow (Image (ShortShortExactData_to_object D X))) (Mor2 (ShortShortExactData_to_object D X)) (@Image_Eq abgr_Abelian (ShortShortExactData_to_object D X)). Proof. use abgr_isKernel_Criteria. - intros D0. induction D0 as [y yH]. set (D' := InvRotDTri PT (TrivialDTri PT X)). assert (e : ZeroArrow (to_Zero PT) (Ob1 D) (Ob1 D') · Mor1 D' = Mor1 D · y). { rewrite ZeroArrow_comp_left. cbn in yH. unfold to_premor in yH. use (pathscomp0 _ (! yH)). set (tmp := PreAdditive_unel_zero PT (to_Zero PT) (Ob1 D) (Ob2 D')). unfold to_unel in tmp. exact (! tmp). } set (Ext' := DExt PT D D' (ZeroArrow (Additive.to_Zero PT) _ _) y e). use (squash_to_prop Ext' (propproperty _)). intros Ext. clear Ext'. set (Mor := TExtMor Ext). use hinhpr. use tpair. + exact (((factorization1_epi abgr_Abelian (Mor1 (ShortShortExactData_to_object D X)) : abgr_Abelian⟦_, _⟧) : monoidfun _ _) (MPMor3 Mor)). + cbn beta. set (comm2 := MPComm2 Mor). rewrite id_right in comm2. use (pathscomp0 _ (! comm2)). clear comm2. set (tmp := @factorization1 abgr_Abelian _ _ (Mor1 (ShortShortExactData_to_object D X))). apply base_paths in tmp. exact (! (toforallpaths _ _ _ tmp (MPMor3 Mor))). - use KernelArrowisMonic. Qed.
Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinDirectSums. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Abelian. Require Import UniMath.CategoryTheory.ShortExactSequences. Require Import UniMath.CategoryTheory.Categories.Abgr. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Morphisms. Require Import UniMath.CategoryTheory.AdditiveFunctors. Require Import UniMath.CategoryTheory.FiveLemma.