Lemma colimArrowUnique' {C : precategory} {g : graph} {d : diagram g C} (CC : ColimCocone d) {c} (k k' : C ⟦ colim CC, c ⟧): (∏ u : vertex g, colimIn CC u · k = colimIn CC u · k') → k = k'. Proof. intro eq. apply pathsinv0. etrans. { apply colimArrowEta. } apply pathsinv0. apply colimArrowUnique. cbn. exact eq. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core.