proposition: Lemma CoequalizerOutUnique' {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer C f g) {e : C} {w w' : C⟦colim E, e⟧} (H : CoequalizerArrow _ E · w = CoequalizerArrow _ E · w') : w = w'.
proof: Proof. use (colimArrowUnique' E). use two_rec_dep. - set (X := colimInCommutes E One Two (ii1 tt)). apply (maponpaths (λ h : _, h · w)) in X. use (pathscomp0 (!X)); rewrite <- assoc. apply pathsinv0. set (Y := colimInCommutes E One Two (ii1 tt)). apply (maponpaths (λ h : _, h · w')) in Y. use (pathscomp0 (!Y)); rewrite <- assoc. apply cancel_precomposition. exact (!H). - exact H. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Chains.Chains UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids UniMath.ModelCategories.Generated.GenericFreeMonoid UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Helpers