proposition: Lemma CoequalizerEndo_is_identity {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer f g) (k : C⟦colim E, colim E⟧) (kH :CoequalizerArrow E · k = CoequalizerArrow E) : identity (colim E) = k.
proof: Proof. apply colim_endo_is_identity. unfold colimIn. use two_rec_dep; cbn. + set (X := (coconeInCommutes (colimCocone E) One Two (ii1 tt))). use (pathscomp0 (! (maponpaths (λ h' : _, h' · k) X))). use (pathscomp0 _ X). rewrite <- assoc. apply cancel_precomposition. apply kH. + apply kH. 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