Lemma EqualizerInEq {a b : C} {f g : C⟦a, b⟧} (E : Equalizer f g) (e : C) (h h' : C⟦e, EqualizerObject E⟧) (H : h · EqualizerArrow E = h' · EqualizerArrow E) : h = h'. Proof. refine (EqualizerInUnique E e (h' · EqualizerArrow E) _ h H @ !EqualizerInUnique E e (h' · EqualizerArrow E) _ h' (idpath _)). do 2 refine (assoc' _ _ _ @ !_). apply maponpaths. apply EqualizerArrowEq. 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.