Lemma AdditiveCokernelToCoequalizer_isCoequalizer {x y : ob A} (f g : x --> y) (CK : Cokernel (to_Zero A) (to_binop _ _ f (to_inv g))) : isCoequalizer f g (CokernelArrow CK) (AdditiveCokernelToCoequalizer_eq1 f g CK). Proof. use make_isCoequalizer. intros w0 h H'. use unique_exists. - use CokernelOut. + exact h. + use to_rcan. * exact (g · h). * rewrite to_lunax''. rewrite <- to_postmor_linear'. rewrite to_assoc. rewrite (@to_linvax' A (to_Zero A)). rewrite to_runax''. apply H'. - cbn. use CokernelCommutes. - intros y0. apply to_has_homsets. - intros y0 X. cbn in X. cbn. use (CokernelArrowisEpi _ CK). rewrite CokernelCommutes. exact X. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Opp. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.BinDirectSums.