Definition from_Cokernel_to_Cokernel {x y : C} {f : x --> y} (CK CK': Cokernel f) : C⟦CK, CK'⟧. Proof. use (CokernelOut CK CK' (CokernelArrow CK')). use CokernelCompZero. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Zero. - exact (ZeroArrowFrom w). - intros y X. cbn in X. use ArrowsFromZero.