Definition RightShortExact_Coequalizer_ShortShortExactData {x y1 y2 : ob A} (f : x --> y1) (g : x --> y2) : ShortShortExactData A (to_Zero A). Proof. set (DS := to_BinDirectSums (AbelianToAdditive A) y1 y2). set (CE := Abelian.Coequalizer A (f · to_In1 DS) (g · to_In2 DS)). set (PA := (AbelianToAdditive A) : PreAdditive). use make_ShortShortExactData. - use make_MorphismPair. + exact x. + exact DS. + exact CE. + use (@to_binop PA). * exact (f · to_In1 DS). * exact (@to_inv PA _ _ (g · to_In2 DS)). + exact (CoequalizerArrow CE). - cbn. exact (AdditiveCoequalizerToCokernel_eq1 (AbelianToAdditive A) _ _ CE). 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.