proposition: 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: 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.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.UnivalenceAxiom UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.NumberSystems.Integers UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.ShortExactSequences UniMath.CategoryTheory.Categories.Abgr UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.AdditiveFunctors UniMath.CategoryTheory.FiveLemma