proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Equalizers