proposition: Lemma CoequalizerOutUnique {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer f g) (e : C) (h : C⟦b, e⟧) (H : f · h = g · h) (w : C⟦colim E, e⟧) (H' : CoequalizerArrow E · w = h) : w = CoequalizerOut E e h H.
proof: Proof. apply path_to_ctr. use two_rec_dep. - set (X := colimInCommutes E One Two (ii1 tt)). apply (maponpaths (λ h : _, h · w)) in X. use (pathscomp0 (!X)); rewrite <- assoc. change (dmor _ _) with f. change (coconeIn _ _) with (f · h). apply cancel_precomposition, H'. - apply 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.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.EqDiag UniMath.CategoryTheory.Limits.Coequalizers