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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Retracts. Section CoequalizersFromReflexiveCoequalizers. Section CoequalizersFromReflexive. End CoequalizersFromReflexive. End CoequalizersFromReflexiveCoequalizers.