proposition: Lemma CoequalizerOutComp {y z : C} {f g : y --> z} (CE : Coequalizer f g) {w w' : C} (h1 : z --> w) (h2 : w --> w') (H1 : f · (h1 · h2) = g · (h1 · h2)) (H2 : f · h1 = g · h1) : CoequalizerOut CE w' (h1 · h2) H1 = CoequalizerOut CE w h1 H2 · h2.
proof: Proof. use CoequalizerOutsEq. rewrite CoequalizerCommutes. rewrite assoc. rewrite CoequalizerCommutes. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Retracts