Lemma limUnivProp {C : precategory} {g : graph} {d : diagram g C} (CC : LimCone d) : ∏ (c : C) (cc : cone d c), iscontr (∑ x : C⟦c, lim CC⟧, ∏ (v : vertex g), x · limOut CC v = coneOut cc v). Proof. apply (pr2 CC). 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.