Lemma isCoequalizer_path {hs : has_homsets C} {x y z : C} {f g : x --> y} {e : y --> z} {H H' : f · e = g · e} (iC : isCoequalizer f g e H) : isCoequalizer f g e H'. Proof. use make_isCoequalizer. intros w0 h H'0. use unique_exists. - exact (pr1 (pr1 (iC w0 h H'0))). - exact (pr2 (pr1 (iC w0 h H'0))). - intros y0. apply hs. - intros y0 X. exact (base_paths _ _ (pr2 (iC w0 h H'0) (tpair _ y0 X))). 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.