Definition ShortShortExact_from_isShortExact {a b c : A} (f : a --> b) (g : b --> c) (H : (KernelArrow (Abelian.Image f)) · (CokernelArrow (Abelian.CoImage g)) = ZeroArrow (to_Zero A) _ _) (isEq : isKernel (to_Zero A) (KernelArrow (Abelian.Image f)) (CokernelArrow (Abelian.CoImage g)) H) : ShortShortExact A. Proof. use make_ShortShortExact. - use make_ShortShortExactData. + use make_MorphismPair. * exact a. * exact b. * exact c. * exact f. * exact g. + exact (ShortShortExact_from_isSortExact_eq f g H isEq). - exact (ShortShortExact_from_isShortExact_isKernel f g H isEq). Defined.
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.