Lemma equiv_isEqualizer2 {a b : C} (f g : C⟦a, b⟧) (e : C) (h : C⟦e, a⟧) (H : h · f = h · g) : Limits.Equalizers.isEqualizer f g h H <- isEqualizer C f g e h H. Proof. intros X. set (E := make_Equalizer C f g e h H X). intros e' h' H'. use (unique_exists (EqualizerIn C E e' h' H')). - exact (EqualizerArrowComm C E e' h' H'). - intros y. apply hs. - intros y T. cbn in T. use (EqualizerInUnique C E). exact T. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Equalizers.