Definition RightShortExact_Coequalizer_ShortShortExact {x y1 y2 : ob A} (f : x --> y1) (g : x --> y2) : ShortShortExact A. Proof. set (DS := to_BinDirectSums (AbelianToAdditive A) y1 y2). set (CE := Abelian.Coequalizer A (f · to_In1 DS) (g · to_In2 DS)). use make_ShortShortExact. - exact (RightShortExact_Coequalizer_ShortShortExactData f g). - cbn. cbn in CE. fold DS. fold CE. use make_ShortShortExact_isCokernel_isKernel. exact (AdditiveCoequalizerToCokernel_isCokernel (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.