proposition: Lemma isCoequalizerOutsEq {y z w: C} {f g : y --> z} {e : z --> w} {H : f · e = g · e} (E : isCoequalizer f g e H) {w0 : C} (φ1 φ2: w --> w0) (H' : e · φ1 = e · φ2) : φ1 = φ2.
proof: Proof. assert (H'1 : f · e · φ1 = g · e · φ1). rewrite H. apply idpath. set (E' := make_Coequalizer _ _ _ _ E). repeat rewrite <- assoc in H'1. set (E'ar := CoequalizerOut E' w0 (e · φ1) H'1). intermediate_path E'ar. apply isCoequalizerOutUnique. apply idpath. apply pathsinv0. apply isCoequalizerOutUnique. apply pathsinv0. apply H'. Defined.
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