proposition: Lemma retract_is_equalizer {C : category} {a b : C} (f : retraction b a) : Equalizer (f · retraction_section f) (identity a).
proof: Proof. use make_Equalizer. - exact b. - exact (retraction_section f). - abstract ( refine (_ @ !id_right _); refine (assoc _ _ _ @ _); refine (maponpaths (λ x, x · _) (retraction_is_retraction f) @ _); apply id_left ). - apply make_isEqualizer. intros d f' Hf'. use unique_exists. + exact (f' · f). + abstract exact (assoc' _ _ _ @ Hf' @ id_right _). + abstract ( intro y; apply homset_property ). + abstract ( intros g' Hg'; refine (!id_right _ @ _); refine (!maponpaths _ (retraction_is_retraction f) @ _); refine (assoc _ _ _ @ _); apply (maponpaths (λ x, x · _)); exact Hg' ). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Retracts