proposition: Lemma cats_LimConeHSET : Cats.Limits.LimCone D.
proof: Proof. use make_LimCone. - apply cats_limset. - exists (λ u f, pr1 f u). abstract (intros u v e; apply funextfun; intro f; apply (pr2 f)). - intros X CC. use tpair. + use tpair. * intro x; exists (λ u, coneOut CC u x). abstract (intros u v e; apply (toforallpaths _ _ _ (coneOutCommutes CC _ _ e))). * abstract (intro v; apply idpath). + abstract (intros [t p]; apply subtypePath; [ intro; apply impred; intro; apply isaset_set_fun_space | apply funextfun; intro x; apply subtypePath]; [ intro; repeat (apply impred; intro); apply setproperty | simpl; apply funextsec; intro u; apply (toforallpaths _ _ _ (p u))]). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.WeakEquivalences UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Pullbacks UniMath.CategoryTheory.Limits.Graphs.Equalizers UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Categories.HSET.Core