Lemma CokernelOutComp {y z : C} {f : y --> z} (K : Cokernel f) {w w' : C} (h1 : z --> w) (h2 : w --> w') (H1 : f · (h1 · h2) = ZeroArrow Z _ _) (H2 : f · h1 = ZeroArrow Z _ _) : CokernelOut K w' (h1 · h2) H1 = CokernelOut K w h1 H2 · h2. Proof. use CokernelOutsEq. rewrite CokernelCommutes. rewrite assoc. rewrite CokernelCommutes. apply idpath. Qed.
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.