Lemma retract_is_coequalizer {C : category} {a b : C} (f : retraction b a) : Coequalizer (f · retraction_section f) (identity a). Proof. use make_Coequalizer. - exact b. - exact f. - abstract ( refine (_ @ !id_left _); refine (assoc' _ _ _ @ _); refine (maponpaths _ (retraction_is_retraction f) @ _); apply id_right ). - apply make_isCoequalizer. intros d f' Hf'. use unique_exists. + exact (retraction_section f · f'). + abstract exact (assoc _ _ _ @ Hf' @ id_left _). + abstract ( intro y; apply homset_property ). + abstract ( intros g' Hg'; refine (!id_left _ @ _); refine (!maponpaths (λ x, x · _) (retraction_is_retraction f) @ _); refine (assoc' _ _ _ @ _); apply maponpaths; exact Hg' ). 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.