Lemma AdditiveCoequalizerToCokernel_isCokernel {x y : ob A} (f g : x --> y) (CE : Coequalizer f g) : isCokernel (to_Zero A) (to_binop x y f (to_inv g)) (CoequalizerArrow CE) (AdditiveCoequalizerToCokernel_eq1 f g CE). Proof. use make_isCokernel. - intros w h H'. use unique_exists. + use CoequalizerOut. * exact h. * use (to_rcan A (to_inv g · h)). rewrite <- to_postmor_linear'. rewrite <- to_postmor_linear'. rewrite (@to_rinvax' A (to_Zero A)). rewrite ZeroArrow_comp_left. exact H'. + cbn. use CoequalizerCommutes. + intros y0. apply to_has_homsets. + intros y0 X. cbn in X. use (CoequalizerArrowisEpi CE). rewrite CoequalizerCommutes. 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.