proposition: Lemma LimFunctor_unique (F : [A, C, hsC]) (cc : cone D F) : iscontr (∑ x : [A, C, hsC] ⟦ F, LimFunctor ⟧, ∏ v, x · lim_nat_trans_in_data v = coneOut cc v).
proof: Proof. use tpair. - use tpair. + apply (tpair _ (λ a, limArrow (HCg a) _ (cone_pointwise F cc a))). abstract (intros a a' f; simpl; apply pathsinv0; eapply pathscomp0; [ apply (postcompWithLimOfArrows (HCg a)) | apply pathsinv0; eapply pathscomp0; [ apply postcompWithLimArrow | apply limArrowUnique; intro u; eapply pathscomp0; [ now apply limArrowCommutes | now use nat_trans_ax]]]). + abstract (intro u; apply (nat_trans_eq hsC); simpl; intro a; now apply (limArrowCommutes (HCg a))). - abstract (intro t; destruct t as [t1 t2]; apply subtypePath; simpl; [ intro; apply impred; intro u; apply functor_category_has_homsets | apply (nat_trans_eq hsC); simpl; intro a; apply limArrowUnique; intro u; now apply (nat_trans_eq_pointwise (t2 u))]). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory