Lemma lim_endo_is_identity {J C : precategory} {F : functor J C} (CC : LimCone F) (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). - now intros v; 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.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory.