Lemma colim_endo_is_identity {C : precategory} {g : graph} (D : diagram g C) (CC : ColimCocone D) (k : colim CC --> colim CC) (H : ∏ u, colimIn CC u · k = colimIn CC u) : identity _ = k. Proof. use (uniqueExists (colimUnivProp CC _ _)). - now apply (colimCocone CC). - intros v; simpl. now apply id_right. - simpl; now apply H. 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.