proposition: 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: Proof. use CokernelOutsEq. rewrite CokernelCommutes. rewrite assoc. rewrite CokernelCommutes. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Zero