proposition: Lemma limit_universal : is_limit_cone (type_cone d).
proof: Proof. intro X. use isweq_iso. - intros xcone x. unfold standard_limit. use tpair. + exact (λ ver, pr1 xcone ver x). + intros ver1 ver2 ed. apply (toforallpaths _ _ _ (pr2 xcone _ _ _)). - intros f. apply funextfun; intro xcone. use total2_paths_f; cbn; [reflexivity|]. cbn. apply funextsec; intro ver1. apply funextsec; intro ver2. apply funextsec; intro ed. do 2 (rewrite toforallpaths_funextsec). reflexivity. - intro conex. unfold into_cone_to_cone; cbn. use total2_paths_f; cbn. + reflexivity. + apply funextsec; intro ver1. apply funextsec; intro ver2. apply funextsec; intro ed. cbn. rewrite toforallpaths_funextsec; cbn. rewrite funextsec_toforallpaths. reflexivity. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Sets UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Categories.Type.Core UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Chains.Cochains