proposition: Lemma type_cone_homot_to_path (h : standard_limit_homot) : x = y.
proof: Proof. apply (total2_paths_f (funextsec _ _ _ (pr1 h))). assert (transport_lemma : ∏ p : pr1 x = pr1 y, transportf _ p (pr2 x) = λ u v (ed : edge u v), maponpaths (dmor d ed) (!(toforallpaths _ _ _ p u)) @ pr2 x _ _ ed @ toforallpaths _ _ _ p v). { intros p; induction p; cbn. do 3 (apply funextsec; intro). exact (!(pathscomp0rid _)). } refine (transport_lemma _ @ _). apply funextsec; intro u; apply funextsec; intro v; apply funextsec; intro ed. rewrite toforallpaths_funextsec. change (pr2 y u v ed) with (idpath _ @ (pr2 y u v ed)). refine (_ @ maponpaths (λ p, p @ _) (pathsinv0l (maponpaths _ (pr1 h u)))). refine (_ @ (path_assoc (! maponpaths _ _) (maponpaths _ _) _)). rewrite maponpathsinv0. apply maponpaths, pathsinv0. exact (pr2 h u v ed). 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