Lemma retract_is_equalizer {C : category} {a b : C} (f : retraction b a) : Equalizer (f · retraction_section f) (identity a). 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.
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.Monics. Require Import UniMath.CategoryTheory.Retracts.