Definition identity_asEqualizer {y z : C} (f : y --> z) : (Equalizer f f). Proof. use make_Equalizer. + exact y. + exact (identity y). + apply idpath. + use make_isEqualizer. intros x h p. use unique_exists. - exact h. - use id_right. - intro. use homset_property. - intros t t_tri. rewrite <-(id_right t). exact t_tri. 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.