proposition: Lemma retract_is_coequalizer {C : category} {a b : C} (f : retraction b a) : Coequalizer (f · retraction_section f) (identity a).
proof: 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.
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