Lemma ShortShortExact_isKernel_from_object (D : @DTri PT) (X : ob PT) : isKernel (Abelian.to_Zero abgr_Abelian) (KernelArrow (Image (ShortShortExactData_from_object D X))) (Mor2 (ShortShortExactData_from_object D X)) (@Image_Eq abgr_Abelian (ShortShortExactData_from_object D X)). Proof. use abgr_isKernel_Criteria. - intros D0. induction D0 as [y yH]. set (D' := TrivialDTri PT X). assert (e : y · Mor2 D = ZeroArrow (to_Zero PT) _ (to_Zero PT) · ZeroArrow (to_Zero PT) _ _). { cbn in yH. unfold to_postmor in yH. rewrite yH. rewrite ZeroArrow_comp_left. set (tmp := PreAdditive_unel_zero PT (to_Zero PT) X (Ob3 D)). unfold to_unel in tmp. exact tmp. } set (Ext' := @DExt _ PT (RotDTri PT D') (RotDTri PT D) y (ZeroArrow (Additive.to_Zero PT) _ _) e). use (squash_to_prop Ext' (propproperty _)). intros Ext. clear Ext'. set (Mor := ExtMor1 D' D y (ZeroArrow (Additive.to_Zero PT) _ _) e Ext). use hinhpr. use tpair. + exact (((factorization1_epi abgr_Abelian (Mor1 (ShortShortExactData_from_object D X)) : abgr_Abelian⟦_, _⟧) : monoidfun _ _) (MPMor1 Mor)). + cbn beta. set (comm1 := MPComm1 Mor). rewrite id_left in comm1. use (pathscomp0 _ comm1). clear comm1. set (tmp := @factorization1 abgr_Abelian _ _ (Mor1 (ShortShortExactData_from_object D X))). apply base_paths in tmp. exact (! (toforallpaths _ _ _ tmp (MPMor1 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.