Lemma CoequalizerEndo_is_identity {y z : C} {f g : y --> z} {E : Coequalizer f g} (φ : C⟦E, E⟧) (H : (CoequalizerArrow E) · φ = CoequalizerArrow E) : identity E = φ. Proof. set (H1 := tpair ((fun φ' : C⟦E, E⟧ => _ · φ' = _)) φ H). assert (H2 : identity_is_CoequalizerOut E = H1). - apply proofirrelevancecontr. apply (isCoequalizer_Coequalizer E). apply CoequalizerEqAr. - apply (base_paths _ _ H2). 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.