Lemma lim_endo_is_identity {C : precategory} {g : graph} (D : diagram g C) (CC : LimCone D) (k : lim CC --> lim CC) (H : ∏ u, k · limOut CC u = limOut CC u) : identity _ = k. Proof. use (uniqueExists (limUnivProp CC _ _)). - now apply (limCone CC). - intros v; simpl. unfold compose. simpl. now apply id_left. - 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.Adjunctions.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Import UniMath.CategoryTheory.opp_precat.