Lemma isaprop_Lims : isaprop (Lims C). Proof. apply impred; intro g; apply impred; intro cc. apply invproofirrelevance; intros Hccx Hccy. apply subtypePath. - intro; apply isaprop_isLimCone. - apply (total2_paths_f (isotoid _ H (z_iso_from_lim_to_lim Hccx Hccy))). set (B c := ∏ v, C⟦c,dob cc v⟧). set (C' (c : C) f := forms_cone(c:=c) cc f). rewrite (@transportf_total2 _ B C'). apply subtypePath. + intro; repeat (apply impred; intro); apply univalent_category_has_homsets. + abstract (now simpl; eapply pathscomp0; [apply transportf_isotoid_dep'|]; apply funextsec; intro v; rewrite inv_isotoid, idtoiso_isotoid; cbn; apply limArrowCommutes). 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.