Lemma LimConeHSET : LimCone D. Proof. use make_LimCone. - apply limset. - exists (λ u f, pr1 f u). abstract (intros u v e; simpl; apply funextfun; intro f; simpl; 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; apply subtypePath]; [ intro; repeat (apply impred; intro); apply setproperty | apply funextsec; intro u; apply (toforallpaths _ _ _ (p u))]). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.WeakEquivalences. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Graphs.Equalizers. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Categories.HSET.Core.