Lemma EqualizerInUnique {a b : C} {f g : C⟦a, b⟧} (E : Equalizer f g) (e : C) (h : C⟦e, a⟧) (H : h · f = h · g) (w : C⟦e, lim E⟧) (H' : w · EqualizerArrow E = h) : w = EqualizerIn E e h H. Proof. apply path_to_ctr. use two_rec_dep. - apply H'. - set (X := limOutCommutes E One Two (ii1 tt)). apply (maponpaths (λ h : _, w · h)) in X. use (pathscomp0 (!X)); rewrite assoc. change (dmor _ _) with f. change (coneOut _ _) with (h · f). apply cancel_postcomposition, H'. 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.