proposition: Lemma isaprop_Lims: isaprop (Lims C).
proof: Proof. apply impred; intro J; apply impred; intro F. 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,F v⟧). set (C' (c : C) f := ∏ u v (e : J⟦u,v⟧), @compose _ c _ _ (f u) (# F e) = f v). rewrite (@transportf_total2 _ B C'). apply subtypePath. + intro; repeat (apply impred; intro). apply (homset_property C). + abstract (simpl; eapply pathscomp0; [apply transportf_isotoid_dep'|]; apply funextsec; intro v; rewrite inv_isotoid, idtoiso_isotoid; cbn; apply limArrowCommutes). Qed.
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