Definition LeftShortExact_Equalizer_ShortShortExactData {x1 x2 y : ob A} (f : x1 --> y) (g : x2 --> y) : ShortShortExactData A (to_Zero A). Proof. set (DS := to_BinDirectSums (AbelianToAdditive A) x1 x2). set (E := Abelian.Equalizer A (to_Pr1 DS · f) (to_Pr2 DS · g)). set (PA := (AbelianToAdditive A) : PreAdditive). use make_ShortShortExactData. - use make_MorphismPair. + exact E. + exact DS. + exact y. + exact (EqualizerArrow E). + use (@to_binop PA). * exact (to_Pr1 DS · f). * exact (@to_inv PA _ _ (to_Pr2 DS · g)). - cbn. exact (AdditiveEqualizerToKernel_eq1 (AbelianToAdditive A) _ _ E). 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.